Adjacent to my work on formal verification of libsecp256k1, I dabbled in a side project on hash-based signatures. Unsure about the difficulty, I built a formally verified C implementation of the Winternitz One Time Signature Plus (WOTS+) using the Verified Software Toolchain. It turned out to be surprisingly easy relative to the modular scalar multiplication in libsecp256k1.

Every WOTS+ C function is proved to match a mathematical specification of what it should compute, and the specification itself is proved to be internally consistent.¹ The trusted base is SHA-256 (left abstract in the model, and the C implementation is assumed to match that abstract model), CompCert, VST, and the Rocq kernel. Code and proofs are at https://github.com/remix7531/wots-fv.

Background

WOTS+ is a one-time hash-based signature scheme. A WOTS+ private key is a list of random secrets. The public key is the result of iterating a chaining hash function over each secret a fixed number of times. To sign a message, the signer reveals an intermediate hash on each chain whose position encodes a digit of the message digest. A verifier reapplies the chaining function to the revealed values and checks that the resulting chain endpoints match the public key.

WOTS+ is the one-time signature underlying XMSS. SLH-DSA (the stateless hash-based signature scheme standardized by NIST in FIPS 205) signs a message with FORS at the bottom of a hypertree, with each layer above using WOTS+ to sign the public key of the layer below. Verifying WOTS+ is a prerequisite for verifying either scheme.

For a thorough introduction to hash-based signatures, including Lamport, Leighton-Micali (LMS), XMSS, and SPHINCS+, I recommend Alfred Menezes’s lecture series, starting with Lecture 1: Introduction.

Why hash-based signatures

The German federal cybersecurity agency BSI takes an unusually clear position in TR-02102-1. It recommends that all post-quantum signature schemes be deployed in hybrid combination with a classical scheme, with one exemption. Hash-based signatures (SLH-DSA, XMSS, LMS) may be used standalone. The reasoning is that their security reduces to complexity-theoretic assumptions about cryptographic hash functions, which are well understood. The lattice problems underlying ML-DSA are newer, and BSI notes that the quantum-safe mechanisms it recommends are “not yet trusted to the same extent as the established classical mechanisms” with respect to side-channel resistance and implementation security.

The implementation literature backs this up. ML-DSA reference implementations have seen repeated side-channel and fault-injection attacks (ePrint 2025/582, ePrint 2024/138). SLH-DSA has its own fault-attack literature (Castelnovi-Martinelli-Prest), so the gap is smaller than the citation count suggests. The structural reason is that hash-based signing does no secret-dependent arithmetic on large rings. The secret-dependent surface is SHA-256 over the seeds. SHA-256 is attackable too, but it’s a much smaller surface than a lattice signing pipeline, and far better studied.

Signatures are large: around 2.1 KB for WOTS+ at these parameters, and 7 KB to 49 KB for SLH-DSA depending on parameter set. Signing and verification are orders of magnitude slower than ECDSA. Reusing a one-time key breaks the scheme catastrophically; XMSS and SLH-DSA are the bookkeeping layers on top that prevent that. For long-term signatures (firmware, code signing, regulated archival), hash-based is the conservative choice today.

Bitcoin is another angle. Hash-based signatures are a candidate for a future post-quantum soft fork. Bitcoin needs smaller signatures and is willing to accept different trade-offs than NIST and other standards bodies.

What is proved

There are two layers. First, each of the ten WOTS+ C functions is proved to satisfy a precise contract written in Rocq: input shape, memory layout, and a postcondition expressed in terms of a mathematical model of RFC 8391. Second, the model itself is proved correct as a signature scheme: a signature produced by sign is accepted by verify against the matching public key, for any byte-string message. In Rocq this looks like:

Theorem wots_correct : forall M sk_seed pub_seed ADRS,
  Forall byte_ok M ->
  verify (genPK sk_seed pub_seed ADRS)
         (sign M sk_seed pub_seed ADRS)
         M pub_seed ADRS = true.

The verified C totals 269 lines (wots.c plus util.c; sha256.c is axiomatized, which shrinks the denominator). The hand-written Rocq proof totals about 5,000 lines, a ratio in the same range as the secp256k1 scalar multiplication proof.

