verified-3d-mesh-intersection - Formally verified 3D CSG mesh intersection
Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
verified-3d-mesh-intersection is the first formally verified implementation of 3D constructive solid geometry (CSG) mesh intersection, built in Lean 4. This project revolutionizes trust in AI-generated code by allowing human reviewers to verify only 93 lines of concise specification, while the Lean checker guarantees the correctness of over 1,000 lines of complex AI-written implementation. Users can test the verified kernel via a local web demo that processes STL files without sending data to a server. While prioritizing mathematical certainty over raw speed, it ensures watertight, well-formed output meshes, proving that rigorous formal verification can coexist with AI-driven development.
A human reviewer only needs to read 93 lines of formal specification and run the Lean checker to certify the correctness of the kernel, skipping the intricate 1000+ lines of AI-written implementation.