
Agentic Prover for Rocq
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.
u/Riiiiime — 7 days ago

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.