Inductive Deductive Synthesis: Enabling AI to

Generate Formally Verified Systems

https://arxiv.org/pdf/2605.23109

This paper is pretty cool.

They more-or-less use a proof checker (Rocq, a successor to Coq) as a tool in their agent loop during implementation, instead of turning to verification only at the end. The proof-checker generates structured output clarifying bugs in each stage of the implemenation (rather like a compiler in an ordinary coding assistant), which gets fed back into the prompt for the next stage of the agent-loop.

They use an analogy to chain-of-thought, except the intermediate states are formally verified, with “holes/need to fill this gap” output from the proof assistant rather than just plausible-sounding text inserted into the prompt for the next pass.

One still has to generate a Rocq spec as input — abstract data types, operation signatures, and axioms that specify the behavior of those operations (post-conditions, basically), but then the system produces a verified implementation prototype in Ocaml.

They are looking at using Verus, instead of Rocq as the proof assistant back end, which would produce Rust instead of Ocaml.

#formalverification
#distributedsystems
#rocq #ai #codeassistant

Current status: starting reading chapter 7 of Software Foundation, with #Rocq

So far, I managed to do all the exercises.

Amazing how much *doing*, as compared to only *reading*, helps the learning process.

**Rocq’n’Share 2026**
**Jun 29–Jul 3, EPFL**
Registration free but required: https://framaforms.org/rocqnshare-2026-registration-1769966293
More details: https://proofs.swiss/rocq-n-share/2026/

Are you itching to learn more about the internals of your favorite proof assistant? Do you have a feature to advocate for? Do you need help implementing an extension or hacking the kernel? Do you feel ready to step up and fix that bug that's been pestering you for years?

Join us for Rocq’n’Share! (contd. in thread)

#rocq #rocqprover

Yeeee, I completed chapter 1 (of 17) of volume 1 (of 7) of Software Foundation.

It's a long way to the top if you wanna #Rocq and roll.

Coq theorem prover is now called Rocq

https://rocq-prover.org/about

#HackerNews #Coq #Rocq #theorem #prover #programming #languages #proof #assistants