Kiro's team says it modeled 26 functions of its own agent harness in Lean, proved 70 properties and reproduced 18 bugs on the real code

The authors had the Kiro CLI agent, running Claude Opus 5.5 on Amazon Bedrock, write Lean 4 models of 26 functions across three codebases: the Kiro agent harness, the CLI client and Kiro Crew. The agent then wrote proofs and differential tests that run each model against the real TypeScript, Rust or Python code. Of 96 candidate properties, Lean proved 70, two got bounded checks, 18 were falsified in the model and reproduced on the analyzed code, and six were partial or observations. The final differential runs covered 97,938 cases with no mismatches.

Two of the proved properties: a sub-agent's combined permission decision is never more permissive than its parent's, and truncated tool output never exceeds its byte cap. Among the bugs, the agent server's web fetch tool budgets in bytes but cuts by JavaScript string length, so a page of Chinese or Japanese text can come back up to 1.5 times the cap. In Kiro Crew, cancelling a one-shot job in the moment before its work begins leaves the job switched on, so the scheduler runs it again (PR 25130). The authors say none of the bugs were security findings.

These are the team's internal results. The agent server and CLI repositories are private, and only Kiro Crew, at commit 909e0fc, is public. The authors state that a proof covers the model, not the code, and that their differential tests are sampled evidence of a match. The code listings and Figure 1 did not load in our read of the page.

Why it matters: The pairing is the part that transfers. A proof about a model tells you little until a differential test ties it to the code, and most of the bugs here sat where two representations meet, such as UTF-16 against UTF-8 or a file path against a glob. If your harness enforces byte caps, permission inheritance or a stable cache prefix, those are the short functions this method can check.