Do not use this code. Nobody but me has read the C, there is no fuzzing, and SHRINCS is not a BIP yet. Verification comes last, after tests and review and fuzzing, and libshrincs is the exception to that rule today. It is a proof of concept for the verification architecture, not the library the name implies.

I built a C implementation of WOTS+C, the one-time signature that all of SHRINCS’s compact signing is built from, and proved two things about it. The Verified Software Toolchain (VST) proves that the C computes what a mathematical specification says it should, including memory safety and absence of undefined behavior. SSProve reduces forging a signature against that same specification, in a one-time experiment, to six hardness assumptions about SHA-256 truncated to 128 bits. Both proofs are written in the Rocq proof assistant. Both meet at the same 366-line definition. Code and proofs are at remix7531/libshrincs.

Joint work with Jonas Nick, whose companion post is on Delving Bitcoin. This follows on from Formal Verification of WOTS+, which proved every C function against a model of RFC 8391 but said nothing about whether the scheme could be forged.

As far as I can tell, nobody has combined VST and SSProve before. The shape is not new. Appel’s group paired VST with FCF for OpenSSL HMAC in 2015, and Completing the Chain did XMSS this year in EasyCrypt with a Jasmin implementation. Both go further than mine at the join. Appel’s group carried the FCF security bound into the contract of the C function itself, so their two halves meet in one machine-checked statement. Mine meet at a shared definition and stop there. What differs is the language at the bottom. Handwritten C, carrying comments and structure a reviewer needs, ready for the people who review Bitcoin’s cryptography today.

Two companion posts assume more familiarity with formal methods. Choosing the verification toolchain for libshrincs covers why C, why Rocq, why VST and SSProve specifically, and what each of those costs. The grind was the only detector is about writing 22,000 lines of proof with LLMs, and what cheap proofs take away besides the effort.

Thanks to conduition for feedback on an earlier draft of this post.

This work is funded by OpenSats, under the grant Advancing Formal Verification for Bitcoin Cryptography.

Background

A hash-based signature scheme builds signatures out of nothing but a hash function. No elliptic curves and no lattices. That is why they are the conservative post-quantum choice: their security rests on properties of hash functions that have been studied for decades.

WOTS+ sits at the bottom of such a scheme. A private key is a list of random secrets. The public key is the result of iterating a hash function over each secret a fixed number of times, giving one chain per secret. To sign, the signer reveals an intermediate value on each chain, at a position that encodes one digit of the message digest. A verifier hashes each revealed value forward the remaining number of steps and checks that it lands on the public key. Sign twice with the same key and the two signatures together leak chain values the scheme was relying on you not to reveal. The security claim covers exactly one signature. That is what the “one time” means.

That leaves an obvious attack. Anyone holding a signature can hash a revealed value forward. A value further along the chain corresponds to a larger digit, so an adversary can forge any message whose digits are all larger. WOTS+ blocks it with checksum chains: extra chains encoding the complement of the digit sum, so advancing a message chain forces you to walk a checksum chain backwards.

WOTS+C removes those chains. Instead of a checksum it requires the digits to sum to a fixed constant. Raising one digit then means lowering another, which is the same trap by different means. The signer hashes the message together with a counter, checks whether the resulting digits hit the constant, and increments the counter until they do. The counter travels in the signature, and the verifier recomputes the digits and rejects anything that misses the constant. The checksum chains disappear and the signature gets shorter.

Grinding makes signing variable-time. Harmless here: the hash being ground takes no secret input, and the number of attempts is the counter, which ships in the signature anyway. About 64 attempts on average, capped at 65,536, past which signing fails (which will never happen till the end of the world).

SHRINCS (Shrunken SPHINCS) is the scheme these signatures are for, introduced by Kudinov and Nick and presented on Delving Bitcoin. It targets Bitcoin transaction authorization, is instantiated with SHA-256 alone, and carries two signature schemes under one key pair, with a signature from either one verifying against it.

The stateful path is the compact one. It uses a flexible XMSS (FXMSS) tree, a Merkle tree whose leaves are one-time public keys. Each signature is a WOTS+C signature plus the authentication path, the siblings a verifier needs to walk that leaf up to the root. The signer picks the shape of the tree at key generation, trading signature size against signing budget: balanced gives constant-size signatures and a large budget, unbalanced gives very small first signatures that grow as the budget is spent. The stateless path is SLH-DSA at a non-standard parameter set. It is the fallback for a signer whose state is lost or in doubt.

For a thorough introduction to hash-based signatures, I recommend Alfred Menezes’s lecture series, starting with Lecture 1: Introduction.

