Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

Who Should Read

Backend or agent developers wondering how to trust AI-written code before shipping it

Core Mechanics

• Only 93 lines of spec to read
  • The author implemented and verified 3D mesh intersection (CSG) in Lean 4.
  • A human reads 4 spec files (93 lines excluding comments) and runs the Lean checker.
  • The 1000+ lines of AI implementation and 60,000+ lines of proofs need not be read.
• The checker replaces trust in the LLM
  • The deterministic Lean checker confirms at compile time that the implementation matches the spec.
  • The author says no trust in any LLM is required.
  • The spec is short: solid(meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂.
• Grow the spec in steps and delegate
  • He started with an easy spec and added requirements step by step.
  • At each step the agent reimplemented and reproved.
  • Adding BVH and other optimizations required no re-review because the spec stayed the same.
• Same spec in C++ vibecoding had 3 bugs
  • Opus 4.8 implemented an informal spec in C++ at a similar 1000+ lines.

Community Reactions

• Doubts about whether the spec is right
  • One commenter noted that proof kernels are traditionally small so humans can trust them, and asked how an LLM-generated one can be trusted.
  • Another asked how a verified proof connects to an implementation that actually conforms to it.
• Author says the demo bug was not in the kernel
  • Holes in the output mesh turned out to be an overflow in glue code converting exact rationals to floats for the GPU (since fixed).
  • The author added that the UI and glue code are not verified; only the kernel is.
• Practicality objections
  • One commenter said that without hardware-accelerated floating point these algorithms are too slow to be useful.
  • Others asked about numerical stability and coplanar faces if extended to floats.
• Requests for comparison with existing libraries
  • A commenter asked for a comparison with elalish/manifold on performance and zero corruption.
  • They suggested using manifold's Apache2 unit tests.
  • Others asked about extending to union and difference and about fuzz testing.

How to Apply

• Write a short spec before the code
  • Pick one function the AI is writing today and write its input-output property in one line.
  • For example, a sort result is a permutation of the input and ascending.
  • Turn that property into a test before reading the implementation.
• Verify AI code with property-based tests
  • Add Hypothesis or fast-check tests to your core logic.
  • Run the AI implementation on random inputs even after unit tests pass.
• Grow the spec in steps and delegate
  • Start with easy requirements and have the agent implement and verify at each milestone.
  • Confirm the spec is satisfiable before adding the next requirement.
• Cross-review with a different agent
  • Have an agent other than the author compare the informal spec against the code and reproduce bugs.
  • Save each reproducing input as a regression test.

Try It

# Paste into Claude or ChatGPT (simplified version of the paper's method: spec first, implementation as a black box)

For the function below, write the spec first without looking at the implementation.
Function description: {{function description}}

1. Write the properties that must always hold between input and output, in 5 lines or fewer.
2. Turn them into Hypothesis (Python) property-based tests.
3. Write the implementation separately from a different angle.

Next to try: paste your implementation {{implementation}} and ask for counterexamples that break the tests.

Terminology

Related Papers

• The Judge Can Debias Itself: Awareness and Self-Debiasing for Reliable LLM-as-a-Judge

  Warning an LLM judge about bias or letting it self-critique improved 20 of 21 model–bias combinations.

• 90% of US working hours are spent on tasks not covered well by AI benchmarks

  Mapping 29 benchmarks to job tasks shows 90% of US working hours lack good coverage

• Postgres 19 delayed after AI reviewers find more bugs than humans can fix

  LLM code review surfaced so many bugs that Postgres 19 slipped to November and 8-10 features were reverted

• Show HN: Gemini 4 Argon plays StarCraft

  LLMs wrote StarCraft bots in one hour; GPT-6 Astra scored highest.

• A Plausible Explanation Is Enough to Mislead Multimodal Judges

  Adding plausible explanations to fixed answers cut MLLM judges' wrong-answer rejection by 12.7–13.8 points.

• Neural networks are clean

  Looking at neurons directly shows most have one main job, challenging superposition.

Related Resources

• https://github.com/schildep/verified-3d-mesh-intersection
• https://schildep.github.io/verified-3d-mesh-intersection/
• https://github.com/elalish/manifold
• https://manifoldcad.org