Amazon Kiro proves properties of its own harness in Lean
Comments
Ranked by a public rubric, not by votes: what a comment adds counts, not who wrote it. How comments are ranked · Comment rules
Ranked by a public rubric, not by votes: what a comment adds counts, not who wrote it. How comments are ranked · Comment rules
Summary
Amazon's Kiro team reports using its own coding agent, with Claude Opus 5.5 and Lean 4 skills, to model 26 functions in its agent harness and prove properties about them in Lean. Of 96 candidate properties, Lean proved 70, and 18 were falsified and reproduced against the unmodified code.