If the formal methods are the unfamiliar half, two talks are a better starting point than this post. Karthik Bhargavan’s High-Assurance Post-Quantum Cryptography, from the OpenSSL Conference 2025, is the survey. Verified code from HACL* ships in Chrome, Firefox and Linux, and Cryspen’s libcrux put verified post-quantum cryptography into Firefox, OpenSSH and Signal. He is also clear about what those projects do not cover, and he ends on long-term maintainability rather than on the proofs.

Russell O’Connor’s Formal Functional Correctness of libsecp256k1’s Modular Inverse is the closest existing work to this one, and the same tools: Coq and Verifiable C. Bernstein and Yang’s new extended Euclidean algorithm went into libsecp256k1 a few years ago. A new algorithm carries a new risk of getting it wrong, and the proof is what answers that. If you would rather read than watch, I did the same to secp256k1_scalar_mul earlier this year: about 300 lines of C, Rocq and VST, roughly 6,400 lines of proof.

Two proofs, one definition

VST will certify a faithful implementation of a scheme an adversary can break in an afternoon. A game-based security proof models the attacker as a program playing a game against the scheme and bounds its chance of winning. Cryptographers argue a scheme is hard to break that way, and such a proof will happily certify a scheme whose shipped code reads out of bounds. Neither notices the other’s problem, and papers bridge them with a sentence saying the implementation follows the specification.

Here both proofs name the same definition instead.

That definition is 366 lines of Rocq. It says what WOTS+C computes and no more: what the chains are, how a digest becomes digits, what the counter has to satisfy, what signing and verification produce. Under it sits a 350-line address type fixing the 22-byte tweak encoding. That is how each hash is bound to its position in the tree, so a value computed in one place cannot be replayed in another. Someone judging whether this is really WOTS+C reads those two files, plus the byte, index and iteration types underneath them.

Outside its own types, the definition imports the Rocq standard library and nothing else. No VST, no SSProve. It cannot mention a memory predicate or a game, so neither proof can bend it toward itself or quietly specialize it to an easier case.

The C side

Seventeen functions are proved with semax_body, VST’s tactic for discharging a function body against its contract, with nothing left admitted. Eleven are the WOTS+C steps, four of those the public entry points: key generation, signing, recovering a public key from a signature, and verification. The rest are the tweakable hash, the address writer, and the libc helpers the library carries its own versions of.

One contract is currently stronger than it needs to be. The public address contract demands a fully well-formed 22-byte address, while the C depends only on the first 9 bytes and overwrites the rest before reading them. The proof therefore covers a subset of the inputs the C accepts. The C is correct on all of them, the contract just does not say so yet. An incompleteness rather than an unsoundness.

The security side

The headline theorem, shrincs_wots_secure_sha256, quantifies over all valid adversaries and bounds the chance of forging a signature, in a one-time known-message experiment, by a weighted sum of six terms. Each term is the advantage of an explicitly constructed reduction against one assumption on truncated SHA-256:

Adv(KOTS_vc, A)  <=  2 * eps_prf              -- PRF, key derivation from SKseed
                  +  2 * (w-2) * eps_smud     -- SM-UD, chain-value undetectability
                  +  eps_stcrp                -- S-TCR-P, the grinding hash
                  +  eps_tcr_pk               -- SM-TCR, public-key compression
                  +  eps_tcr_chain            -- SM-TCR, chain target collisions
                  +  eps_pre                  -- SM-PRE, chain preimages

Every reduction is a package that is built, not assumed. The six axioms are declared in one file, ssprove/axioms.v, and the abstract theorems above the SHA-256 instantiation use none of them. make audit diffs the whole assumption cone of each proof tree against an allowlist, so a new one fails the build. I read that last separation out of Print Assumptions, not out of the gate.

ssprove/wots/model_bridge.v is the file the architecture claim rests on. It proves that the scheme the games are played against computes what the shared model computes, at the concrete truncated-SHA-256 instantiation, as four equalities: public key generation, the counter search, signing, and verification. If it is wrong, the shared model buys nothing and this is two proofs about two different schemes with the same name.

Reducing to hash assumptions is what a security proof does. It does not follow that published numbers can be substituted for these six. The formal games differ from the experiments they resemble, and in places they are stronger: no tweak disjointness, and a length-preserving chain hash where the published generic bounds assume a compressing one. SSProve assigns no cost to anything, so the assumptions quantify over adversaries of unbounded running time. Read literally, that means the six are only satisfiable at an advantage of one. The concrete numbers have to come from outside the proof. The semantics are classical, and the function is a concrete one rather than a random oracle, so this is not a QROM result. The SSProve security review works through each of those, along with the experiment, the reduction, and the assumption games.

