Amazon Kiro 用 Lean 证明自身智能体外壳的性质

Kiro 团队让 Kiro CLI 用 Claude Opus 5.5 在 Lean 4 中为自身 26 个函数建模并证明性质，96 条候选中 70 条被证明、2 条做有界检查、18 条在模型中被证伪并在真实代码上复现。