Amazon Kiro 用 Lean 形式化验证自身代码，证实 70 项属性并发现 18 个漏洞
来源标题：Amazon Kiro proves properties of its own harness in Lean
Amazon Kiro 团队构建了一套自动化流程，将自身部分代码建模为 Lean 形式化模型、证明定理，并对照 TypeScript/Rust/Python 实际代码校验。首次对自身 26 个函数的 96 项候选属性进行分析，Lean 成功证明 70 项，18 项在模型中被证伪并在实际代码中复现，另有 2 项做了有限范围检查。该演示表明 Lean 驱动的验证流程可用于生产环境，验证智能体运行框架（harness）的属性并捕获隐藏缺陷。
以下正文由 AI 翻译自 Hacker News 最新（原文版权归原站所有），可能存在偏差，重要内容请以原文为准。
我们为Kiro构建了一种自动化方法，使其能够在Lean中对自己的部分代码进行建模，证明关于这些模型的定理，并对照TypeScript / Rust / Python代码检查每个模型。我们首先在Kiro自身上运行了这套方法。我们分析了26个函数的模型中的96个候选属性和观察项。Lean证明了其中70个，两个接受了有限有界检查，18个在模型中被证伪并在被分析的代码上复现，六个产生了部分结果或观察。这展示了Lean驱动的验证工作流如何在真实生产环境中用于验证agentic harness的属性并捕获隐藏的bug。
我们团队负责Kiro的上下文管理。模型周围的harness决定什么进入上下文窗口以及进入多少、压缩长对话、保持每个请求的开头对prompt缓存稳定，并保存会话以便恢复。围绕它的还有其他harness原语，例如工具调用及其审批、流式回复、子代理和后台任务。这类代码中的bug很难用测试捕获。它们依赖于模型选择的输入、并发事件的顺序，或跨多轮及潜在重启累积的状态，而且这类bug往往静默失败：LLM只是基于略微错误的上下文工作。因此我们寻找自动化方式来深入检查这一基础设施，发现其bug，并将其转化为改进。
Kiro如何检查自己的harness。我们要求Kiro证明其自身harness中26个函数的属性。该代理在Lean 4（一种编程语言和证明助手）中为每个函数建模，对照真实代码检查每个模型，然后要么证明预期行为成立，要么找到打破它的输入（通过提供Lean反例）。我们在三个Kiro代码库上运行了它：Kiro agent harness、CLI客户端和Kiro Crew。我们要求Kiro CLI扫描代码库并找到相对紧凑的目标函数，以便构建Lean模型可行且测试非平凡，因此这些目标是有意义的。这是迈向一个能改进其所运行系统的代理的早期一步。Lean的内核检查每个证明，真实代码检查每个发现，而我们审查了每条定理陈述，因为内核可以检查一个与源代码不一致的证明。结果是一个可重复的过程，补充了验证路径难以到达的测试，例如prompt缓存保证和并发。通过Lean内核的证明为每个建模输入提供保证，而不仅仅是单元测试中的有限输入集。失败的证明尝试可以揭示一个具体反例，用于对真实代码运行。
我们证明了什么。在Kiro agent server（又名Kiro harness）、Kiro CLI v3和Kiro Crew的26个核心函数中，Lean证明了关于这些函数模型的70条陈述，每条陈述对于满足定理所述假设的每个建模输入都成立。每个模型都在采样输入上对照真实代码进行了检查（见方法和局限性）。例如：
我们发现了什么。在证明失败的地方，它常常引导我们到达测试未曾触及的边缘情况，通常是在两个表示或两个程序之间的边界处，或在罕见的并发事件顺序中。我们只有在真实、未修改的代码上复现失败证明后，才将其计为一个发现。
普通测试套件，无论是人写的还是LLM生成的，检查的是某人想到的或生成器产生的输入，无法捕获所有角落情况。在代理中，大多数输入来自模型及其读取的文件，因此它们到达的情况远多于任何人写入测试的情况。处理它们的代码往往很小，看起来明显正确：一个截断、一个只读检查、一个允许列表匹配。这正是证明最有帮助的地方。这类函数足够短，可以精确建模；代码意图足够精确，可以表述为定理；而且它们在每个会话中运行。普通的非穷尽测试套件采样行为；证明为形式模型建立普遍结果。不过，证明是关于模型的，所以我们仍然需要测试将模型与代码联系起来，如下所述。
在agent server、CLI和Kiro Crew中，harness依赖于几种非穷尽测试只能采样的属性：
每一条都是关于所有输入、所有会话或所有事件顺序的陈述。这就是定理采取的形式，也是非穷尽测试只能采样的形式。
这项工作由Kiro自己完成：Kiro CLI，使用由Amazon Bedrock提供的Claude Opus 5.5以及一组Lean 4技能。该代理找到了目标，编写了Lean模型、证明、差分测试和复现脚本——即对真实、未修改代码运行反例的小程序。Lean独立于代理检查生成的证明。将这些证明与生产代码连接仍然依赖于模型、定理陈述和差分测试harness的准确性，我们单独审查和测试了这些。我们设定了范围，选择要针对的仓库和领域，并在定理陈述和发现出现时进行审查。每条定理都将代码意图重述为形式陈述（代码意图源自文档或设计不变量，每个发现都在真实代码上确认）。我们仅使用Lean 4.28.0发行版，没有外部Lake依赖，如Mathlib。agent server是Kiro IDE、web和CLI v3背后的共享harness（一个代理，每个界面），CLI结果适用于Kiro CLI v3。我们在其私有仓库中分析了agent server和Kiro CLI，并在其公共仓库的提交909e0fc处分析了Kiro Crew。本文中的数字是经Kiro团队审查的内部实验结果。
（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）
正文由 探How 从来源站点 RSS 同步，内容未经改写；遇到排版缺失或需要图片、视频时请以原文为准。