AI Learns to Write Formally Verified Code: The IDS Framework Explained

Forum topic · QianXun · 2026-05-25

Summary

A Chinese tech forum post discusses a May 2026 arXiv paper titled 'Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems' (arXiv:2605.23109) by Shubham Agarwal et al. from the University of Washington and Stellaris AI. The paper introduces IDS, a dual-agent framework that generates formally verified systems up to 200x faster than human experts. The framework combines a Deductive Synthesis Agent (DSA), which decomposes goals and iteratively writes machine-checked mathematical proofs using the Rocq (Coq) proof assistant, and an Inductive Synthesis Agent (ISA), which observes failures and synthesizes higher-level strategies. Reported results: IDS completed 7/7 distributed key-value store tasks versus 2/7 for a top general model, produced verified code in 6.8 hours at about $106 (work that takes humans months), and generated code up to 3x faster than previously published verified systems. The post also raises open questions about reliance on initial synthesis strategies, computational costs at the scale of OS kernels, and limits of automated proof tools.

This post from zhichai.net introduces a recent paper on AI-driven formal verification, framed around the idea of 'zero-defect' software.

What formal verification is

Formal verification uses rigorous mathematical proof to show a system is correct in all possible situations — not just tested ones. For distributed systems (thousands of servers keeping data in sync), this is described as nearly the only reliable approach. The catch: humans write provably-correct code extremely slowly, sometimes months per small module.

The paper

The proposed IDS framework reportedly lets AI write formally verified systems up to 200x faster than human experts.

How it works: two cooperating agents

1. Deductive Synthesis Agent (DSA) — the rigorous builder. It decomposes a large goal into small components, writes a mathematical proof for each, and uses Rocq (Coq) as a machine-checked oracle. Any proof gap causes rejection, and DSA iterates until the component is mathematically airtight.

2. Inductive Synthesis Agent (ISA) — the strategist. It monitors DSA: when it gets stuck in one place, or produces correct-but-slow code, ISA analyzes prior failures and proposes a new overall architecture/strategy. This ability to generalize from local failures is the 'inductive' part.

Reported results

Outperforming top models: On a hard distributed key-value store challenge, the strongest general model (GPT-5.5 preview) completed only 2/7 tasks, while IDS achieved 7/7.
Efficiency: Work that takes human experts months was done in 6.8 hours at a cost of about $106.
Performance: By incorporating performance feedback into the loop, generated code ran up to 3x faster than the best previously published verified systems.

Open questions raised by the post

1. Dependence on initial intuition — IDS relies heavily on the first synthesis strategy; whether ISA can escape a dead end when the correct path is entirely outside the AI's initial search space remains unclear, and tested tasks stay within the distributed-systems domain. 2. Cost of certainty — massive proof search and trial-and-error may not scale linearly to multi-million-line systems like OS kernels. 3. Limits of the prover — if a proof lies beyond current automated proof theory even in Rocq, the AI may hit the same walls as humans.

Takeaway

The author's conclusion: AI is shifting from a 'probabilistic imitator' to a 'guardian of logic.' IDS suggests a path toward software that is mathematically guaranteed not to fail or contain exploitable logic flaws — though the above limitations mean this is a promising direction, not a solved problem.