Formally Verified Mesh Intersection

Tap a solid to edit its exact transform.

First mesh

Denominator digits · 3

Drag a solid in the scene to move it · drag empty space to orbit · scroll / pinch to zoom

Choose the first mesh

Subdivisions · 3

More subdivisions add vertices on the (rationalized) surface — the shape gets rounder.

Supported file formats:

STL — floating-point coordinates will be converted to rational numbers (no rounding).
Plain text (.txt) — custom exact-rational format: a triangle count, then one line of nine rational coordinates per triangle.

Your file stays in your browser — nothing is uploaded to a server.

Caution: Not yet optimized for large meshes. On import the mesh is validated against the WellFormedMesh conditions by the verified kernel.

—

Trust 93 lines of spec, not 1000+ lines of AI code.

Export the result mesh

Computing verified intersection…

Exporting as STL voids guarantees

STL stores coordinates as single-precision floating-point numbers. Snapping the exact rational result to floats can void the guarantees the verified algorithm established — the exported mesh may for example no longer be free of self-intersections. To keep the exact, verified geometry, export the plain-text format instead.

Initializing secure runtime… reload if this persists.