几句 prompt 让 Opus 用 Lean 形式化验证 Agent SDK,产出 16 个修 bug PR
bcherny · x · 2026-09-23
开发者 bcherny 分享了一种用大模型做形式化验证的实操方法:用 Opus 5.5 对 Claude Agent SDK 进行 Lean 形式化建模,仅凭几条简短 prompt 就得到 16 个修复 bug 与竞态条件(race condition)的 PR。
要点:
- 除 Lean 外,TLA+ 同样好用;作者常把两者结合,用于排查数据流、并发与状态管理问题
- 作者自称并不熟悉这两门形式化语言,但 Claude 在两者上都表现出色,等于大幅降低了形式化验证的使用门槛
- 这套思路适合对自己的代码做形式化建模,能发现人工很难注意到的 bug
- 作者顺势抛出讨论:形式化验证会不会成为编程(至少是找 bug)的未来
所属事件:Opus 5.5+Lean 形式化验证 Agent SDK 修出 16 个 bug(19 条相关)→
「编程与Agent」频道最新
- Plurai 推出 Agent 仿真平台：从代码库构建数字孪生自动找故障 — thisguyknowsai · 2026-11-11
- 0xJeff:x402 的真正短板在企业级,大钱在 B2V 而非机器互付 — 0xJeff · 2026-11-11
- 开发者自建 git 网页应用被 Codex 安全护栏误判为网络安全风险 — brianmichel · 2026-11-11
- 形式化验证让 AI 编码更快：Lean 证明成为 agent 优化护栏 — bigdata · 2026-11-11
- Orchestrator v0.14.11 发布：统一管理散落各处的 AI 编程会话 — julianweisser · 2026-11-11
- DeepSeek 开源编码 agent DSH 登上 HF Harness 榜，五项评测并列第一 — TheZachMueller · 2026-11-11