一个新项目展示了首个经过形式化验证的三维构造实心几何（CSG）操作实现 [1]。该项目采用Lean 4验证框架，用93行形式化规范替代传统的1000多行AI生成代码 [1]。这一设计使得人类审查者仅需阅读规范内容并运行Lean检查器，就能认证核心算法的正确性 [1]。
项目的验证工作由AI自主完成，生成了超过60000行的Lean证明代码 [1]。这些证明代码在编译时由Lean检查器进行验证，确保与形式化规范的一致性，整个过程无需对任何大语言模型（LLM）进行信任 [1]。项目还提供了WebAssembly web演示供用户体验 [1]。
A new project demonstrates the first formally verified implementation of three-dimensional Constructive Solid Geometry (CSG) operations, specifically mesh intersection, using Lean 4 for verification [1]. Rather than requiring trust in thousands of lines of AI-generated code, the approach replaces over 1,000 lines of implementation with a concise 93-line formal specification [1]. Human reviewers can now authenticate the kernel's correctness simply by reading the specification and running the Lean checker, with no need to trust any large language model [1].
The verification process leverages AI to autonomously generate over 60,000 lines of Lean proof code, which is then guaranteed at compile time to align with the specification by the Lean checker [1]. This compile-time verification ensures correctness without requiring any trust in the LLM that produced the proofs [1]. The project also provides a WebAssembly web demonstration of the verified implementation [1].