Don't read the AI's code. Read the 93-line spec.

A human wrote 93 lines of formal specification. An AI wrote roughly 1,000 lines of kernel code and over 60,000 lines of proofs. To certify the kernel, a reviewer reads the 93 lines and runs the Lean 4 proof checker. The rest is a black box.

That is the pitch of a Show HN project by GitHub user schildep. The kernel does one thing: compute the exact intersection of two 3D triangle meshes, a building block of constructive solid geometry (CSG) used in CAD tools, 3D printers, and game engines. The author calls it the first formally verified implementation of a 3D CSG operation. That claim is the author's; no independent benchmark or peer review appears in the source bundle.

What makes the project interesting is the workflow, not the geometry. LLM-generated code has made volume a practical review problem. A reviewer can plausibly read 93 lines; almost no one can read 60,000. The repo bets that a small, machine-checkable specification can move the audit bottleneck from code reading to spec writing.

The shape of the trust

The README sets out three layers: a 93-line spec written in Lean 4, an interactive proof assistant and programming language, that defines what the output mesh is and what it means for a mesh to be well-formed; about 1,000 lines of AI-written kernel code that implements the operation against that spec; and over 60,000 lines of AI-written Lean proofs that the kernel matches the spec.

The single load-bearing claim is encoded in [CSG/Def.lean](https://raw.githubusercontent.com/schildep/verified-3d-mesh-intersection/main/CSG/Def.lean): the solid represented by the output mesh of meshIntersect M1 M2 equals the intersection of the solids represented by M1 and M2. Everything else, including well-formedness, exact rational arithmetic, and the precondition check in [MeshIntersectWithPreconditionCheck.lean](https://raw.githubusercontent.com/schildep/verified-3d-mesh-intersection/main/CSG/MeshIntersectWithPreconditionCheck.lean), exists to make that equation checkable.

The reviewer workflow is short: read the 93-line spec, run the Lean checker, and accept its output. The kernel and the proofs are treated as untrusted output from a language model. The same move that a compiler gives you for ordinary code, where you don't read the compiler's source either, is being attempted for an entire numerical kernel.

What the spec actually pins down

The data model in [CSG/DataStructures.lean](https://raw.githubusercontent.com/schildep/verified-3d-mesh-intersection/main/CSG/DataStructures.lean) is plain: a Point is a triple of exact rationals (Fin 3 → Rat), a Triangle is three points, a Mesh is an array of triangles. No floats anywhere in the kernel. Rational arithmetic is what makes the solid-equality theorem provable: the check has to commute with the geometric operation, and floats would break that.

The precondition check, with diagnostics from [WellFormedCheckMsg.lean](https://raw.githubusercontent.com/schildep/verified-3d-mesh-intersection/main/CSG/WellFormedCheckMsg.lean), makes the contract honest. If the input meshes violate the assumptions the proofs rely on, the kernel refuses the operation rather than producing an output whose proof no longer applies. The output mesh, on success, is guaranteed well-formed.

The trust boundary

The headline undersells what is and is not covered. The kernel is verified. The web demo's UI, the glue that loads meshes and renders output, and the STL export are not. STL is the 3D-printing standard, but it stores single-precision floats; snapping exact rationals to floats can introduce errors that violate the theorem the kernel proves. The README flags the consequence: that export path voids the formal guarantee. Any practical pipeline that wants the verified property has to consume the kernel's output directly, not via STL.

Two other caveats sit in the source. The output mesh may be finer than necessary, because the author has not yet formalized compactness. And the performance story is not a story: the browser-runnable demo takes about 24 seconds to compute the exact intersection of two 70,000-triangle Stanford bunnies, orders of magnitude slower than state-of-the-art mesh-intersection libraries. The author frames that gap as not a fundamental limitation of formal verification, and a working engineer should take that claim as motivation rather than proof.

When this pattern fits

The narrow lesson is about 3D meshes. The general one is about the conditions under which "don't read the code" is a defensible engineering posture. Three things have to hold: the property you care about must be expressible in a small spec; a real checker must exist for that spec; and the surface that touches the unverified outside world has to be narrow enough that the boundary failure modes (here, the STL snap) are acceptable.

CSG mesh intersection fits the template because the property is sharp, checkable, and the only thing downstream code needs: the solid of the output mesh equals the intersection of the solids of the inputs. A bug in the meshing density or a slow runtime are engineering nuisances; a bug in the solid equation would be a geometric lie. Formal verification spends its budget on the lie.

The hardest open question is not whether this particular kernel is correct; the Lean checker answers that. It is whether this pattern scales to kernels with messier specifications, where the property you want to enforce is "behaves reasonably on adversarial input" rather than "satisfies equation N." For that, you still have to read the code, or wait for a different kind of checker. The repo is one data point in favor of the narrower claim: when the property is exact and the spec is short, the LLM can be the implementation team.