Learning Rocq with Software Foundations

Last month (January 2026) I got into the Rocq proof assistant.

In this post, I’m going into my experience learning the basics of Rocq by working through the Software Foundations: Logical Foundations (Volume 1) book. We’ll take a quick look at Constructive Logic and Inductive Propositions (my biggest learnings), as well as common errors I made. Finally, I’ll summarize my experience so far with Rocq and what I’m doing next.

Rocq is a proof assistant that was recently renamed from Coq. Rocq is an interactive theorem prover and a functional programming language. Rocq has a small core: even familiar things like natural numbers and lists aren’t kernel built-ins. They’re defined in libraries. Using Rocq, we can define our own types (or use ones from the standard library) and prove theorems about them. This might be basic lemmas about natural numbers or large proofs such as the Four color theorem.

Rocq can be used for formal verification. Formal verification is the practice of specifying and proving properties about code. With formal verification, we can prove certain properties about programs such as memory safety, termination, or correctness. Currently, I am surveying different formal verification projects to verify the C source code of libsecp256k1. I chose the Verified Software Toolchain (VST) as the first candidate, since it’s one of the most mature projects and uses Rocq, a well-established general-purpose proof assistant. VST has been used to verify many crypto projects such as OpenSSL’s HMAC and SHA256, as well as SafeGCD. Even if I do not end up using VST, I still learned the valuable skill of using Rocq.

Rocq is not the first proof assistant for me. I am coming from using F* (FStarLang), which is a highly automated proof assistant with built-in SMT solving, so many goals are discharged automatically. I mainly used it with Low*, which is a subset and library of F* to generate verifiably correct and safe C code, and the HAX toolchain to verify Rust code.

I started reading Certified Programming with Dependent Types by Adam Chlipala because from the cover it seemed to serve my goal. I quickly realized that it was too advanced for me. When looking at the “Books” section on the Rocq website, it is the only free book that falls into the “advanced” category. Instead, I switched to Software Foundations: Logical Foundations (Volume 1), written by many authors.

I definitely do NOT recommend reading any Software Foundations book cover to cover as a PDF. The best aspect of the series is that the source of the book itself is Rocq proof scripts. The book is intended to be read inside an IDE like VS Code with the VSRocq extension. We can check proofs step by step ourselves and, more importantly, do the numerous exercises.

I briefly want to go into the two most interesting concepts of the book. If you find these interesting, you can take a look at my notes before deciding if you want to read it yourself.

Constructive Logic

As the name Logical Foundations suggests, the first book of the series dives into foundational logic. The authors explain the basics of constructive logic. In contrast to classical logic (which is taught in the first semester of many STEM degrees), constructive logic proofs must be explicit and constructive. We cannot argue abstractly that something must exist; we must give concrete evidence. One downside is that we cannot prove many things we take for granted in classical logic: for example, that every proposition is either true or false (forall P : Prop, P \/ ~P). A big advantage, however, is that proofs can be checked by machines.

Rocq specifically uses Intuitionistic type theory, a form of constructive logic whose foundation is the Curry-Howard correspondence. This principle equates propositions with types and proofs with programs. This essential connection makes machine checking possible. Since proofs are programs, a computer can verify their correctness by type-checking and evaluation.

While I’d seen most of this before, these chapters of the book really gave me a deeper understanding of constructive logic and why this basic theory is necessary to machine-check proofs.

Inductive Propositions

Inductive types and recursive functions are well-understood concepts for me and many others. Instead of expressing propositions using universal, existential, and logical connectives, propositions can be defined inductively by a set of rules. At first, I was confused why I would want to define a proposition in this more complicated way. However, it makes perfect sense when we are using constructive logic. To prove something is to construct a term of a type, and when that type is defined inductively, that often becomes a lot easier. We have the classical definition for even:

Definition even (n : nat) : Prop := 
    exists k, n = 2 * k.

We can define an equivalent proposition inductively. An even number is either 0 or the successor of the successor of an even natural number.

Inductive even' : nat -> Prop :=
| ev_0 : even' 0
| ev_SS (n : nat) (H : even' n) : even' (S (S n)).

When we have an inductive proposition in the hypothesis, we can do induction on that proposition. This was a big Aha! moment for me, as it allows us to prove more interesting things quite easily when we have inductive propositions in our context.

Throughout the exercises, I repeatedly ran into a few patterns of mistakes. If you’re starting out, hopefully this saves you some time:

• induction vs destruct. Before touching tactics, pause and decide what your proof object is. If you have an inductively defined type/proposition (e.g. nat, list, or a custom Inductive predicate) you often want induction (on the right thing!). For “finite” data like bool, option, or a small sum type, destruct is usually enough. Rule of thumb: look at the constructors of the thing you’re eliminating.

• Backward vs forward reasoning. Most proofs are written backwards: you transform the goal until it becomes a trivial term. Forward reasoning (working in the context) helps when you will need the same fact in multiple branches: derive it once, then reuse it. Typical forward tools: assert, specialize, and “cleanup” tactics like contradiction and discriminate.

• Direction matters for apply and rewrite. apply H tries to match the goal against the conclusion of H (and leaves the premises as new goals). rewrite H uses an equality to rewrite either the goal or a hypothesis. Use rewrite H in H1 / rewrite <- H when the direction is backwards.

• Tactics don’t always work in both places. Some act primarily on the goal (f_equal, reflexivity), others are most useful on hypotheses (inversion, subst). I created a small tactics reference while doing exercises and keep it open on the side.

• VSRocq sometimes gets confused (crashes 5 times in a couple of seconds) if you forget to close a proof with Qed. and keep editing.

Given that I already have experience with another proof assistant, I thought I would be verifying C programs using the Verified Software Toolchain by now (after a couple of weeks). However, the learning curve is quite shallow. It still takes a long time to learn, and is more like “read these two and a half books” than “skim this documentation in an afternoon.” Software Foundations: Verifiable C (Volume 5) lists the prerequisites before reading that book, which are Logical Foundations and a couple chapters from Software Foundations: Programming Language Foundations (Volume 2), including doing the exercises. All books are designed to be the basis for a computer science university course, which I suppose would have 5-6 ECTS. That is between 125 and 180 hours of work depending on experience, the number of optional chapters, and the scope of exercises, and is around the time it took me to complete the book and most exercises.

The integrated exercises and being able to step through proofs on your own is what makes Software Foundations unique. Grinding through progressively harder proofs and getting that small dopamine hit when Rocq says “There are no more subgoals” before writing Qed. makes it quite addictive.

Looking forward, I am going to continue reading Programming Language Foundations and then finally Verifiable C. I am very interested in more advanced proof automation using coqhammer and SMTCoq to see how they compare with SMT solving in F*.

Finally: Do the exercises!