Boris Cherny 用 Opus 5.5 结合 Lean 形式化验证 Claude Agent SDK
Anthropic 的 Boris Cherny 拿 Opus 5.5 写 Lean 验证 Claude Agent SDK，几条提示词修出 16 个 bug，并发代码排查可以抄这个思路。
#TLA+
共 2 条 · 7 天 0 条 · 30 天 1 条
信息流里打上「TLA+」标签的资讯、产品与论文，按刊登时间排，新的在上。
9月23日
6月5日
LLM写TLA+规范：最高语义正确率仅8.6%
形式化验证团队终于有了LLM能力的基准数据——当前模型无法可靠生成TLA+规范，但渐进式提示和推理对齐是突破口，做形式化方法或分布式系统验证的开发者值得关注。