Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
Shubham Agarwal, Alexander Krentsel, Shu Liu, Mert Cemri and colleagues (UC Berkeley with Google and UC Santa Cruz, including Ion Stoica, Matei Zaharia and Sylvia Ratnasamy) build Inductive Deductive Synthesis, an agentic LLM system that writes a distributed system's implementation and its mechanized correctness proof together, and it completes all seven key-value-store specifications it was given.
Ask this paper
Problem: Coding agents test and refine code, but properties such as read-write consistency must hold under every interleaving of events, which testing cannot cover. Codex with GPT-5.4 and Claude Code with Opus 4.6 complete only 2 of 7 distributed key-value-store specifications.
Method: IDS synthesizes the implementation and the proof jointly and incrementally, and it records failed attempts so that later attempts try different strategies.
Results: All 7 specifications are verified, in about 6.8 hours and $106 per spec on average. That is roughly 200x faster than expert effort and 17% cheaper than the frontier coding agents.
Performance loop: Performance feedback enters the same loop, which produces verified implementations up to 3x faster than previously published verified systems.
Abstract
AI agents increasingly excel at generating, testing, and refining code. However, they fall short on tasks requiring formal guarantees of full coverage that testing alone cannot provide. Distributed systems are a prime example: properties such as consistency between reads and writes must hold under every possible interleaving of events. Mechanized formal verification can guarantee such correctness, but typically demands months to years of expert effort. As evidence, even SOTA coding agents (Codex with GPT-5.4 and Claude Code with Opus 4.6) succeed on only 2/7 distributed key-value-store specifications. In this paper, we present the first effective approach to addressing this gap, Inductive Deductive Synthesis (IDS), which jointly and incrementally synthesizes implementation and proof, and learns from failed attempts to systematically try promising strategies. Built as an agentic LLM system, IDS achieves 7/7 in about 6.8 hours and $106 per spec on average, roughly 200x faster than expert effort and 17% cheaper than SOTA agents. IDS further incorporates performance feedback into the same loop, yielding implementations up to 3x faster than published verified systems.