Pick a scheme because its assumptions are old and well understood, then verify the implementation with a proof pipeline younger than the code it is checking, and you have not removed the risk. You have moved it into the tooling, where it is harder to see. You may have increased it, through false confidence. Every translation step between the source you ship and the statement a kernel checked is a place where that happens.

Hash-based signatures are the conservative choice among the post-quantum options. Their security reduces to properties of hash functions that have been studied for decades, which is why BSI exempts them from its hybrid-deployment recommendation. That reasoning should not stop at the scheme.

This post lays out the choices I made for libshrincs and what each one costs. I made the short version of the language argument in the WOTS+ post. This is the full version, plus everything else. It is a note to my future self as much as to you. I forget things, and I would rather read my own reasoning in a year than reconstruct it.

Verification comes last

The most important decision here is not about tools at all. It is about ordering. The proof is the last step: tests, then review, then fuzzing, then a proof of what is left.

Each of those catches a different kind of mistake, and the later steps do not retire the earlier ones. A proof says nothing about whether the specification is the one you wanted. That is exactly the question review is good at. Serious review of cryptographic code is slow, skilled work. Do it before the proof. Proving code nobody has read wastes the proof if the code turns out wrong.

The libshrincs repository is the exception to its own rule. It has tests and no fuzzing, and nobody but me has read the C. It exists to find out whether the verification architecture holds up. One primitive is enough for that, and it does not need a finished spec. The ordering above is what the real library gets, once the BIP lands and the code is written to stay.

The language

The implementation is C. It is ISO specified, it has several independent implementations, and qualified compilers have decades of use in avionics, automotive, and industrial control. Auditors and procurement teams know what to do with it.

The argument specific to this project is narrower. The people who would review this code already read C. libsecp256k1 is C, so Bitcoin’s cryptography reviewers are C reviewers. A post-quantum signature library that wants review from that community should not also ask it to learn a language first.

Rust is the better language for new projects and it is where this code should eventually live. I have used hax and Aeneas on non-trivial implementations and I like both. Today Rust has one production compiler, a specification effort much younger than the language, and a certification story (Ferrocene, the Safety-Critical Rust Consortium) that auditors have not caught up with. Certification, procurement, and deployment cycles add years on top of whenever that lands.

The cost of choosing C is real: no borrow checker, no type-level guarantees, and a proof obligation for every array access that Rust would have discharged for free. I pay that in proof lines.

The prover

The C proof is in VST and CompCert, and the security proof is in SSProve. Both sit in Rocq.

Most of the momentum in formal program verification is elsewhere: Rust and Lean 4, Aeneas and hax and the libraries built with them. I follow that work closely and I am looking forward to using it. Writing proofs there is more pleasant and more efficient than what I am doing here. For most projects it is the better answer.

For this one I wanted something more rigid. The argument is the one that picked the scheme. Rocq has been in continuous development since the 1980s. Long enough that its failure modes are known. The newer tools are better in most of the ways I notice day to day, and I picked the old one anyway.

The other half of the answer is that I can afford to. Hash-based signatures are structurally simple: the code walks a data structure, so the invariants are structural and the proof burden is high but dull. That is the case where an older, slower tool costs me proof lines and nothing else. VST is good enough here in a way it would not be for a scheme with real arithmetic in it.

One kernel, or several tools

The newer pipelines tend to spread work across tools, extracting one source into several backends and proving a different property in each. Functional correctness in one system, protocol security in another, game-based security in a third. That is good engineering when the pieces are independent.

Here they are not. The extraction between tools is trusted. The models on either side of it are related by argument instead of by theorem. If the functional-correctness model and the security model disagree, no kernel anywhere notices, because no kernel ever sees both.

Verification Theatre, a 2026 audit of two verified Rust libraries, reported 13 bugs: 9 in parts nobody had verified, and 4 inside the verified perimeter, three of those specification errors and one a proof that should not have gone through. The authors of the libraries dispute the count and deny that any verified code was affected. I do not know who is right. I would want an audit that hard on my own code. Either way it documents the gap between the assurance a library advertises and the assurance it carries. A trusted step between tools is one place that gap opens.

Staying in Rocq means both proofs are stated against the same model of WOTS+C. The function contracts say the C implements that model, the games are built from it, and their agreement is one definition in one development. It is still not one composed theorem.

An additive pipeline

VST proves the C I ship. It does not produce it.

HACL* generates its C from F*, and Jasmin generates its assembly from Jasmin source. In both, the shipped code is an output of the proof instead of an independent artifact under review. Jasmin buys something I do not have: its compiler is proved in Coq to preserve constant-time down to assembly, given a source-level check. Speculative constant-time has no such theorem for the shipped compiler, which is its own argument for checking the binary.

I run ctgrind under three compilers and claim nothing beyond that. The gap is closable in the same additive style. BINSEC checks constant-time on the compiled binary, without the source and without committing me to a particular compiler, so the guarantee can be added afterwards. A bounded analysis, not a proof the kernel rechecks. Evidence rather than a theorem. Also future work.

The additive order buys reviewability. The C is an ordinary C library that can be read line by line. The proofs sit beside it instead of in the way. Someone can fix a bug in the C without ever opening Rocq. If VST and SSProve are both superseded in ten years, the same C is still there.

