This project presents what is believed to be the first formally verified implementation of 3D mesh intersection, a constructive solid geometry (CSG) operation. Developed in Lean 4, the implementation is verified against a concise 93-line formal specification that precisely defines the resulting mesh's surface and guarantees practical well-formedness conditions.

An experimental aspect of this work is its approach to AI-generated code. A human reviewer is only required to examine the 93 lines of formal specification and run the Lean checker, bypassing the need to scrutinize the 1000+ lines of AI-written implementation code. To establish correctness, AI autonomously generated over 60,000 lines of Lean proofs, which also do not require human inspection. The Lean checker ensures conformance to the specification at compile time, eliminating trust in any Large Language Model (LLM).

A web demo is available, showcasing the verified mesh intersection kernel compiled to WebAssembly. This allows users to intersect example meshes or import and intersect meshes from STL files directly in their browser. While the kernel is formally verified, the UI and glue code are not. Performance is currently slower than state-of-the-art implementations, prioritizing minimized human review effort over speed.