Experience Report: Smuggling a Little Bit of Coq Inside a CAD Development Context (Extended Abstract)

TL;DR

This paper shares practical insights and experiences on integrating the formal verification tool Coq into CAD software development, highlighting benefits, challenges, and enabling factors for industrial use.

Contribution

It provides real-world examples and analysis of how Coq can be effectively incorporated into CAD development processes, which is rarely documented.

Findings

Coq can be practically used in CAD development with proper factors.

Examples show Coq's advantages in specific verification tasks.

Identifies challenges and non-issues in integrating Coq into industrial workflows.

Abstract

While the use of formal verification techniques is well established in the development of mission-critical software, it is still rare in the production of most other kinds of software. We share our experience that a formal verification tool such as Coq can be very useful and practical in the context of off-the-shelf software development -- CAD in particular -- at least in some occasions. The emphasis is on 3 main areas: factors that can enable the use of Coq in an industrial context; some typical examples of tasks, where Coq can offer an advantage; examples of issues to overcome - and some non-issues - when integrating Coq in a standard development process.