AI 让形式化验证翻身:seL4 曾需 20 人年,如今初创公司号称可用
lemire · x · 2026-10-30
lemire 回顾了形式化验证的历史:从 Dijkstra 1970 年的名言「测试只能证明 bug 存在,不能证明不存在」出发,指出这一路线过去因成本过高而失败——seL4 微内核约 8700 行 C 代码需要约 20 万行 Isabelle 证明、20 人年的验证工作量。
但现在情况在变化:大量初创公司和学术项目宣称 AI 可以让形式化验证变得实用,例如让 AI 证明 C 代码是规格说明的正确实现(包括内存使用等性质)。最明显的应用是密码学与安全关键系统——让 AI 证明系统无法被攻破。
他提醒不要过度兴奋:这些仍是数学模型,处处需要假设。但他本人很期待,计划用形式化方法验证自己一直在用的启发式方法。文中列举的初创公司:
- Truth(2026 年 10 月发布,约 7000 万美元种子轮):打造适用于任何语言的「通用验证机器」
- Harmonic(Aristotle):2026 年 10 月底宣布支持 C 软件与 Verilog 硬件的形式化验证
「编程与Agent」频道最新
- 数据泄漏已波及 648 篇论文，autoarxiv 一键自动复现 arXiv 研究 — pandeyparul · 2026-10-30
- METR 实验：AI 让资深开发者慢 19%，本人却自认快了 20% — srimisra · 2026-10-30
- Clairvoyance 免费工具：把 Claude Code、Codex 等编码 agent 接入日常桌面工作流 — draginol · 2026-10-30
- 同一条提示词：Fabric Apps 版 Claude 报表更好且成本仅五分之一 — adnan_hashmi · 2026-10-30
- 用 Antigravity 插件市场审计 80 页幻灯片，自动对齐文档更新 — rseroter · 2026-10-30
- OpenAI 11 月 9 日办 Cloud Native 黑客松，M5Stack 变身集群桌面警报器 — OpenAIDevs · 2026-10-30