Developer releases formally verified 3D mesh tool to cut reliance on AI code
A new open-source project demonstrates how formal verification can eliminate the need to trust large language models in software development, though performance remains a trade-off.
A developer has published a formally verified implementation of a 3D constructive solid geometry (CSG) mesh intersection algorithm in Lean 4, aiming to reduce the need for human review of AI-generated code. The project, hosted on GitHub under the repository schildep/verified-3d-mesh-intersection, shifts the burden of verification to a concise 93-line formal specification rather than relying on trust in the more than 1,000 lines of implementation code generated by artificial intelligence.
The AI autonomously wrote more than 60,000 lines of Lean proofs, which are verified at compile time with zero trust placed in large language models. By treating the implementation and proofs as a black box, the developer argues that human reviewers only need to inspect the short specification and run the Lean checker to certify the kernel’s correctness. This approach allows the system to guarantee conformance to the specification for all possible inputs, rather than just specific test cases.
While the computational kernel is formally verified, the user interface and glue code are not. The implementation prioritises mathematical correctness over performance, taking 24 seconds to compute the exact intersection of two 70,000-triangle meshes. This is significantly slower than state-of-the-art conventional tools, though the developer noted that this performance gap is not a fundamental limitation of formally verified software.
The project utilises a stepwise refinement process guided by AI models including Claude Opus 4.8 and Fable 5. A comparative test revealed that a C++ implementation of the same specification, written by the same AI model, contained at least three distinct bugs in rare geometric configurations. These bugs were undetectable by black-box testing but were identified when comparing the C++ code against the formally verified Lean implementation.
The tool includes a web demo where users can intersect example meshes or import STL files; the compiled Lean code runs locally in the browser, ensuring no data is sent to a server. The specification allows for non-manifold surfaces, such as touching along edges or vertices, to ensure the intersection of any two well-formed meshes remains well-formed. The developer cautioned that while formal verification provides strict guarantees, the resulting code may acquire technical debt and lack the cohesive design of human-controlled code.
