Formally Verified 3D CSG: Trust a 93-Line Spec, Not 1000 Lines of AI Code

A developer has released what is claimed to be the first formally verified implementation of a 3D constructive solid geometry (CSG) operation — mesh intersection — written in Lean 4. The implementation is checked against a concise specification that exactly pins down the surface of the resulting mesh and enforces practical well-formedness conditions on the triangulation.

The project's real experiment is avoiding the need to trust AI-generated code at all. A human reviewer only needs to read the 93-line formal specification and run the Lean checker to certify correctness of the kernel, entirely skipping review of the 1000+ lines of intricate AI-written implementation code.

To establish correctness, an AI agent autonomously wrote over 60,000 lines of Lean proofs that never need human inspection. The Lean checker guarantees conformance to the spec at compile time, placing zero trust in any LLM output, so both implementation and proofs can be treated as a black box. A web demo runs the verified kernel compiled to WebAssembly directly in the browser.