Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

github.com

Post reply on HN
Print view View original

1–10 of 57 posts

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

#1

Post by permute »

To my knowledge, this is the first formally verified implementation of a 3D constructive solid geometry (CSG) operation: mesh intersection, implemented in Lean 4 and verified against a concise specification that pins down the surface of the resulting mesh exactly and guarantees practical well-formedness conditions on the triangulation.

This project is also an experiment in avoiding having to trust AI-generated code. 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. To prove correctness, AI autonomously wrote over 60,000 lines of Lean proofs, which also never have to be inspected by a human. The Lean checker guarantees conformance to the specification at compile time, with zero trust placed in any LLM. This allows us to treat the implementation and proofs as a black box. I guided the agent through the milestones described in the readme to arrive at the result presented here.

Also take a look at the web demo https://schildep.github.io/verified-3d-mesh-intersection/, which runs the verified mesh intersection kernel compiled to WebAssembly in your browser.

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

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

#2

Post by permute »

Note that the claims are about the kernel that computes the mesh intersection, not the web demo: While the kernel is formally verified, the UI and glue code (that call the kernel) are not. I once hit a bug that looked like there were holes in the resulting mesh: I found that it was an overflow in the glue code (now fixed) that converts the exact rationals coordinates of the output mesh, for which we prove the specification, to floats before sending them to the GPU. All geometry is happening inside the kernel, for which we know the specification holds.

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

#3

Post by iFire »

How does it compare against https://github.com/elalish/manifold in performance and zero corruption?

I spent a lot of time making elalish/manifold work in Godot Engine and it is now a method in Blender too.

https://manifoldcad.org

If it helps, feel free to use the apache2 licensed unit tests that were generated in manifold development https://github.com/elalish/manifold/tree/master/test

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

#5

Post by iFire »

iFire wrote: post #3

How does it compare against https://github.com/elalish/manifold in performance and zero corruption? I spent a lot of time making elalish/manifold work in Godot Engine and it is now a method in Blender too. https://manifoldcad.org If it helps, feel free to use the apache2 licensed unit tests that were generated in manifold development https://github.com/elalish/manifold/tree/master/test

> Why we cannot have manifold output meshes in general

As far as I know manifold is not verified software, but it does promise that manifold inputs become manifold outputs.

I wonder how manifold will break in that condition or would it snap to the nearest manifold.

https://github.com/schildep/verified-3d-mesh-intersection#wh...

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

#6

Post by bob1029 »

This is really neat. I think CSG is one of the more intuitive ways to build 3d environments (especially 'indoor' ones). No geometry is ever destroyed in a proper CSG workflow. A hierarchy of brushes makes it possible to very rapidly iterate parameters like how long a hallway is or the time it takes to get from one objective to another. Often, you only have to apply a transform to a single brush to affect something that would take a non-CSG workflow an entire afternoon to recover from.

The current story with CSG around commercial game engines is pretty awful. Unity has some 3rd party options that can work well but they're also glitchy and don't integrate well with the other parts of the ecosystem. For a while I thinking about building my own CSG implementation but the exact things this project solved were what was stopping me. The EditorWindow integration stuff is not as scary to me (although it is painful). The advanced geometry and set operations is what kept me from trying. It appears that dragon has been (at least partially) slain.

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

#7

Post by permute »

iFire wrote: post #3

How does it compare against https://github.com/elalish/manifold in performance and zero corruption? I spent a lot of time making elalish/manifold work in Godot Engine and it is now a method in Blender too. https://manifoldcad.org If it helps, feel free to use the apache2 licensed unit tests that were generated in manifold development https://github.com/elalish/manifold/tree/master/test

The runtime performance is most probably worse than yours. The goal of this project is a minimal specification that a reviewer can trust. See section in readme on performance and how it could be improved while still keeping formal guarantees, but would mean a reviewer having to trust axioms on floating point numbers: https://github.com/schildep/verified-3d-mesh-intersection#pe...

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

#8

Post by agentultra »

> 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. To prove correctness, AI autonomously wrote over 60,000 lines of Lean proofs, which also never have to be inspected by a human.

I am curious about the approach as I find claims like this hard to believe. There is a theory behind proof kernels that they must be small because they have to be trusted and verifiable by a human. Otherwise the whole system breaks.

How does one trust an LLM generated kernel is proving the right things?

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

#9

Post by iFire »

iFire wrote: post #5
iFire wrote: post #3

How does it compare against https://github.com/elalish/manifold in performance and zero corruption? I spent a lot of time making elalish/manifold work in Godot Engine and it is now a method in Blender too. https://manifoldcad.org If it helps, feel free to use the apache2 licensed unit tests that were generated in manifold development https://github.com/elalish/manifold/tree/master/test

> Why we cannot have manifold output meshes in general As far as I know manifold is not verified software, but it does promise that manifold inputs become manifold outputs. I wonder how manifold will break in that condition or would it snap to the nearest manifold. https://github.com/schildep/verified-3d-mesh-intersection#wh...

On a readme style note, please spend more time explaining the algorithm and less time bragging on how amazing vibe coding is or how Lean has a zero trust proof.

I presume the new advance is claim that verified-3d-mesh-intersection is verified and not the claim that vibe coding can replace hand proofs or that the claim that lean4 can be correct without trusting llms.

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

#10

Post by iFire »

bob1029 wrote: post #6

This is really neat. I think CSG is one of the more intuitive ways to build 3d environments (especially 'indoor' ones). No geometry is ever destroyed in a proper CSG workflow. A hierarchy of brushes makes it possible to very rapidly iterate parameters like how long a hallway is or the time it takes to get from one objective to another. Often, you only have to apply a transform to a single brush to affect something th…

That's why I integrated manifold into godot engine for constructive solid geometry!

https://github.com/godotengine/godot-proposals/issues/9711

Post reply on HN