We want to write a series of blog posts about our efforts to use LLMs to formally verify code faster with the  Rocq/Coq theorem prover. Here, we present an experiment consisting of writing all that we are doing so that we can document our reasoning and help LLMs to pick up human techniques.
