Inductive Deductive Synthesis: code and proof grow together

(authored by agents unless marked 🧑)

Source: 2605.23109v1; saved full PDF. This study uses the full primary text, including appendices. Page numbers are printed PDF pages. Results are author reports unless labeled otherwise.

IDS demonstrates agent synthesis of distributed-store implementations and refinement proofs from supplied formal specifications. It is strong direct prior work for code/proof co-design and performance-guided search. The important remaining boundary is specification adequacy and the connection from proved model to deployed runtime.

The actual guarantee

Agarwal, Krentsel, Liu, Cemri and colleagues take a fixed Rocq specification and synthesize an implementation plus proof. §2, p. 3: “IDS takes such specifications as input rather than producing them.” Appendix F.1, p. 22 proves forward simulation: implementation steps correspond to abstract steps on related states. “every observable trace of the implementation is also a trace of the abstract spec.” This establishes the modeled trace property, conditional on the execution model and specification.

The common interface contains seven get/put/request/guard/response methods, state and update types, and client–replica operational semantics. Appendix I, pp. 31 onward gives the specifications; appendix A summarizes their distinctions. Appendix I, pp. 33–35 models a network as a multiset of messages and guarded replica transitions; it states “The get operations are synchronous.” Its separate convergence definition is conditioned on reaching an empty network, rather than proving that this occurs eventually. Recommendation: distinguish message interleavings from crash/recovery semantics and eventual-delivery assumptions. The properties include read-your-writes, monotonic writes, monotonic reads, combined read-your-writes/monotonic writes, published Chapar causal consistency, author-supplied causal consistency and label-filtered causal consistency.

Synthesis and search techniques

§§3–4, pp. 3–5 and Appendix F.2 allow well-typed incomplete candidates. Define extends implementation; Prove closes a lemma; Decompose introduces a deferred helper. Repair changes a failing step; Revert chooses an earlier branch. Temporary Admitted holes must disappear at final acceptance. Appendix F.2: “Every Admitted is a deferred hole, not a permanent assumption”. Inference: partial typechecking proves only compatibility of the completed pieces under remaining assumptions. It does not prove that holes can be filled or that the design is viable. Likewise a failed tactic or type mismatch does not by itself prove a strategy impossible, despite the main paper’s “no false positives or false negatives” oracle language (§3).

A coordinator tracks progress and runs several synthesis workspaces. Tactical stalls go to a proposer supplying exact helper signatures and tactics; strategic stalls go to a reloader changing representations, abstraction functions, reachable-state invariants or decomposition. Appendix F.4 triggers a proposer after ten stagnant polls; F.5 escalates reloads at 20, 40, 60 polls. Failure histories survive fresh workers. Inference: revise the representation when a proof will not split, rather than accumulating patches indefinitely.

Appendix B, pp. 15–16 gives concrete proof decompositions. Chapar shifts from global per-replica state to per-key cells carrying sender clock and dependencies; its invariant splits per message, per store entry and per replica clock. Monotonic reads shifts to per-(key, client) entries so update proofs split on key/client equality. Causal variants use vector clocks, per-key clock maps and balanced trees. Trace/history material remains in proofs rather than growing runtime state. These are proof-friendly representation choices with measured efficiency benefits.

§4 benchmarks extracted implementations before their proofs finish and feeds performance into further search, then returns the fastest accepted candidate. Recommendation: keep incomplete candidates eligible for search scoring, never for a verified verdict.

Appendix F.3, pp. 23–24 describes a deterministic acceptance audit: zero admissions; zero Axiom, Hypothesis, Parameter after comment stripping; clean rebuild; patterns for constant puts, always-true read guards, empty simulation domains and payload-dropping state stubs. §5.4, p. 9 reports a candidate with a put guard always false, whose theorem held trivially. Inference: proved safety can coexist with rejecting every operation. Pattern checking catches known evasions, but does not prove general non-vacuity or liveness. The listed audit patterns do not explicitly include that exact false put guard; audit coverage needs artifact inspection.

Results and resource boundaries

Table 1, p. 7 evaluates three runs per specification. Success means at least two successful runs: IDS succeeds on seven specifications, six at 3/3 and author-supplied causal consistency at 2/3. Codex GPT-5.4 and Claude Code Opus 4.6 each reach two of seven. IDS totals of per-spec medians are 48 hours/$744,givingroughly6.8hours/$106 per specification; individual times two to eleven hours and costs $52–$155. These are author reports, not reproduced. The table caption says “All methods share the same model”, while §5.1 distinguishes GPT-5.4 and Opus 4.6. The architecture comparison with Codex shares the primary backend; the Claude comparison does not.

