GoKawiilFormally verified 3D mesh intersection - trust 93 lines of spec, not 1000+ lines of AI-written code
To my knowledge, this is the first formally verified implementation of a 3D constructive solid geometry (CSG) operation: mesh intersection, implemented in Lean 4 and verified against a concise specification that pins down the surface of the resulting mesh exactly and guarantees practical well-formedness conditions on the triangulation. (See also related work.)
This project is also an experiment in avoiding having to trust AI-generated code. A human reviewer only needs to read 93 lines of formal specification and run the Lean checker as described below to certify the correctness of the kernel, skipping the intricate 1000+ lines of AI-written implementation. To prove correctness, AI autonomously wrote over 60,000 lines of Lean proofs, which also never have to be inspected by a human. The Lean checker guarantees conformance to the specification at compile time, with zero trust placed in any LLM. This allows us to treat the implementation and proofs as a black box. I guided the agent through the milestones described below to arrive at the result presented here.
Web demo
Try out the web demo built around the verified kernel, where you can intersect example meshes or import and intersect meshes from STL files. The compiled Lean code runs locally in your browser; no data is ever sent to a server. Note that while the kernel is formally verified, the UI and glue code are not.
Our implementation is far slower than state-of-the-art mesh intersection implementations: it takes 24 seconds to compute the exact intersection of two 70k-triangle Stanford bunnies. In this project we prioritize minimizing the effort of human review of correctness over performance. Note that this performance gap is not a fundamental limitation of formally verified software, which can in principle be as fast as conventional software. See details.
The output meshes are guaranteed to satisfy the properties described below, but the meshing may be suboptimal with respect to other criteria that we did not yet formalize; for example, it may produce a mesh that is finer than necessary.
Background and formalization
A triangle mesh is a set of triangles, usually expected to form a closed surface that does not penetrate itself, among other well-formedness conditions we will discuss below.
Humans intuitively associate triangle meshes with a "solid", i.e. a volume in 3D space: the set of all points not on the surface but "inside" the mesh. ("Inside" can be described mathematically by signed ray intersection counting.)
... continue reading