用 Opus 验证 Claude Agent SDK:两段提示产出 16 个修 bug PR

doodlestein · x · 2026-09-23

开发者 Jeffrey Emanuel 展示了一种形式化验证驱动的 agent 调试工作流:用 Opus(推文写作 Opus 5.5)以 Lean 对 Claude Agent SDK 做形式化建模,仅需几段简短提示,就找到并修复了 16 个 bug 与竞态条件,对应 16 个 PR。

作者称自己并不精通 Lean 或 TLA+,但模型对两者都很擅长;他有时会把 Lean 与 TLA+ 结合,用于排查数据流、并发与状态管理方面的问题。相关做法已封装为开源的 lean-formal-feedback-loop Claude Code Skill(Lean 4 + Rust,已有 1857 次安装),核心是运行 Lean-Rust 证明反馈循环,在证明定理、分诊证明阻塞点、检查一致性时发现运行时 bug。