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…