HN Debrief

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

  • Programming
  • Developer Tools
  • AI
  • Open Source

The project is a formally verified implementation of one 3D constructive solid geometry operation: intersecting triangle meshes. It is written in Lean 4, and the core claim is that a human can review a 93 line formal specification, run the Lean checker, and avoid reading the 1000 plus lines of AI-generated implementation and 60000 plus lines of AI-generated proofs. That does not mean the whole demo is verified. The author explicitly says only the geometry kernel is covered. The browser demo and glue code are outside the proof boundary, and one past bug came from converting exact rational output coordinates to floats for the GPU.

If you are considering AI-generated systems code, this is a concrete pattern worth watching: lock down a small formal spec and treat the generated implementation as disposable. For geometry and other edge-case-heavy domains, verification looks more plausible today as a trust tool than as a route to production performance.

Discussion mood

Strongly positive and impressed, with curiosity focused on what exactly is verified and skepticism centered on performance and the remaining trust chain. People liked the idea of using formal methods to contain AI-generated code, but they were quick to point out that toolchains, compilers, hardware, and unverified glue still matter.

Key insights

  1. 01

    The verified core stops before rendering

    The proof boundary ends at the mesh intersection function itself, which sharply changes how to interpret the demo. A real bug already slipped through in the unverified glue that converted exact rational coordinates to floats for the GPU, producing apparent holes even though the proven kernel was fine. That is a good reminder that formal guarantees survive only as far as the verified interface does.

    If you adopt this pattern, keep the verified component narrow and make boundary conversions painfully explicit. Expect bugs to migrate into adapters, serialization, and display code.

      Attribution:
    • permute #1
  2. 02

    Verification shrinks trust, not to zero

    The meaningful gain here is not absolute proof of running machine code. Lean still goes through an unverified compiler path, often via generated C, and hardware can violate its own spec under real conditions. Even so, that leaves you trusting the same messy lower stack you already trust every day while removing most of the application-level algorithm risk. For a brittle geometry engine, that is a big reduction in where subtle bugs can hide.

    Treat formal verification as a way to move risk downward into shared infrastructure, not to erase it. That framing makes it easier to decide where the extra proof effort is worth paying.

      Attribution:
    • angry_octet #1 #2
    • ekidd #1
    • kens #1
  3. 03

    Exact arithmetic is the current price

    The implementation gets its guarantees by using exact rational numbers, represented with unbounded integers, for all geometric operations. That avoids numerical instability, but it is also why performance is expected to lag practical libraries. The promising path is the standard exact-predicate design used by CGAL, where floating point handles easy cases and exact arithmetic resolves ambiguous ones. That keeps correctness on the hard cases instead of papering them over.

    Do not read this as “verified means slow forever.” Read it as a reference design for the correctness layer, with room to swap in a filtered arithmetic backend later.

      Attribution:
    • permute #1 #2
    • TobiasJacob #1
    • amuresan #1
  4. 04

    Mesh CSG is useful well beyond demos

    People building tools in Unity, Godot, Blender, and level editors treated this as relevant because boolean operations on meshes are still a practical pain point. Existing libraries like Manifold have improved the situation and are already shipping in places like Blender and Godot integrations, but this project tackles the part many teams avoid touching at all: the algorithmic and topological edge cases inside the boolean kernel. That gives it value even if nobody ships this exact codepath unchanged.

    If your product depends on robust booleans, watch the spec and proof structure more than the current benchmark numbers. The reusable asset may be the formal contract, not this exact implementation.

      Attribution:
    • bob1029 #1
    • iFire #1 #2
    • regularfry #1
  5. 05

    The spec choice makes intersection easier than union

    The current proof is not just “one boolean op done, the rest are trivial.” The author defined solids in a way that excludes the mesh surface itself, which fits intersection neatly but means union needs a different specification shape. That is a subtle point, because it shows the hard part is often the mathematical contract, not just coding another operation. The implementation could likely be reduced to intersection tricks, but the proof story still has to be rewritten carefully.

    When scoping formal methods work, budget heavily for specification design. Extending coverage to nearby features can require new semantics even when the algorithmic reduction looks obvious.

      Attribution:
    • permute #1 #2

Against the grain

  1. 01

    Verified rationals miss many production constraints

    For teams that need hardware-accelerated floating point and high throughput, this exact implementation does not yet solve the operational problem. The proof covers a mathematically cleaner arithmetic model than the one most production geometry pipelines actually run. That limits immediate applicability, even if proofs over floating point are possible in principle.

    Do not mistake a correctness milestone for a drop-in production kernel. If latency and throughput dominate your requirements, wait for a verified filtered-arithmetic version or plan to invest in one.

      Attribution:
    • CyLith #1
    • permute #1
    • angry_octet #1
    • TacticalCoder #1
  2. 02

    The repo undersells the algorithm itself

    One complaint was that the readme spends too much effort on the “zero trust AI” framing and not enough on explaining the geometric algorithm. That matters because the enduring contribution may be the algorithm-spec-proof package, while the AI angle is mostly packaging around it. Readers trying to learn from the work want the geometry story, not just the trust story.

    If you publish formal-methods work for practitioners, document the algorithm as carefully as the proof boundary. Otherwise you will attract curiosity but slow down adoption and reuse.

      Attribution:
    • iFire #1

In plain english

CGAL ↩
Computational Geometry Algorithms Library, a widely used C++ library for geometry algorithms that includes robust exact-predicate techniques.
coplanar ↩
Lying on the same geometric plane.
CSG ↩
Constructive solid geometry, a way to build 3D shapes by combining simpler solids with operations like union, intersection, and difference.
exact rational arithmetic ↩
Arithmetic done with exact fractions instead of approximate floating point numbers, so results have no rounding error.
floating point ↩
The standard computer number format for fast approximate real-number calculations, which can introduce rounding errors.
formal specification ↩
A precise mathematical description of what a program must do, written so a proof assistant can check claims against it.
geometry kernel ↩
The core algorithmic part of a geometry system that performs operations like intersections and booleans on shapes.
Lean 4 ↩
A programming language and proof assistant used to write code, formal specifications, and machine-checked mathematical proofs.
mesh ↩
A 3D shape represented by vertices, edges, and usually triangular faces.
mesh intersection ↩
A boolean operation that computes the part of two 3D meshes that occupies the same space.
predicate ↩
In computational geometry, a test that returns true or false, such as whether a point lies on one side of a plane.
proof kernel ↩
The small trusted core of a proof assistant that checks whether proofs are valid.

Reference links

Project and demo

Related geometry libraries and integrations

Verification and compiler chain references

Project readme sections discussed