Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

First formally verified 3D CSG

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.

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.

Performance

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.

Triangle Meshes and Solids

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.) This concept of solids allows us to understand what the output of algorithms such as a mesh intersection algorithm should look like, even when the implementation that works on the actual mesh data structure is intricate and has to treat many geometrical special cases with dedicated code.

From a mesh intersection algorithm, we expect that the set intersection of the solids of well-formed input meshes is the solid of the output mesh and that the output is a well-formed mesh again. (We also expect that the algorithm detects and reports correctly if the inputs are not well-formed.)

solid (meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂

This pins down the surface of the resulting mesh exactly as the boundary of the intersected solids.

Algorithms working on triangle meshes can efficiently compute meshes representing solids we have in mind, but conventional programming languages cannot express "solids" explicitly or make statements about them, since these are infinite sets. In Lean this is possible and we can for example intersect such infinite sets or prove that two infinite sets are equal. Moreover, Lean allows us to prove that a function satisfies a condition for all possible input meshes, whereas conventional programming languages only allow us to test that the function satisfies a condition for specific inputs.

Well-Formedness

We define well-formedness of meshes to capture the conditions commonly expected by real-world mesh processing tools - watertight surface, bounding a solid with multiplicity one with coherent outward orientation, no degenerate triangles, no self-intersections - with one relaxation: the surface may touch itself, not at the interiors of faces but along edges and vertices. So strict 2-manifoldness is not required. See why an intersection algorithm that always produces manifold meshes is not possible.

Certifying Correctness

In order to certify correctness of the kernel, which checks the well-formedness preconditions of the inputs and computes the mesh intersection, a reviewer only needs to read 93 lines of formal specification and run the Lean checker as described below. The reviewer can skip the intricate 1000+ lines of AI-written implementation of the algorithm. The Lean checker guarantees conformance to the specification at compile time, with zero trust assumptions on any LLM.

• It suffices to read the files CSG/DataStructures.lean, CSG/Def.lean, CSG/MeshIntersectWithPreconditionCheck.lean and CSG/WellFormedCheckMsg.lean and run the Lean checker as described below. These are just 93 lines of code, excluding comments. Other files do not need to be read, since the theorem statements that specify meshIntersectWithPreconditionCheck (in the file with the same name) only rest on definitions stated in these 4 files.
• A reviewer can skip the implementation of meshIntersectWithPreconditionCheck that reaches over 1000 lines of code in 4 files in CSG/Impl/, since it is guaranteed by the deterministic Lean checker to conform to the human-reviewed specification.
• This works thanks to 60,000 lines of AI-written formal proofs in CSG/Proof/, which also never have to be inspected by a human.

This compression and simplification from the implementation to the specification is possible because many things the implementation has to deal with can be completely decoupled from the specification:

• The implementation has to handle special geometrical cases, which make up much of the complexity of the algorithm, whereas the formal specification is short because the math can be formulated generally. The Lean checker guarantees that all special cases are handled in accordance with the specification without the specification enumerating the special cases.
• The implementation uses accelerating data structures in order to avoid quadratic runtime complexity and other optimizations. While we did not formalize runtime complexity, the Lean checker guarantees that with all these optimizations we still produce results according to the specification.

If in a future commit we for example further improve the runtime performance or the quality of the output mesh, the reviewed specification stays the same and we get correctness with respect to it, without any re-review.

Development Process

Also see how I developed this project only through shaping this specification. During development, I controlled only a small specification, leaving the proofs and detailed implementation as a black box to agents. I started with a specification that I estimated was relatively easy to implement and formally prove correct and then grew the requirements. In each of the steps listed below, I had the agent implement and formally prove the specification. This stepwise refinement allowed me to delegate large pieces of work to agents, while getting feedback that my specification is satisfiable and verifying the progress of the agents toward my end goal at each milestone. I instructed agents to first write informal proofs before formalizing.

1. I started by having an agent formalize a paper that provides a mathematical framework for describing solids based on simplicial chains. This gave me a formal existence result without concrete implementation (see CSG/Legacy/ChainIntersectionExistence.lean). F. R. Feito and M. Rivero, "Geometric modelling based on simplicial chains," Computers & Graphics 22(5), 611-619 (1998). doi:10.1016/S0097-8493(98)00067-3

2. Then I asked for an implementation with proof of correctness (CSG/Legacy/ChainIntersectionAlgorithm.lean). This already satisfied a formal specification similar to my end goal. But overlapping triangles and other issues were still allowed and did occur.

3. I then specified restrictions for the output mesh (similar to the current state of WellFormedMesh) to forbid the kind of problems from the first implementation. I also introduced a general position restriction on inputs that I later removed, to avoid the implementation having to consider a lot of special cases in this step. The stricter requirements forced a complete reimplementation, but some of the formal framework could be reused.

4. I then removed the general position restrictions on inputs, which forced the agent to handle all special geometrical cases correctly.

5. I then had agents optimize the implementation with bounding volume hierarchies and other optimizations. I did not formalize a requirement on runtime, but Lean verified that the optimization still satisfies the same formal spec. So in this step, I did not have to re-review anything to assure correctness.

6. Finally I strengthened the specification further and made it easier to review. This process resulted in the specification you can see in the top level of the CSG/ folder, the proof at CSG/Proof/ and the implementation at CSG/Impl/.

For most of the above steps I used Claude Opus 4.8. For some I used Fable 5 to create an initial informal proof strategy and then had Opus write formal proofs and implementation. Some of the above steps took over 24 hours of autonomous agent work.

In contrast to regular vibecoding, combining AI with formal verification yields strict guarantees that we know will hold for all inputs and are kept enforced with each subsequent modification of the program. But like regular vibecoding, with each step the development can acquire some debt: both the implementation and the proofs that I ended up with are nowhere near as clean and do not follow a cohesive design, as they would be when controlled by a human who kept an overview of everything. Moreover, there are some constraints we did not formalize here, such as the runtime performance or the way faces of the output solid are triangulated beyond the well-formedness condition. Therefore these constraints are as hard to control as with regular vibecoding.

Comparison with C++ Implementation

For comparison, I gave Opus 4.8 an informal description of the specification and asked it to implement it in C++. The length of the implementation excluding tests, glue etc. was in the same 1000+ lines range as the Lean implementation. Even though it wrote unit tests and iteratively fixed its own implementation, upon inspection by an independent agent comparing it to the formally verified Lean implementation, 3 distinct bugs were discovered in the C++ geometry kernel and reproduced on specific inputs. All of these bugs are rare and would be almost impossible to catch by black box testing. Iterated adversarial review of the code by other agents against the informal specification might have caught these bugs. But without formal verification it is not possible to know for sure that there are no more bugs in the implementation.

The C++ kernel has at least 3 distinct bugs which were reproduced:

1. In certain configurations where a vertex of a well-formed mesh lies on both an edge of another part of the mesh and a face of another well-formed mesh.
2. On well-formed input meshes when a cascade of ray intersection tests in the internal computations all happen to hit triangle edges.
3. In certain configurations where a large face was cut by several small features.

Comparison with informal vibecoding, click to expand prompt used to produce alternative C++ implementation:

Implement an exact 3D mesh intersection algorithm. Write in C++, compile to wasm, produce an artifact I can play with. Is important that the kernel, a simple function is in a self contained separate file, the geometrical kernel separated from the all the glue. (This file only depends on a separate bignum/exact rational implementation, separate file), This function should just take meshes as arrays of triangles with exact coordinates as inputs/outputs. This function should check the inputs are a well-formed mesh in the sense below and produce an error message otherwise. Only run the intersection if inputs are well-formed.

Our definition of "well-formed mesh" captures the conditions commonly expected by real world mesh processing tools - watertight surface, bounding a solid with multiplicity one with coherent outward orientation, no degenerate triangles, no self-intersections - with one relaxation: the surface may touch itself, not at the interiors of faces but along edges and vertices (so strict 2-manifoldness is not required). This relaxation is needed so that intersection of any two well-formed meshes is again well-formed. Everything should be computed with rationals. It should treat all special cases correctly. Always producing a well-formed mesh as output if inputs are well-formed. You can intersect triangles pairwise (use bvh optimization) emitting polygons and triangulating with steiner fans.

Drawbacks of combining formal verification with vibecoding

• It tends to produce code that is slower or disregards other practical considerations that are not captured in the specification. This stems from the difficulty of the formal verification pushing for simpler code and from the lack of formally verified practical software in the training data.
• It can take orders of magnitude more tokens and time for agents to autonomously develop formal proofs, rather than to reason informally about their implementation.
• Many practical problems do not admit a simple formal specification.

As I write this, the capability of AI agents to work on large well-defined tasks is rapidly increasing with each model release. The capability of humans to review their output and reason about it does not. I hope we can use formal verification among other methods as a lever to keep control.

Requires elan. The Lean version is pinned in lean-toolchain (currently leanprover/lean4:v4.15.0).