coding agents 将约 30% Git 建模进 Lean 4，证明 8000 多条定理并发现 100 多个潜在缺陷

开发者 Natalie Marleny 宣布一项为期两个月的实验，借助 coding agents 将约 30% 的 Git 用 Lean 4 形式化建模，并证明了 8000 多条关于实现的定理。实验在 Git v2.55 中发现超过 100 个潜在缺陷，其中至少两个可能构成安全漏洞。团队还构建了差分随机测试框架，形成超过 1 万个独立测试用例的 Git 实现差分测试语料库。