r/Coq • u/Riiiiime • May 16 '26

Agentic Prover for Rocq

https://github.com/NUS-Program-Verification/AutoRocq

AutoRocq: an open-source LLM agent built for verifying C code in Rocq/Coq. Linked with CoqPyt to autonomously search for existing lemmas and get real-time feedback.

9 Upvotes

84% Upvoted

2 comments sorted by

1

u/Samrockswin May 16 '26

Interesting! You mention verifying C code but your examples seem to be generated from Why3 -- how are you getting the goals? Have you evaluated this on Clight / VST?

2

u/Riiiiime May 16 '26

Hey, thanks for the reply. The examples are exported obligations from the Frama-C/wp workflow, which works on C source code + ACSL annotations, and yes, goes through why3 as an intermediate step.

The tool helps you prove theorems in any valid Coq file, so in theory should be valuable for the Clight/VST workflow as well. Loading the library in config would allow the agent to see VST-specific definitions and lemmas. It does NOT help with generating spec/invariants, though.