用 AI 智能体把 30% Git 建模进 Lean 4,证实超 8000 条定理并发现 100+ 潜在缺陷

kfountou · x · 2026-10-24

开发者 Natalie Marleny 宣布一项为期两个月的实验:借助 coding agents 将约 30% 的 Git 用 Lean 4 形式化建模,并证明了 8000 多条关于实现的不同价值定理。

这一过程在 Git v2.55 中发现了超过 100 个潜在缺陷,其中至少两个可能构成安全漏洞。团队还构建了差分随机测试(DRT)框架,积累了目前最大的 Git 实现差分测试语料库(超 1 万个独立测试用例),并已用这些用例测试其内部用 TypeScript 实现的小型 Git,下一步将对所有主流 Git 实现做差分测试。