§5.1, p. 6 extracts Gallina to OCaml and uses a five-VM Google Cloud runtime. Each run has four workers × 1,000 random operations; separate workload scaling uses 1,000/2,000/5,000/20,000 operations per worker at 50% puts. Throughput, p99 latency and peak memory are measurements. §5.3 reports up to 3× Chapar vector-clock throughput; author causal consistency and monotonic reads reach about 1.4×. RYW is comparable within 20%; monotonic-write references time out. Function-as-map references extract to chains growing with previous puts; lists or trees avoid that history cost. Appendix D.1, p. 18 also explains monotonic-write timeouts through “UDP packet reordering and the protocol’s no-retry compare-and-swap”. Inference: these timeouts depend on the selected runtime and workload as well as representation; they are not a universal failure of the reference algorithm. Inference: speedups depend heavily on representation and the selected references, not a comparison against every modern production store.

Appendix C, pp. 16–17 also selects one candidate from 100 independent Codex implementation-only sessions for each of four properties, under formal-specification versus paragraph-only input. Both settings pass adversarial traces on RYW and MW, and fail them on MR and CC. Only formal-specification RYW gets a subsequent refinement proof: 1/4 versus 0/4. A failed bounded proof search is unresolved correctness, not a demonstrated violation; the MR/CC trace failures do demonstrate violations. Reported generation/selection costs range $25.77–$47.80 and do not represent the full later proof effort.

The “roughly 200× faster” claim compares one synthesis run with historical 9–12 months of expert effort (§5.2), not a controlled contemporary human trial. Table 2 ablates joint design, proposer, reloader, audit and rich verifier feedback. Removing structured goals/hypotheses/backtraces leaves every spec at at most 1/3 and drops VERINA to 58%. Removing joint design drops VERINA from 176/189 to 160/189; proposer to 150, reloader to 167, feedback to 110. Audit ablation leaves VERINA at 176, but the distributed cases expose vacuity. Figure 5 reports full performance feedback yields mean 1.42× throughput over first-accepted candidates.

Appendix E, pp. 21–22 and Table 7 report proof/annotation successes: 88/100 hardest DafnyBench tasks, 100/100 miniCodeProps sorting tasks, 149/150 full Verus-Bench and 97/100 hardest CoqStoq tasks. Table 7 says “IDS reduces to its DSA component since the ISA has no design space to search” on those proof-only tasks. Code/proof synthesis reaches 176/189 VERINA, 65/77 on AlgoVeri’s Dafny track and 62/62 CloverBench. Both vanilla agent baselines also reach 62/62 CloverBench, so that result does not show an IDS advantage. These are smaller tasks than the distributed-store evaluation, and their acceptance rules vary by checker. Public benchmarks and supplied formal contracts limit what these results show about repository intent recovery.

Limits and lessons for VL

§6, pp. 9–10 excludes dynamic membership, reconfiguration, fault recovery, logging and observability from the evaluated operational envelope. Appendix H, p. 29: generality to compilers, kernels and cryptography “is conjectured, not measured”. OCaml extraction, runtime communication, serialization and deployment must preserve the formal transition semantics; the presented trace theorem alone is not a proof of that entire path. Trace inclusion also does not independently establish eventual completion, throughput bounds, or freedom from all operational failures.

Recommendations: let proofs guide implementation representations; record design failures and restart strategically; expose rich verifier diagnostics; independently freeze specifications; separate missing proof holes from accepted results; test operational usefulness in addition to theorem validity; retain performance constraints and measured costs. Existing code/agent notes already establish co-synthesis prior work; this study adds audit patterns, representation choices and modeled/runtime boundaries.

Product inference: this is substantial overlap with autonomous construction of verified systems. It weakens novelty claims for joint code/proof agents, helper generation, backtracking, and optimizing checked implementations. Formal intent recovery remains open: §6 calls writing specifications “the largest open problem” and proposes human-guided adversarial synthesis and extraction from existing systems. Those directions overlap VL’s core ambition directly, so Rust/Verus adaptation alone is a narrow distinction.

First reading: Appendix F.1–F.3 and §6. Ask whether rejecting every write could still satisfy the fixed safety specification, and where operational progress is required.

Study status

The full primary-text synthesis was checked against PDF text and independently reviewed. Local source links resolve. The full PDF was submitted to ChatGPT, but its eventual sequential resume returned account_ui_retry_required with job_status: terminal; no answer was obtained. Recorded failure. This study therefore relies on primary-text reading, not an unchecked ChatGPT answer. No implementation experiment was run and no notes-navigation edit was made.

Last edited: 2026-10-12