Simulating physical systems, like how fluids flow or solids deform, is the backbone computational science and engineering. But in order to simulate how a physical system evolves, we have to first describe its shape. This is the problem of mesh generation: How does one take a geometric model of an engine, a lake, a building and decompose it into a mesh of triangles or tetrahedra? Programs for mesh generation are difficult to develop. They require precise and non-standard arithmetic to avoid catastrophic errors, and they rely on some of the most complicated data structures in Computer Science. As a result, most programs for mesh generation are so difficult to change that they are now outdated relative to the capabilities of modern hardware. In this project, the investigators are developing meshing algorithms alongside machine-checked proofs of their correctness. The project’s novelties are to develop proven correct meshing algorithms for the first time, and more generally to develop reusable methodologies for creating geometric software alongside its proof of correctness. In particular, the investigators will re-implement the award winning “Triangle” library for Delaunay triangulation in the language Rocq, develop new, re-usable arithmetic predicates and new relational data structure methodologies for use in this and other correct-by-construction software projects. Quite often, meshing dominates the cost and is the principal constraint on numerical accuracy of a simulation. The project’s impacts are to speed up simulations and improve their accuracy. The migration of key geometric libraries and subroutines to a correct-by-construction methodology also helps with long-term maintenance of such critical software infrastructure. The project work is organized in four interrelated tasks. The first subsystem concerns the development of Rocq-verified, staged floating-point predicates in the style of Priest’s big-float arithmetic, following Jonathan Shewchuk’s o