Kiro proves properties of its own harness in Lean

We built an automated way for Kiro to model parts of its own code in Lean, prove theorems about those models, and check each model against TypeScript / Rust / Python code. We ran it first on Kiro itself. We analyzed 96 candidate properties and observations across models of 26 functions. Lean proved 70 of them, two received finite bounded checks, 18 were falsified in the model and reproduced against the analyzed code, and six produced partial results or observations. This is a demonstration of how Lean-driven verification workflows can be used in a real production setting to verify properties of the agentic harness and to catch hidden bugs.

Our team works on context management for Kiro. The harness around the model decides what enters the context window and how much of it, compacts long conversations, keeps the start of each request stable for the prompt cache, and saves sessions so they can be restored. Around it sit the other harness primitives, e.g. tool calls and their approvals, streaming replies, sub-agents and background tasks. Bugs in this code are hard to catch with tests. They depend on inputs the model chooses, on the order of concurrent events, or on state built up over many turns and potential restarts, and such bugs often fail silently: the LLM simply works from slightly wrong context. So we look for automated ways to examine this infrastructure in depth, find its bugs, and turn them into improvements.

How Kiro checks its own harness. We asked Kiro to prove properties of 26 functions in its own harness. The agent modeled each function in Lean 4, a programming language and proof assistant, checked each model against the real code, and then either proved that the expected behavior holds or found the input that breaks it (by providing a Lean counterexample). We ran it on three Kiro codebases: Kiro agent harness, the CLI client and Kiro Crew. We asked Kiro CLI to scan the codebases and find target functions which are relatively compact so that building a Lean model is feasible and non-trivial to test, so these targets are interesting. It is an early step toward an agent that improves the system it runs in. Lean’s kernel checks every proof, the real code checks every finding, and we reviewed every theorem statement, because the kernel can check a proof misaligned with the source code. The result is a repeatable process that complements tests where the verification path is hard to reach, such as prompt-cache guarantees and concurrency. A proof that passes the Lean kernel provides guarantees for every modeled input, not only the finite set of inputs in unit tests. A failed proof attempt can reveal a concrete counterexample to run against the real code.

What we proved. Across 26 core functions in the Kiro agent server (aka Kiro harness), the Kiro CLI v3 and Kiro Crew, Lean proved 70 statements about models of those functions, each for every modeled input that satisfies the theorem’s stated assumptions. Each model was checked against the real code on sampled inputs (see The method and Limitations). For example:

• Removing duplicate file attachments never changes what the model saw on an earlier turn, so that step cannot break the prompt-cache prefix as the conversation grows.
• Combining a sub-agent’s permission decision with its parent’s never yields more permission than the parent’s, and tightening a policy never turns a refusal into an approval.
• Once a task in Kiro Crew’s queue is handed to a new worker, no fenced write from the old worker can change it, assuming each store call runs as one indivisible step.

What we found. Where a proof failed, it often led us to an edge case the tests had not reached, usually at a boundary between two representations or two programs, or in a rare order of concurrent events. We counted a failed proof as a finding only after reproducing it on the real, unmodified code.

Ordinary test suites, whether written by people or generated by an LLM, check the inputs someone thought of or a generator produced, can’t catch all corner cases. In an agent, most inputs come from the model and the files it reads, so they reach far more cases than anyone writes into a test. The code that handles them is often small and looks obviously correct: a truncation, a read-only check, an allowlist match. That is where a proof helps most. Such functions are short enough to model exactly, the code intent is precise enough to state as theorems, and they run in every session. Ordinary non-exhaustive test suites sample behavior; a proof establishes a universal result for the formal model. The proof is about the model, though, so we still need tests to tie the model to the code, as described below.

Across the agent server, the CLI and Kiro Crew, the harness rests on a few kinds of properties that non-exhaustive tests can only sample:

