Formally Verifying 3D CSG: Trusting 93 Lines of Specification Over Thousands of Lines of AI Code

When AI Generates Code, What Should We Trust?

As AI programming assistants become mainstream, developers increasingly rely on large models to generate code. But a pointed question emerges: when AI produces thousands of lines of code in one go, how can we be confident that code is correct?

Recently, a project called "Formally Verified 3D CSG" appeared on Hacker News (earning 37 points and 14 comments), offering a highly inspiring answer: Rather than reviewing 1,000 lines of AI-generated code, trust 93 lines of formally verified specification instead.

This project focuses on 3D CSG (Constructive Solid Geometry), a technique for building complex 3D models by combining simple geometric shapes through Boolean operations (union, intersection, difference). It's widely used in CAD modeling, 3D printing, and game engines.

CSG is a foundational modeling technique in computer graphics and CAD, with its core idea rooted in set theory. Developers can start from basic geometric primitives like spheres, cubes, and cylinders, then construct arbitrarily complex 3D models through Boolean operations. For example, to model a metal block with a hole, you simply perform a difference operation between a cube and a cylinder. CSG has extensive industrial applications: open-source CAD tools like OpenSCAD use CSG as their core modeling paradigm, game engines like Unity and Unreal use CSG for level prototyping, and the 3D printing field relies on CSG for Boolean merging and cutting of models. However, implementing CSG is extremely complex—floating-point precision issues, degenerate geometry (such as coplanar triangles), and edge case handling all make correct CSG implementation a classic hard problem in computational geometry. It's precisely this quality of being "conceptually simple but difficult to implement" that makes it an ideal testing ground for formal verification.

Core Idea: Making Formal Specifications the Anchor of Trust

What Is Formal Verification

Formal Verification is a mathematical proof-based method for rigorously proving that a program's behavior conforms to its specification. Unlike traditional software testing, which can only demonstrate "no bugs were found for specific inputs," formal verification can mathematically prove that a program satisfies given properties for all possible inputs.

Formal verification isn't a new concept—its history traces back to Tony Hoare's Hoare Logic in the 1960s. Current mainstream formal verification tools include: Coq (an interactive theorem prover based on constructive type theory), Lean (a next-generation theorem prover funded by Microsoft), Isabelle/HOL (a proof assistant based on higher-order logic), and TLA+ (a language designed by Leslie Lamport for specifying concurrent systems). In industry, formal verification already has success stories: Intel uses formal methods to verify chip designs to avoid floating-point errors like the Pentium FDIV bug, Amazon Web Services uses TLA+ to verify distributed system protocols, and the CompCert project provides a C compiler fully verified in Coq. These cases demonstrate that formal verification is not merely academic research but a powerful tool for ensuring the correctness of critical systems in engineering practice.

The elegance of this project lies in capturing the essence of the trust problem: whether code is written by humans or generated by AI, what truly needs human review and trust should be the specification that defines "correctness," not the implementation details.

93 Lines of Specification vs. 1,000 Lines of AI Code

The project title itself is a bold value proposition. Let's break down the logic behind it:

• 1,000 lines of AI code: Complex implementation, difficult to review line by line. AI may introduce hard-to-detect edge case errors. Human review of thousands of lines of code is not only time-consuming but also highly prone to oversight.
• 93 lines of specification: A highly condensed description of "what properties CSG operations should satisfy." This specification is short enough for humans to fully understand and be confident it correctly expresses the intended behavior.

Once the specification is trusted by humans, formal verification tools can automatically prove that those 1,000 lines of implementation indeed satisfy these 93 lines of specification. Thus, trust is elegantly transferred to a scale that humans can manage.

The idea of "separating specification from implementation" has deep theoretical roots in computer science. Dijkstra emphasized in his classic work A Discipline of Programming that program correctness should be defined relative to its specification. This idea manifests in Design by Contract (popularized by Bertrand Meyer in the Eiffel language), Dependent Types, and Refinement Types. A specification essentially answers "What" (what should the system do), while implementation answers "How" (how does the system do it). In the AI programming era, this separation gains new practical significance: when implementation cost approaches zero (handled by AI), human core value focuses on precisely expressing intent—that is, writing correct specifications.

Why Formal Verification Is Especially Important in the AI Programming Era

The Trust Crisis of AI Code

Under the current AI programming paradigm, developers face a paradox: AI can rapidly produce massive amounts of code, but the sheer volume actually intensifies the review burden. Traditional "manual code review" is gradually losing feasibility when facing vast quantities of AI-generated code.

