Boris Cherny 分享用 Claude 与 Lean 形式化验证 Claude Agent SDK 的实际提示词

Boris Cherny 公开了自己用 Claude 配合 Lean 形式化验证 Claude Agent SDK 的实际提示词。被引案例称，作者用 Opus 5.5 通过几个简短提示词产出了 16 个修复 bug 和竞态条件的 PR，并可结合 TLA+ 排查数据流、并发与状态管理问题。