• Bounded content. Every piece of content that enters the model’s context window has a size cap, and when content is cut the agent can retrieve the rest.
• Persistence. Reloading a session, even after a restart, gives the model exactly the messages it saw live.
• Prompt caching. The start of each request (the tool list, the first message and the history) stays the same from one turn to the next, so the model provider can reuse its cached work.
• Permissions. An approval covers exactly what you approved, and a sub-agent never gets more permission than its parent.
• Ordering. Sessions, streamed replies and background tasks end in the right state whatever order their events arrive in.
• Cross-repo contracts. Where two codebases depend on each other, they must establish cross-repo contracts. For example, Crew translates one tool allowlist for both the agent server and the CLI, and the CLI must keep an update from the agent server at the start of the session. Usually each repository’s tests only check the code in its own repository; a Lean model can include both sides and prove they match.

Each is a statement about all inputs, all sessions or all orders of events. That is the form a theorem takes, and the form non-exhaustive tests can only sample.

The work was done by Kiro itself: the Kiro CLI, using Claude Opus 5.5 served by Amazon Bedrock and a set of Lean 4 skills. The agent found the targets, wrote the Lean models, the proofs, the differential tests and the reproduction scripts, small programs that run a counterexample against the real, unmodified code. Lean checks the generated proofs independently of the agent. Connecting those proofs to the production code still depends on the accuracy of the models, theorem statements and differential-test harnesses, which we reviewed and tested separately. We set the scope, choosing the repositories and the areas to target, and reviewed the theorem statements and the findings as they came in. Each theorem restates a code intent as a formal statement (the code intent is derived from the documentation or design invariants, and every finding is confirmed on the real code). We used the Lean 4.28.0 distribution only, with no external Lake dependencies such as Mathlib. The agent server is the shared harness behind the Kiro IDE, web and CLI v3 (One agent, every surface), and the CLI results apply to the Kiro CLI v3. We analyzed the agent server and the Kiro CLI in their private repositories, and Kiro Crew at commit 909e0fc of its public repository. The numbers in this post are internal experimental results reviewed by the Kiro team.

Because an agent wrote the proofs, we also checked for the ways Lean can accept a semantically similar proof target that is missing the code intent: an unfinished step, an extra axiom, or assumptions that can never all hold. We listed the axioms behind every theorem, ten counterexamples behind five of the findings, and one control case for one of those findings. A theorem whose assumptions contradict each other holds trivially (it is vacuous) and thus is not useful. For every theorem this post quotes or describes, we gave a concrete input that satisfies all of its assumptions, checked in Lean, so the assumptions of each are jointly satisfiable.

A Lean model is a second implementation of a function, written in Lean. It represents the source’s inputs and observable outputs through an explicit encoding, and it is written so that Lean can reason about it. The theorems talk about the model, not about the source code: Lean cannot read Python, TypeScript or Rust. So, under that encoding, the model has to compute what the source computes, and it has to be simple enough to prove things about.

Here is an example from Kiro Crew’s task queue where concurrency issues might arise. The queue keeps one row per task in SQLite, and many dispatchers, run loops and callbacks call it at the same time. Two dispatchers can try to take the same task at the same moment, and only one may win. claim decides that with one guarded UPDATE, run under the store’s lock and inside a transaction. This is the core of it in taskq/store.py:

And here is its Lean model:

The risk is a task that runs twice. Two dispatchers can see the same queued task at the same moment and both call claim to take it. If both calls succeeded, two agents would do the same work, and anything the task changes outside Kiro would change twice. The Lean theorem below rules this out. It says that right after one dispatcher’s claim call succeeds, the task is admitted (taken and about to start), and a claim call from any other dispatcher, at any time, is refused. Only a later write that puts the task back in the queue, such as scheduling a retry, makes it available again.

The theorem is deliberately small. It follows from the guard in claim and from admitted not being a claimable state. Its value is not the difficulty of the proof but that the guard it relies on is the one the differential tests matched against the real SQL. It speaks about the row right after a successful claim; stale_writer_fenced_out below covers what happens across later calls. It covers concurrency only through an assumption: each successful transaction is one atomic state transition. Under that assumption, two claim calls cannot both succeed on the same claimable row. A competing connection may instead get a lock error: BEGIN IMMEDIATE waits up to the store’s busy_timeout and then fails, and claim raises TaskStoreUnavailable. Retries, availability and that error path are outside this theorem. A Crew gateway takes a file lock on its home directory, so a second gateway cannot write the same database. Another process, such as a manual sqlite3 session, still could, and between processes only SQLite’s write lock provides this. Lean does not check that assumption.