The trusted base

The trusted base is SHA-256, CompCert, VST, the six hash assumptions, the classical axioms the libraries bring with them, and the Rocq kernel. The kernel is the small program that rechecks every proof term. Everything else reduces to it.

SHA-256 is left uninterpreted in the model. Its 151 lines of C are assumed to match. VST ships Appel’s verified SHA-256, but closing the gap means adopting his C and reconciling two functional models, so it is not a matter of dropping in a file.

clightgen runs the C preprocessor, so what is verified is three preprocessed translation units, one of which folds in util.c textually while the shipped build compiles it separately. An include path that differs between the two invalidates the proof silently.

The classical axioms come with the libraries rather than from me. The C side inherits excluded middle, propositional and functional extensionality, set extensionality, Streicher’s K, and the classical reals, through CompCert and the Rocq standard library. The security side inherits classical choice, proof irrelevance, and its own copies of the extensionality axioms, through SSProve and mathcomp-analysis. The model inherits none of them. Its only assumption is SHA-256, so the definition both proofs are pinned to rests on less than either proof does.

Then there is what the kernel does not check. Four bridge files decide whether the two proofs are about the same scheme: one relates the flat byte array the C mutates in place to the structured address the model uses, and three relate the games to the model. About 1,200 lines, and with the contracts and the game statements around them a few thousand. That is the hand-checked surface. A wrong precondition or a wrong winning condition leaves either proof correct and worthless, and the kernel will not notice. The kernel checked all 22,484 lines around it: 6,215 for the C, 13,411 for the security half, and the remainder model and audit scripts. None of that checking reaches these.

There is also no single theorem with the C on one side and a security bound on the other (yet). The two statements are different kinds of judgement. Appel’s group did close that gap for HMAC. They carried the FCF bound into the postcondition of the C function’s contract, so one semax_body mentions both the code and the advantage. I have not done it, so I do not write end to end.

Comparison to the WOTS+ proof

The earlier WOTS+ work covered 269 lines of C in about 5,000 lines of Rocq. The strongest thing it said about the scheme was a round-trip theorem: what a signer produces, a verifier accepts. That is the most a functional model alone can offer. It is perfectly compatible with the scheme being trivially forgeable.

This one covers 346 lines of C and adds the two things that model could not say. VST adds that every array access is in bounds, the arithmetic does not overflow, no path has undefined behavior, and every caller-visible buffer is left in the state its contract names, including the ones a function only writes on its way through. SSProve adds the forgery bound.

The C grew from 269 lines to 346, and the effort did not grow in proportion. The WOTS+ specifications and the C-representation bridges carried over almost directly. Most of the new work was the security half, which is a different activity from proving C.

What’s next

Roughly in the order I expect to do it. The order matters more than the list, and the toolchain post makes that case.

• The BIP, written so it is easy to formalize. Closed loops, types that make illegal states unrepresentable, obvious branching, and trivial termination. If it transcribes into Rocq or Lean 4 line by line, its ambiguities surface before anyone proves the wrong reading.
• The C, written so it is easy to prove. Tests and fuzzing come before the proof, because proving the wrong code is the most expensive way to find out it has a bug. Review comes before all of it, and that is the part I need from other people.
• Strengthening my own SSProve skills. It is good enough to build an architecture around. I want it good enough to review a game hop line by line.
• SSProve for the rest of SHRINCS. The largest item by far. The FXMSS proof exists and is being refactored right now. The stateless path is SLH-DSA, so the tight SPHINCS+ proof applies and porting it from EasyCrypt to Rocq is work, not research. The stateful path has nothing to port: the machine-checked XMSS proof fixes the tree shape where ours is chosen by the signer, and the combiner putting two schemes under one key is uncovered. That part is new cryptography.
• VST for the rest of the C, and Appel’s verified SHA-256 in place of the axiom.
• Composing the two halves, which needs a substitution lemma and the memory argument that goes with it.
• Constant time, beyond the ctgrind runs I do today. BINSEC is the plan, and the toolchain post says why.
• Project-specific agents for proof maintenance, so that keeping this alive does not mean re-deriving it by hand every time a definition moves.

Underneath the list is the one thing I set out to find out. Two proofs of different kinds, about the same 366 lines, with neither able to bend the definition toward itself. That part holds. What is still missing is the join: the two halves meet at that definition and not in one theorem.

The library the name implies is not written yet. Its C comes after the BIP, and tests, review and fuzzing come before any proof about it. None of that takes a proof assistant, and none of it is work I can do alone. If you write C, fuzz it, or review cryptography, come find me when the BIP lands.