Kiro 用 Lean 檢查代理底座性質

Back to all postsWe 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.

Why an agent needs more than tests 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 method 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.What a Lean model is 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: Loading code example...And here is its Lean model: Loading code example...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.

Loading code example...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; stalewriterfencedout 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 busytimeout 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