The model differs from the source in a few ways. It is a pure function: state goes in and the new state comes out. The model considers sequences of calls, treating each store operation as one indivisible step. That is an assumption about the store, not something Lean proves: it relies on the store’s lock within a process and on SQLite’s transactions across processes. It represents data exactly where a bug could hide, such as times, string encodings and byte limits. And it compiles to an ordinary program, so we can run it against the real code.

A model is useful only if it does what the source code does. Each model starts with a header giving the source file and line numbers, so a reviewer can compare the two side by side. We did not rely on that review alone: every model was run against the real code on thousands of random inputs, and we fixed the model until no output differed (step 3 below). A theorem then holds for the model on every modeled input that meets its assumptions. The differential test is evidence, not proof, that the model and the source agree: it shows they agree on every input we tried, and it is only as strong as the inputs we generated.

This leaves the usual gap between a model and its code: the proof covers every modeled input that meets its assumptions, while the match between model and code is checked on about 100,000 sampled inputs. Three things keep that gap small here. The functions are short, the models keep the structure of the source code, and the generators aim at the inputs where these functions break, such as multi-byte text, lengths at a cap and reordered events. As a check on the tests themselves, we changed one behavior on the real-code side for two of the trackers, and the differential tests reported hundreds of mismatches.

We followed the same steps in each repository. Figure 1 shows the whole flow, including the two places where a mismatch sends us back to fix the model.

1. Find targets. We pointed the Kiro CLI at each repository (Kiro harness, Kiro CLI and Kiro Crew) and asked it to find functions that make a statement about the code as a theorem: a size cap, an approval rule, a reload that must match the live session, a state machine that must never go backwards. The scan read doc comments, design invariants and call sites, and produced a ranked list of targets with the source file and line of each. The model describes what the code does, the theorem states the behavior it should satisfy.

2. Model. The agent wrote a Lean model of each function, as described above, keeping the structure of the original so a reviewer can compare them line by line.

3. Check the model against the real code. A proof about the wrong model proves nothing, so before proving anything we compiled each Lean model to an executable and ran it side by side with the real implementation on thousands of random inputs: TypeScript through Node or Bun, Rust through a small binary linked against the real crate, Python by importing the real module. Inputs ranged from random strings and random sequences of calls to shell commands run against real bash and git, and the generators aimed at boundaries: multi-byte and CJK text, lengths just below and above each cap, shuffled and repeated event orders, and floods past the 64-update limit of the CLI’s session-start hold. When outputs differed, we checked which side was wrong and fixed the model where it was. The final runs, 97,938 cases across the three codebases, had no mismatches.

4. Prove. We stated each target code intent as a theorem and proved it. A stuck proof might be due to multiple reasons: the theorem may be false, the model may be wrong, or the proof may be incomplete. We investigated each stuck proof, and when the goal it got stuck on pointed at an input that breaks the expected behavior, we proved a theorem bug_… stating that a specific input violates the expected code behavior in the model, so the counterexample itself is checked in Lean. For two properties we wrote a bounded check instead of a proof (these properties relied on external software and thus it was not possible to faithfully model in Lean). A bounded check covers every input up to the bound, or every case in a fixed list, and nothing beyond. That is why the two bounded checks in Table 1 are counted separately and not as proved.

5. Reproduce. A counterexample counted as a finding only when a script that runs the real, unmodified code showed the same result. Then we checked whether real callers can reach that input, and worked out what a user would see when it happens.

For most findings we went one step further: we wrote the fix in Lean and proved it closes the gap without changing the behavior the code is meant to keep. This proves the fixed model correct; the code change that implements the fix needs its own differential test before the proof says anything about it.

