用 Lean 形式化 Julia 源码，AI 辅助证明找出 Base 中约 400 个 bug
ericjang11 · x · 2026-10-30
Miles Cranmer 在 Julia Discourse 发文，介绍用 Lean 4 形式化验证软件的新实践，并称受近期安全事件中「形式化找漏洞」方法启发。
- 方法：把每个 Julia 函数建模为 Lean 模型，docstring 的承诺变成定理，让 AI agent 尝试证明；证明失败时的反例通常就是 bug，再回到真实 Julia 中验证。AI 数学能力提升后，这类以前需要手写形式化证明的工作可以大规模进行。
- 成果：在自己的 DynamicExpressions.jl 包上发现大量潜藏 bug——即使这是经过精心编写、重度测试、100% 人工审查的代码库；对 Julia 语言本身的完整源码做形式化，至今已找出约 400 个 Base 库 bug。
- 结论：这不代表 Base 比一般软件更糟糕，而是说明 Lean 形式化是极其强大的抓 bug 手段，AI agent 让它从「巨大的痛苦」变成可规模化操作。
Eric Jang 转发并称赞了评论区「clanker based correctness」的说法。
「编程与Agent」频道最新
- 让 Agent 自己爬坡优化 SDK：123 次提交后包体积省 33%、内存降 74% — samgoodwin89 · 2026-10-30
- 越来越多开发者出现「Agent 编排综合征」，呼吁离线重启自律 — IanArawjo · 2026-10-30
- 开发者实测：GitHub Copilot 搭载 Opus 5.5 反超 Claude Code — DimitrisPapail · 2026-10-30
- WhatsApp agent 两次因自身计划文件崩溃，作者总结 7 条加载自修复规则 — petrusenko_max · 2026-10-30
- NVIDIA 开源 Nemotron 3.5 检索全家桶:8B Embed/Rerank 加多模态 Parse — NVIDIAAI · 2026-10-30
- 「无限工作机器」:AI 让买卖双方 Bot 互斗,效率提升反增总工作量 — Ididit-forthecookie · 2026-10-30