Formally Verified 3D CSG: Prioritizing a 93-Line Spec over 1,000+ Lines of AI Code

This project introduces what is, to the author's knowledge, the first formally verified implementation of a 3D Constructive Solid Geometry (CSG) operation—specifically, mesh intersection. Developed using Lean 4, the system is verified against a compact specification that precisely defines the resulting mesh surface and ensures essential well-formedness for the triangulation.

🛡️ The Philosophy of Trust

The primary goal of this experiment was to eliminate the need to trust AI-generated code. In traditional AI-assisted development, you must trust the LLM's output; here, the trust is shifted to a mathematical proof.

The Review Burden

By utilizing the Lean checker, the correctness of the kernel is certified at compile time. Because the AI autonomously generated the implementation and the massive volume of proofs, they can be treated as a black box. A human reviewer only needs to verify the 93-line specification to be certain of the result.

🌐 Web Demonstration

A live web demo is available, allowing users to intersect example meshes or upload their own via STL files.

• Privacy: The compiled Lean code executes locally in the browser via WebAssembly; no data is transmitted to a server.
• Scope of Verification:
  • Core Intersection Kernel (Verified)
  • User Interface (Not Verified)
  • Glue Code (Not Verified)

Performance Note

The implementation prioritizes provable correctness over execution speed.

Benchmark: It takes approximately 24 seconds to compute the exact intersection of two Stanford bunnies (each containing 70k triangles).

While this is significantly slower than state-of-the-art non-verified tools, this is a choice of priority, not a fundamental limitation of formal verification. Additionally, while the output is guaranteed to be correct, the resulting triangulation may be finer than necessary (suboptimal density).

📐 Background & Formalization

Defining the "Solid"

A triangle mesh is typically viewed as a set of triangles forming a closed, non-self-penetrating surface. However, humans perceive these as solids—volumes in 3D space.

Definition: A "solid" is the set of all points not on the surface but "inside" the mesh, which can be mathematically determined using signed ray intersection counting.

This abstraction allows us to define the goal of a mesh intersection algorithm using set theory:

$\text{solid}(\text{meshIntersect } M_1, M_2) = \text{solid } M_1 \cap \text{solid } M_2$

Why Lean 4?

Conventional languages cannot explicitly represent "solids" because they are infinite sets of points. Lean 4 enables:

1. Infinite Set Manipulation: The ability to intersect infinite sets and prove their equality.
2. Universal Quantification: Proving a function works for all possible input meshes, rather than just passing a finite set of test cases.

Mesh Well-Formedness

To ensure the output is usable by real-world tools, the project defines "well-formedness" as follows:

• Watertight: The surface must be closed.
• Orientation: Coherent outward-facing normals.
• Multiplicity: Bounding a solid with multiplicity one.
• Geometry: No degenerate triangles.
• Intersections: No self-intersections (though the surface may touch itself at vertices or along edges).

Note: It is mathematically impossible for an intersection algorithm to always produce strictly manifold meshes.

🛠️ Technical Implementation Details

The project structure includes several key components for the build and deployment process:

# Key files in the repository
lakefile.lean       # Lean build configuration
Web.lean            # Web-specific logic
emcc-wasm.sh        # Emscripten compilation script
wrapper.c            # C wrapper for Wasm integration

The workflow involved guiding an AI agent through specific milestones to reach the final verified state, ensuring that every step of the implementation was backed by a machine-checked proof.