Table 1. Verification results and supporting checks for the Kiro harness, the Kiro CLI and Kiro Crew. In each row, Properties is the sum of the four outcome columns. Proved counts properties proved for every modeled input that satisfies the theorem’s stated assumptions. Bounded check counts properties checked on every case up to a size bound, or on a fixed list of cases; they are not counted as proved. Partial or observation counts properties proved only in part and observations about the code that is not reachable. Lean theorems include the lemmas the proofs need; test cases are the generated inputs of the differential tests: one input for a pure function, or one random call sequence for a stateful one.

Lean proved 70 of the 96 properties, each for every modeled input that satisfies the theorem’s stated assumptions (remaining properties resulted in a discovered bug or a partial finding / observation). These are the ones we find most useful, because each one depends on many inputs or on the order of events, which is where tests are thinnest.

Removing duplicate files keeps the request prefix. When the same file is attached more than once, Kiro harness keeps only one copy of its contents before sending the request. If that step changed earlier messages as the conversation grew, every turn would change the reusable prefix, which can prevent cache reuse. We proved that for any history xs and any new messages ys, the result for xs followed by ys starts with the result for xs. So this step never rewrites what the model saw on the turn before, for any number of files, in any order. The theorem covers deduplication only; the request prefix also depends on the other steps that build the request.

History survives edits and reloads. Kiro harness keeps deleted and reverted messages in the session file and resolves them when it builds the history. We proved that resolving twice gives the same result as resolving once, that the result only drops messages and never reorders them, and that a forked session always starts with the effective history of its parent. After a reload, every tool card ends in the status the user saw live, for all eight tool call states (waiting for approval, running, success, accepted, error, handled error, canceled and rejected).

Cut output never goes over its cap. The CLI’s agent cuts shell command output and other tool results to a byte limit before they enter the context window. We proved that the cut text is never longer than the limit in UTF-8 bytes, for any valid UTF-8 string, including when a truncation notice is appended (a notice longer than the limit is itself cut to fit), and that without a notice it keeps the longest prefix that fits without splitting a character. The model matched the real Rust functions on about 4,000 cases of multi-byte text.

Session status holds up when events finish out of order. Kiro harness tells clients whether a session is busy, waiting for the user or idle, including the background workflows it started. Workflow events are processed by separate asynchronous chains that can finish in any order, and the tracker uses a sequence number to put them back in order. We proved that for the events that start, pause and finish a run, every delivery order gives the same status as the original order. The proof covers every permutation, not a sample. We checked the model against the real tracker on 6,000 random event sequences, most of them delivered out of order.

A sub-agent is never less restricted than its parent. When Kiro harness starts a sub-agent, it combines the sub-agent’s own permission decision with its parent’s. We proved that the result is always one of the two decisions and always the more restrictive of them, and that a deny or an explicit ask from the sub-agent is never weakened. So, through this step, a sub-agent cannot approve a tool call that its parent would refuse or ask about, whatever the two policies say. We also proved that tightening a policy never turns a refusal into an approval, where tightening means the decision becomes at least as restrictive in the order allow, ask, explicit ask, deny, and that a normalized absolute path can’t climb above its root with ...

One allowlist, two backends. Crew lets users write tool allowlists in the CLI’s allowedTools format and translates them into Kiro harness policy patterns. We modeled all three matchers (Crew’s translation, Kiro harness’s policy matcher and the CLI’s glob matcher), checked each model against the real code, and proved that the translation never grants more on harness than the CLI would, for any entry without a backslash (kas_le_cli). An entry with a backslash can grant more on Kiro harness; that is one of the three Crew findings, and we proved a fix that refuses such entries.

Model fallback stops. When a model refuses a request, the CLI’s fallback logic switches to another model. We proved it never switches more than three times in one turn and never switches to a model already tried in that turn, for any sequence of refusals and calls.

Two dispatchers never take the same task. When several dispatchers race for one queued task, only one claim call can succeed. Right after it, the task is admitted, and a claim call from any other dispatcher is refused (claim_exclusive, the theorem in the example above). The model treats each store call as one indivisible step, as the store’s lock makes it, so under that assumption no two claim calls succeed on the same claimable row, in any order; a competing call may instead fail with a lock error, which the theorem does not cover.

