一个新项目展示了首个经过形式化验证的三维构造实心几何（CSG）操作实现 。该项目采用Lean 4验证框架，用93行形式化规范替代传统的1000多行AI生成代码 。这一设计使得人类审查者仅需阅读规范内容并运行Lean检查器，就能认证核心算法的正确性 。