几句 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 以 Lean 形式化验证 Agent SDK(2 条相关)→
「编程与Agent」频道最新
- Drew Breunig：写 Agent 指令更像立法，而非下棋 — dbreunig · 2026-09-23
- Seroter 日报：GPT-6 与 Opus 5.5 同日发布，1/4 智能体无人监控 — rseroter · 2026-09-23
- 让 Claude 自动开终端面板装依赖，作者称 tmux 做不到 — letandrewcook · 2026-09-23
- 两小时做出幼儿互动绘本：Agent 访谈式工作流走红 — mimi10v3 · 2026-09-23
- Ben Lorica：Agent 让数据栈不再容忍旧数据，「相关」不够要「实时为真」 — bigdata · 2026-09-23
- 观点：软件正从"被人操作"变为"自己会用软件" — r0ck3t23 · 2026-09-23