The task queue fences out stale workers. Kiro Crew’s task queue moves each task through 15 states, from queued through running and the waits to done, failed or cancelled. Every successful claim call increases the row’s generation, and the writes a worker makes afterwards name the generation it holds. We proved, for any sequence of calls, that the generation never goes down, so once the task has been taken by a new worker, no fenced write from the old worker can change the row:

The model matched the real store, running on SQLite, on 4,500 random sequences with about 20,000 calls in total. Those sequences ran one call at a time, so they test the logic of each call, not the store’s concurrency; the claim about concurrent workers rests on the atomicity assumption above.

Eighteen code intents were falsified in the model, and for each we reproduced the counterexample on the analyzed code (for the session-start race, at module level). Edge cases like these are normal in code of this size. When we searched the CLI’s and Kiro Crew’s GitHub issues and the agent server’s pull requests on October 1, 2026, no open issue matched any of them, though one open agent-server pull request would fix one finding and another described part of one. Each one needs an unusual input or a particular timing. Several fail safely: the user is asked again, or the model sees a little more or less text than intended. For most of them we also proved a fix in Lean.

Let’s look at the concrete concurrency bug discovered in the Kiro Crew codebase.

A cancelled job that runs anyway, see PR 25130. Kiro Crew can run a job once at a set time, and the user can cancel it while it runs. The code intent is that a cancelled “one-shot” job never re-runs again. Here is the flow that breaks this behavior. If the user clicks Cancel run while the job is still waiting to start its work, Cancel stops the run but leaves the job switched on, so the scheduler runs it again seconds later and the release notes are posted anyway. Tests miss this because the cancel has to land in the brief moment before the job’s work begins. Lean found it as a counterexample: a sequence of ten events in the model of the job’s lifecycle that ends with the job’s work having run after the cancel. We reproduced the sequence on the real scheduler. The fix is one condition in Cancel, and with it Lean proves that no sequence of events runs a cancelled job again.

The main groups of other discovered bugs are:

• A concurrency race. Two sessions starting at the same time can interfere: if another session registers with the CLI while session/new is in flight, an update sent during session start, such as a tool call from a session-start hook, can be dropped. Races like this are hard to catch with tests, because a test runs one order of events and the bug appears only in another. In Lean we stated the theorem over every sequence of session-start events in the model, for any number of sessions. The proof did not go through, and we wrote the interleaving that drops the update as a bug_… theorem checked in Lean. We then replayed that interleaving on the CLI’s real code that holds and replays session updates, imported unchanged and connected to a copy of the client’s handler table. This is a module-level reproduction, not an end-to-end reproduction in the running CLI.
• Caps measured in the wrong unit. Seven of the nine Kiro harness findings are in the functions that cut text to fit a cap. web_fetch has a budget in bytes but cuts the page by JavaScript string length, which counts UTF-16 code units, keeping half as many code units as the budget has bytes. That assumes each code unit takes at most two bytes in UTF-8. A Chinese or Japanese character is one code unit but three bytes in UTF-8, so such a page can come back up to 1.5 times the cap. The default mode also does not say a page was cut. A cut counted in UTF-16 code units can split an emoji at the very end of the text. grep_search shortens match lines but not context lines, so one very long context line, for example from a minified file, can push the matches out of the capped result. Nothing fails in these cases; the model sees somewhat more or less text than intended.
• Very large command output. A shell command, hook or workflow step that prints more than 2^29 − 24 UTF-16 code units of output (about 512 MiB of ASCII text) exceeds the longest string V8 can build in the build we tested (Node 26.3.0 with V8 14.6, on macOS arm64), and harness runs on Node, which uses V8. Kiro harness collects the output into one string before its size caps run, so the error comes before the cap. Nothing catches it, and Kiro harness’s handler for uncaught errors exits the process, ending its open sessions. Kiro harness’s collector for background terminals already keeps only the most recent output, and we proved it can never reach that limit (tail_join_safe), so the fix is to use it for every command.
• Spec rules after a cold reload. In spec mode the live path and the reload path attach implicit rules to different messages, so a turn after a cold reload differs slightly from the request the live session would have sent and changes the reusable prefix once, which can prevent cache reuse for that turn.
• Glob characters in an approved path. The CLI turns an “always allow” path into a glob pattern without escaping it. For a Next.js route such as app/[slug]/page.tsx this means you are asked again about the file you approved, and a different path such as app/s/page.tsx is approved as well. We proved the fix in the model: escape the path first, and the grant then matches exactly the approved path and the files under it, while ordinary paths are unchanged.

