三年形式化验证实践:从手写 Dafny 到 AI 写 Rust 并自证 Lean 定理
carlk22 · reddit · 2026-09-23
作者记录三年用形式化方法验证 AI 软件算法的演进:2023 年手写 Rust + 手写 Dafny 验证;去年手写 Rust + AI 写 Lean 证明(耗时约三周、数百轮 prompt);今年变为 AI 写 Rust + AI 写 Lean 证明,更难的证明往往几轮 prompt、几分钟内完成。
今年的关键变化:Codex Sol 能写新算法、翻译成 Lean、构造 Lean 可检验的证明,并重构证明以减少 slop;作者仍人工审查翻译并测试 Rust 与被证算法一致。主要工具是 Codex Sol 5.6,由 ChatGPT GPT-5.6 Sol 写 prompt。
结论:这不能解决信任 AI 软件的通用问题,但对能精确定义的算法,形式化验证正成为实用方案的一环。详细经验写成《vibe-coded 算法的九条验证规则》一文。
「编程与Agent」频道最新
- dair-ai 教程:用 Pi 和 Jev 搭自定义 Agent Harness — dair_ai · 2026-09-23
- AI 改 UI 越改越烂?视觉反馈循环是解法 — nikola_mr64990 · 2026-09-23
- 长会话突然变笨?不是模型变差,是上下文里堆满了"垃圾" — ClickOk5811 · 2026-09-23
- API 提取效果比 App 差?问题出在文件预处理而非模型本身 — TangeloOk9486 · 2026-09-23
- 让 AI 复查一个已知并发 bug，它报告一切正常 — cto_junior · 2026-09-23
- 一句「有问题就问我」：邀请 AI 澄清需求产出更好结果 — thisiskp_ · 2026-09-23