A coordination framework for formal proof development with Kiro | Amazon Web Services

Large language models (LLMs) and coding agents are increasingly capable of proving difficult mathematical theorems and completing formally verified Lean programs. Yet, existing agentic provers rely on the backend models’ capabilities while lacking the ability to explore when they get stuck: when a proof resembles patterns the model already knows, it might succeed quickly. When it doesn’t, the model can spend thousands of tokens repeating failed tactics, lose track of intermediate results, or abandon the proof altogether.

We develop a prover harness, MAESTRO, in Kiro CLI that gives LLMs a systematic framework for exploring, decomposing, and making structured progress on difficult problems. The prover constructs a shared proof skeleton and organizes the work across specialized agents that explore independent proof obligations concurrently. A persistent coordinator evaluates their feedback, repairs broken proof structure, and decomposes difficult goals into smaller…