Two more code intents did not hold either, but we found no reachable production call path to the input that breaks them. That is why we count them as observations rather than findings. These are two observations about Kiro harness in Table 1 and are not counted among the eighteen. None of the bugs in any of the three codebases were security findings.

Proofs fit the harness well. Context management, permissions and the state machines around them make short, exact theorems: the same prefix next turn, the same request after reload, an approval that covers exactly one file, a result that holds in any order of events. The functions behind them are small and translate into Lean directly. Most of the proved properties and fifteen of the eighteen findings are in these areas, and most findings sit at a boundary between two representations, such as UTF-16 and UTF-8, or a file path and a glob. Writing both sides down in one language showed where they disagree.

The differential test matters as much as the proof. Differential tests helped us find and fix errors in Lean models. When Lean couldn’t complete a proof, the remaining goal often revealed the input causing the failure. We then proved that the fix satisfied the intended behavior, not just that specific input.

A proof establishes a property of the Lean model, under the model’s definitions and assumptions. How much that tells us about the real system depends on things the proof does not check by itself:

• The model must match what the code does. The agent wrote each model from the source, and a model can miss something the code does. Differential tests check the model against the real code, but only on sampled inputs, so a difference on an input we never generated would go unnoticed. Some models also rest on a stated assumption, such as the task queue treating each store call as one indivisible step.
• The theorem must state what the code should do. The agent wrote each theorem from doc comments, design invariants and call sites, and we reviewed them. If a theorem leaves out part of the intended behavior, a bug can escape even when the proof succeeds.
• The model’s types must be faithful. Where a model uses Lean’s unbounded natural numbers or abstracts a data structure, it does not capture overflow, floating-point behavior or the cost of an operation. We modeled exact representations where the precise statement about code behavior (theorem or lemma) depends on them, such as UTF-8 and UTF-16 lengths.
• The trusted base is larger than the kernel. The proofs depend on Lean’s kernel. The differential tests also depend on the Lean compiler, the harness that feeds both sides the same inputs, and the runtimes of the real code. The 17 theorems that use native_decide also trust the Lean compiler and the C toolchain it builds with. None of them backs a proved property: they are bounded checks, counterexamples and one control case, and every counterexample was also reproduced on the real code.
• Results are tied to a commit. Each model describes the code at the commit we analyzed. A later change to the code is not covered until the model is updated and the differential tests pass again.

These problems are well known in autoformalization, where the main difficulty is making sure a Lean statement faithfully captures the original, whether a mathematical claim in natural language or code in another programming language. For the findings, the real code settles the question: we replayed each counterexample against it, and a failure there confirms the bug independently of the model. We considered the differential tests and our review of the theorem statements sufficient evidence to trust the proofs. We aimed the method at 26 functions where it pays off: small, compact statements and mostly on a boundary between two representations. We judged whether each finding is reachable from the code that calls it.

Kiro’s context management rests on harness properties such as content in the context window is bounded, a reloaded session remains unchanged, and the prompt caching is intact throughout the trajectory. Until now these assumptions lived in design documents and in unit tests. For the functions in this post they are now theorems about Lean models, each tied to the real code by differential tests on sampled inputs. That covers those functions at the commits we analyzed, not the whole harness.

That gives our roadmap a foundation. We plan to state each one as a theorem while the feature is designed, and to rerun the differential tests whenever the code changes, to help catch regressions before review. The steps are automated, but every theorem statement and finding still needs a person to review it, so extending the checks to other Kiro repositories depends on review effort as well as compute. The goal is that more of the harness’s core behavior becomes proven rather than assumed.

To get started with Lean, see Lean’s documentation. To learn more about how the Kiro agent harness works, read One agent, every surface, and download Kiro to try it on your own codebase.