Verified 3D Mesh Intersection: Formally Verifying AI-Generated Geometry Kernels

Formal Verification of 3D Mesh Intersection

The verified-3d-mesh-intersection project provides the first formally verified implementation of a 3D constructive solid geometry (CSG) mesh intersection operation. By using the Lean 4 theorem prover, the project demonstrates a workflow where a human defines a concise formal specification, and an AI agent generates both the complex implementation and the massive volume of proofs required to certify that the implementation adheres to that specification.

This approach shifts the trust requirement from the implementation—which often contains intricate edge cases and thousands of lines of code—to a small, human-readable specification and the deterministic Lean checker.

Trusting the Specification, Not the Implementation

A human reviewer can certify the correctness of the geometry kernel by reviewing only 93 lines of formal specification. The project is structured to decouple the mathematical requirements from the algorithmic execution:

• The Specification (93 lines): Contained within CSG/DataStructures.lean, CSG/Def.lean, CSG/MeshIntersectWithPreconditionCheck.lean, and CSG/WellFormedCheckMsg.lean. This defines what a "well-formed" mesh is and what the resulting intersection of two solids must be.
• The Implementation (1,000+ lines): AI-generated code in CSG/Impl/ that handles the actual geometry calculations and optimizations.
• The Proofs (60,000+ lines): AI-generated formal proofs in CSG/Proof/ that link the implementation to the specification.

Because the Lean checker verifies these proofs at compile time, the implementation and the proofs can be treated as a "black box." If the Lean checker passes, the implementation is guaranteed to conform to the specification regardless of how the AI wrote the code.

Handling Geometric Edge Cases

Formal verification ensures that rare geometric special cases are handled correctly without requiring exhaustive unit testing. In traditional mesh intersection, "edge cases" are often the primary source of bugs. The verified kernel correctly handles scenarios that typically cause failures in unverified implementations, including:

• Coplanar Overlaps: Correctly emitting faces when two tetrahedrons overlap coplanarly with the same normal direction, or producing an empty result when they overlap with opposite normal directions.
• Vertex-on-Face/Edge: Scenarios where a vertex of one mesh lies exactly on the edge or face of another.
• Internal Ray Hits: Cases where internal ray-casting subroutines hit a triangle edge or vertex exactly, or traverse a face coplanarly.
• T-Junctions: The automatic resolution of T-junctions to ensure the output mesh remains well-formed.

Development Workflow: AI-Driven Refinement

The project was developed through a process of stepwise refinement using AI agents (primarily Claude Opus 4.8 and Fable 5). The developer guided the agent through several milestones:

1. Existence Proof: Formalizing a mathematical framework for solids based on simplicial chains.
2. Initial Implementation: Creating a basic algorithm with a proof of correctness, though it initially allowed overlapping triangles.
3. Constraint Strengthening: Introducing "well-formedness" restrictions to forbid mesh corruption.
4. Generalization: Removing general position restrictions to force the AI to handle all special geometric cases.
5. Optimization: Implementing Bounding Volume Hierarchies (BVH) to improve performance. Lean verified that these optimizations did not break the original specification.

Performance and Practical Trade-offs

The verified implementation prioritizes correctness over execution speed. The kernel is significantly slower than state-of-the-art libraries like CGAL or Manifold because it avoids hardware-accelerated floating-point computations to eliminate the need for additional trusted axioms.

For example, intersecting two 70k-triangle Stanford bunnies takes approximately 24 seconds on an M4 Pro. This performance gap is a result of using exact rationals and performing runtime well-formedness checks on all inputs.

Comparison: Formal Verification vs. "Vibecoding"

To test the value of this approach, the author prompted an AI to implement the same specification in C++ (informal "vibecoding"). Despite the AI writing unit tests and iteratively fixing the code, an independent agent discovered three distinct bugs in the C++ kernel that were nearly impossible to catch via black-box testing. These bugs related to specific vertex-on-edge configurations and ray-intersection cascades.

Summary of Trade-offs

Feature	Formal Verification + AI	Informal AI Coding (Vibecoding)
Correctness	Guaranteed by machine-checked proof	Probabilistic; relies on testing
Human Review	Review 93 lines of spec	Review 1,000+ lines of code
Performance	Often slower (simpler/exact math)	Faster (hardware floats)
Development	High token/time cost for proofs	Rapid iteration

Technical Constraints and Limitations

• Non-Manifold Output: The project acknowledges that it is impossible to always produce manifold output meshes. Certain exact rotations of meshes can result in solids whose surfaces touch at a single point or along an edge, creating non-manifold geometry that still satisfies the formal specification of a solid intersection.
• Scope of Verification: The verification applies strictly to the kernel. The UI and "glue code" used in the web demo (which converts exact rationals to floats for GPU rendering) are not verified and may contain bugs.

"The capability of AI agents to work on large well-defined tasks is rapidly increasing... The capability of humans to review their output and reason about it does not. I hope we can use formal verification... as a lever to keep control."

Related Work

• Di Vito and Hocking (2021): Verified polygon merge algorithms in PVS.
• verified-polygon-intersection: A previous project by the author verifying 2D multipolygon intersection in Lean 4.
• CGAL Nef Polyhedra: A widely used unverified exact 3D mesh boolean library.