Why VST and CompCert

Nothing about VST is new. The first paper is from 2011. It is not a one-lab project either: groups at Princeton (Appel and Beringer) and the University of Illinois Chicago (Mansky) carry it, and Cao’s group at Shanghai Jiao Tong built VST-A on top of it and QCP alongside it. Fifteen years of continuous maintenance means it outlasted multiple PhD students. Plenty of academic verification tools never get there, because they are built for a thesis and go quiet a year or two after the student graduates. VST is not frozen either. The program logic has been rebuilt on top of Iris, a framework for concurrent separation logic, shipping as the 3.x beta line since 2024 and under active development, while the 2.x line I build on stays stable.

Then there is documentation. Verifiable C is Volume 5 of Software Foundations, the textbook series that teaches Rocq itself. You can work through it without knowing anybody. With most verification tools the real documentation is the source or the maintainer. Access to a maintainer is not something to depend on for infrastructure that strangers will maintain decades from now.

VST is also foundational. Its program logic is proved sound in Rocq against the operational semantics of CompCert Clight. That soundness proof is checked by the kernel like everything else. Not for free: the C side inherits excluded middle, propositional and functional extensionality, set extensionality, Streicher’s K, and the classical reals, through CompCert and the standard library. Those come with the libraries rather than from me, but they are in the trust surface and calling them “the extensionality axioms” hides half the list. Floyd, its tactic layer, symbolically executes a function forward inside that proved-sound program logic, turning a program plus a contract into the obligations left over. It gets there by building a proof, not by handing conditions to something else. The term it emits is rechecked by the kernel, so a bug in Floyd costs me a failed proof and not a false one.

CompCert carries the other half and made the same journey from research project to industry support. AbsInt sells and maintains it for safety-critical customers, a slower and more rigid kind of maintenance than a research group offers. The caveats are worth stating. That half of the chain applies only to binaries actually built with CompCert, its theorem stops at assembly with the assembler and linker below it trusted, and the free compiler is under a non-commercial license. Build libshrincs with GCC and the proof covers the source only.

VST also ships a proof I can reuse. Appel’s verified SHA-256 would replace the axiom my C currently rests on.

Why SSProve

SSProve deserves the same scrutiny. There the requirement did most of the choosing: I needed a game-based framework inside Rocq.

EasyCrypt is the obvious alternative and passing on it has a real cost, because the strongest existing work on hash-based signature security is in EasyCrypt. Two things pushed me away. It puts the security proof in a different system from the C proof, which is the trusted-extraction problem above. And it is not foundational: obligations go to SMT solvers, and what comes back is trusted rather than reconstructed as a proof term that a small kernel rechecks.

One concession belongs next to that. EasyCrypt can express the running time of an adversary and SSProve cannot, so on the axis a cryptographer cares about most, the tool I passed on is ahead of the one I took.

Inside Rocq the practical choices are FCF and SSProve. FCF’s development has slowed. I took SSProve because state-separating proofs, where a scheme is built from composable packages and a security argument is a sequence of package rewrites, match the shape of the paper proofs being mechanized. That will matter more once WOTS+C composes into FXMSS than it does for the one-time signature alone.

SSProve dates from 2021, nowhere near the maturity I just credited Rocq and VST with. Its wide author base is not the same thing as day-to-day maintenance, which sits with a few people. Being foundational in the same kernel as the C proof was worth more to me than the extra years. It is the weakest link in everything above.

The documentation is the clearest disadvantage. VST has a volume of Software Foundations you can work through knowing nobody. SSProve has the paper, the examples, and then the source. The wrong kind of dependency for infrastructure meant to outlast its authors. So I am writing a tutorial as I learn the framework properly. Work in progress.

Tooling that outlasts its vendors

The same standard applies to the tools that write the proofs, not just the ones that check them.

These proofs were written with frontier models from Anthropic and OpenAI, driving rocq-mcp the way I described in April. That is fine for building the thing and wrong to depend on for maintaining it. I cannot run either one, and I cannot promise anyone that they will still exist. So I have set myself a requirement. libshrincs has to stay maintainable with open-weights models on a high-end consumer card, not a datacenter cluster.

I do not know yet whether I can hold it. The trend helps, since open-weights models improve by the month. What the proofs cost to write is most of why this matters at all.

What it costs

All of this costs me. Proving C against a Rocq model is far more proof work per line than pushing Rust through Aeneas into Lean: the 269 lines of C in the WOTS+ implementation took about 5,000 lines of Rocq, a ratio of roughly 19:1.

That grind is getting much cheaper, for reasons I wrote about separately. Automation is what the newer toolchains sell, and also the part I expect to get cheaper on its own whichever one you pick. So I weighted longevity over ergonomics.

The argument is much weaker for lattice cryptography and for field arithmetic, and not because of line count. secp256k1_scalar_mul is about 300 lines, roughly the size of my WOTS+ C. It took an order of magnitude more time to prove. The shape of the obligation differs. Hash-based code walks a data structure, so the invariants are structural. Modular arithmetic needs bit-exact equalities with operand bounds threaded through every carry, and NTTs and rejection sampling pile more on top. If I were shipping ML-DSA I would want the code generated from a specification, and the newer Rust and Lean 4 pipelines would look a lot more attractive.