Current mainstream AI programming assistants (such as GitHub Copilot, Cursor, Claude, etc.) are based on large language models (LLMs), whose code generation is fundamentally a probabilistic token prediction process, not logical reasoning. Multiple studies show that AI-generated code correctness varies with task complexity: it may exceed 80% on simple algorithmic problems, but can drop significantly in scenarios involving complex state management, concurrency control, or edge condition handling. More troublesome is that AI-generated errors often possess "surface plausibility"—the code structure is complete, naming is proper, and it may even pass some test cases, but produces incorrect results under specific boundary conditions. This characteristic of "looking correct but having subtle bugs" makes manual review particularly difficult.

The solution proposed by this project points toward a possible way out: shift the object of trust from "implementation" to "specification." Specifications are inherently more concise than implementations and closer to human thinking, as they are essentially formalized expressions of intent.

From "Reviewing Code" to "Reviewing Intent"

The significance of this shift is profound. In traditional software engineering, specifications are often vague, written in documentation, and disconnected from code. Formal verification demands that specifications be precise, executable, and strictly bound to the implementation.

Once AI handles most of the implementation work, the human role can focus on:

1. Writing and reviewing specifications — ensuring what we truly want is correctly defined
2. Trusting verification tools — letting mathematical proofs replace manual line-by-line checking
3. Focusing on high-level design — investing energy in "what to do" rather than "how to do it"

This effectively redraws the boundary of responsibilities between humans and AI in software development.

The Rationale of 3D CSG as a Formal Verification Target

Choosing 3D CSG (Constructive Solid Geometry) as the formal verification target is quite wise. CSG operations have clear mathematical definitions—Boolean set operations—whose correctness can be precisely described in the language of geometry and set theory.

This type of problem is an ideal scenario for formal verification:

• Solid mathematical foundation: Union, intersection, and difference all have well-defined mathematical semantics
• Properties are easy to express: Commutativity, associativity, boundary handling, etc., can all be formalized
• Implementation is complex but specification is simple: Geometric computation code is often lengthy and full of edge cases, while the properties it should satisfy are relatively concise

This characteristic of "simple specification, complex implementation" is precisely where formal verification delivers the most value, and perfectly matches the contrast of "93 lines of specification vs. 1,000 lines of implementation."

Implications for Future Software Development

Verification-First: A Scalable Trust Model

Though small, this project outlines a trust model that remains reliable in the AI era. As code generation capabilities continue to strengthen, the "verification-first" development paradigm may become increasingly important.

Imagine a future where developers only need to carefully write correct specifications, AI handles generating implementations that satisfy those specifications, and formal verification tools automatically guarantee consistency between the two. Humans no longer need to read those machine-generated implementation details—they only need to be confident that their intent has been accurately captured.

The "Verification-First" philosophy is gaining increasing attention. In the blockchain and smart contract space, because code is immutable once deployed and directly manages assets, formal verification has become an industry best practice—companies like Certora and Runtime Verification specialize in providing formal verification services for smart contracts. In the AI-assisted programming field, emerging research directions include: having AI generate not just code but also proofs (as AlphaProof attempted in mathematical competitions), specification-based Program Synthesis, and using LLMs to assist in writing formal specifications. These trends indicate that the fusion of formal methods and AI is moving from academic research toward engineering practice, potentially forming a new software development paradigm in the future.

Real-World Challenges and Limitations

Of course, this path also faces practical challenges. Formal verification itself has a high barrier to entry, writing correct specifications requires specialized skills, and not all software problems have clear mathematical definitions like CSG. For applications with complex business logic where the specification itself is difficult to formalize, the applicability of this approach still needs exploration.

Additionally, the capability boundaries of verification tools, performance overhead, and potential errors in the specification itself (garbage in, garbage out) are all issues that require careful consideration. It's worth noting that there exists a problem in formal verification known as the "verifier's dilemma": how do we guarantee the correctness of the verification tool itself? Mainstream strategies include using verified proof checkers (such as Coq's kernel, which is only a few thousand lines of code—small enough to be manually audited) and cross-verification with multiple tools. These are engineering realities that must be confronted when promoting the "verification-first" paradigm in practice.

Conclusion

This small project that appeared on Hacker News uses a clever comparison to reveal a core proposition of the AI programming era: In a world where code can be generated infinitely, the scarce resource of trust is "proof of correctness," not "the code itself."

The contrast between 93 lines of specification and 1,000 lines of implementation is not just a technical demo but a manifesto of a development philosophy—anchoring human trust in manageable, verifiable specifications, and letting machines handle the heavy lifting of implementation and proof. This may well be a microcosm of how formal methods and AI programming are converging.