This is functional correctness, not cryptographic security. We do not prove unforgeability: that an adversary given the public key and one signature cannot forge a signature on a different message. For WOTS+ the relevant notion is one-time EUF-CMA, a game-based statement that needs a different framework, and it assumes the caller never reuses a key.

Spec style

The Gallina model is written to read like the RFC 8391 pseudocode, with a small custom for i < n {{ ... }} notation for the bounded loops of WOTS+. This is one of the things I want to push further in future work. A specification that a cryptographer can read and agree with line by line against the standards document is as important as the proof itself. If the spec is wrong, the proof is worthless. My fips-180-4-lean project is the direction I would like to take this: a literate translation of the SHA-2 standard PDF, with the formal definitions sitting next to the prose they encode.

Why VST and C

Post-quantum signatures need to ship soon. BSI’s TR-02102-1 gives classical signatures a runway until the end of 2035. Sounds generous. It isn’t: regulated-industry migration eats most of a decade even after a compliant toolchain exists.

C is the path that exists today. Qualified C compilers like HighTec (based on GCC and LLVM), Wind River Diab, and Green Hills have been used in safety-critical automotive, avionics, and industrial code for decades. The auditors know what to do with them. SLH-DSA is built on SHA-256, which is well studied, and verifying it in a language with a similarly long certification track record fits.

I love Rust, and the ecosystem is moving fast on both qualified toolchains (Ferrocene, the Safety-Critical Rust Consortium) and formal verification tooling (hax, Aeneas, both of which I have used on non-trivial implementations). Auditors and procurement teams lag the open-source ecosystem by years. Even once a qualified Rust toolchain is in every auditor’s vocabulary, certification, procurement, and deployment cycles add years on top. Rust is where I want this code to live, but that is not realistic right now.

VST proves your existing C source. HACL*, the other major verified-C ecosystem, produces excellent verified C from F*, but the C is a compilation output of the proof, not the source of truth.

When the C is compiled with CompCert the guarantee extends through to assembly. Commercial use requires a paid license from AbsInt, but it is the only mature verified C compiler that exists.

Comparison to secp256k1 scalar multiplication

This was the surprise of the project. Modular scalar multiplication in libsecp256k1 is roughly 300 lines of straight-line C with no loops, and the proof was hard. Every intermediate arithmetic operation comes with a precondition on the bounds of its operands. The proof has to thread those bounds through hundreds of multiplications, additions, and carries. The Gallina spec is arithmetic equality modulo a 256-bit prime. Every bit has to match.

WOTS+ is the opposite shape. There are loops, but the bodies are short, and each loop has a clean inductive invariant. There is no integer arithmetic to track beyond loop counters and array indices. The spec is structural (the verifier accepts what the signer produces), not arithmetic, so the proof is largely about showing that the C code walks the same list-shaped data structure as the model. SHA-256 is the only real complexity, and it is sealed behind axioms.

In rough numbers, WOTS+ took me a small fraction of time that modular scalar multiplication did, despite having more verified C lines.

Future work

The natural next step is to extend to SLH-DSA, starting with FORS (the few-time signature scheme that sits one layer above WOTS+ in SLH-DSA’s hypertree). The WOTS+ specifications and model carry over directly.

On the security side, I would like to do for SLH-DSA what I sketched at the end of the secp256k1 post: a refinement chain from a high-level cryptographic security proof in SSProve down to verified C, then to a CompCert-compiled binary. There is ongoing EasyCrypt work on SLH-DSA that would be a reasonable starting point.

A few smaller items on the list:

• Improve the public C API to use uint8 sig[static x] rather than raw pointer parameters. I could not figure out how to express this constraint in VST specifications.
• Rewrite the Gallina spec in a more pseudocode-faithful style, similar to what I did in my Lean fips-180-4-lean project. The current spec is close, but a side-by-side read against RFC 8391 should be effortless.
• Replace the axiomatized SHA-256 with VST’s existing verified SHA-256 implementation, eliminating the largest item in the trusted base.