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.

翻译：AI智能体在生成、测试和优化代码方面日益出色。然而，在需要测试无法单独提供的全覆盖形式化保证任务上，它们仍存在不足。分布式系统就是典型例子：读写一致性等性质必须在每种可能的事件交织下成立。机械化形式化验证可以保证这种正确性，但通常需要专家数月甚至数年的努力。证据表明，即使是最先进的编码智能体（Codex搭配GPT-5.4与Claude Code搭配Opus 4.6）仅在7个分布式键值存储规约中成功完成2个。本文提出了首个有效解决这一差距的方法——感应式演绎合成（IDS），该方法联合并增量地合成实现与证明，并从失败尝试中学习以系统性地探索有前景的策略。IDS作为基于智能体的大语言模型系统，平均约6.8小时和每个规约106美元即可达成7/7的成功率，比专家努力快约200倍，比最先进智能体便宜17%。IDS进一步将性能反馈融入同一循环中，生成的实现比已发表的经过验证系统快达3倍。