WireGuard in Linux

We proved 38 C specs of WireGuard in the Linux kernel at commit 551c722f (2026-09-29), with two lib/crypto patches. Each spec states a property, and each has a theorem in Rocq (formerly Coq). Nineteen short specs use no model of the protocol: the handshake's keys agree and its secrets are erased, stale, replayed and failed messages change nothing, the replay window accepts each nonce once, and the AEADs give back what they encrypted. The other 19 are the longer specs of our first proof, which compare the kernel with a model of the handshake. AI agents wrote the proof, about 300,000 lines of Rocq, and Rocq checks it. The specs, the proof and every change to the code are in genproof/wireguard-auto-proofs-public.

The short specs#

Each spec links to its page, which shows the spec whole, as it is in the repository, with its theorem. A short spec is 19 to 51 lines of C, 59 to 153 with its small shared headers. In a spec, any_u64(), upto(n), any_bytes(n) and the nondet_* functions stand for any value, and gp_assert states what must hold. The first comment of each file states the property in full, with every bound; it starts with Law, the older word for a spec.

The handshake#

Keys agree, secrets are erased, and stale, replayed or failed messages change nothing. 8 specs

• hs_matching_keysC file · 36 lines

  When a handshake between A and B completes on both sides, A's sending key is B's receiving key and the other way round, and only A's keypair is the initiator's.

• hs_session_erasesC file · 43 lines

  After an initiation and a response have been exchanged, a wg_noise_handshake_begin_session that succeeds leaves that side's handshake in state HANDSHAKE_ZEROED, with its ephemeral private key, the peer's ephemeral key and the chaining key all zero.

• hs_begin_session_stateC file · 42 lines

  Beginning a session from a handshake in any state but HANDSHAKE_CREATED_RESPONSE or HANDSHAKE_CONSUMED_RESPONSE fails, allocates nothing and leaves the three keypair slots as they were.

• hs_response_stateC file · 33 lines

  A response is taken only by a handshake that is waiting for one: in any state but HANDSHAKE_CREATED_INITIATION, consuming B's genuine response fails.

• hs_replay_initiationC file · 30 lines

  An initiation that B accepted is rejected when the same 148 bytes come again, at any later clocks, whether or not B answered it and began its session in between.

• hs_stale_responseC file · 34 lines

  After a new initiation, B's response to the old one is rejected (assuming the new random sender index differs from the old one).

• hs_reject_initiationC file · 45 lines

  A consume_initiation that fails, on any 148 bytes and with B's handshake with A in any state, leaves B's peer for A as it was: every field of its handshake, its three keypair slots and its reference count.

• hs_reject_responseC file · 41 lines

  A consume_response that fails, on any 92 bytes and after A's initiation, leaves A's peer for B as it was: every field of its handshake, its three keypair slots and its reference count.

Replay protection#

The replay window (counter_validate, copied out of receive.c) accepts each nonce once, and only inside the window. 5 specs

• rp_freshC file · 33 lines

  A nonce below REJECT_AFTER_MESSAGES and at most 8128 below the newest accepted nonce (or with none accepted yet) is accepted, after any other nonces.

• rp_duplicateC file · 25 lines

  A nonce that was accepted is rejected when it comes again, after any nonces in between.

• rp_too_oldC file · 26 lines

  A nonce more than 8128 below the newest accepted nonce is rejected.

• rp_limitC file · 19 lines

  Every nonce at or above REJECT_AFTER_MESSAGES (2^64 - 8130) is rejected.

• rp_any_orderC file · 30 lines

  For any start s with s + 8128 below REJECT_AFTER_MESSAGES, after any nonces below s, any distinct nonces from s to s + 8128, given in any order, are all accepted.

Encryption and the primitives#

What is encrypted decrypts, a failed decryption writes nothing, and feeding data in pieces changes nothing. 6 specs

• ae_roundtripC file · 29 lines

  ChaCha20-Poly1305: for any message, associated data, 64-bit nonce and key, decrypting what encryption wrote succeeds and gives back exactly the message.

• ae_xroundtripC file · 30 lines

  The same for XChaCha20-Poly1305, with a 24-byte nonce.

• ae_fail_untouchedC file · 51 lines

  A decryption that fails (either AEAD, any bytes as ciphertext) leaves every byte of its output buffer as it was.

• ae_split_blake2sC file · 37 lines

  BLAKE2s in one call gives the same hash as init, update over the message in any pieces, and final, for any key of 0 to 32 bytes and any output length of 1 to 32 bytes.

• ae_split_chacha20C file · 39 lines

  ChaCha20 over the whole message writes the same bytes as over it in pieces, all but the last a multiple of 64 bytes, for any key, block counter and nonce.

• ae_split_poly1305C file · 33 lines

  Poly1305 gives the same tag for the message in one update or in any pieces, for any key.

Earlier, longer properties#

These are the 19 specs of our first WireGuard proof, renamed x_<name> with their statements unchanged. They check the handshake in noise.c and cookie.c, from any state, failure paths included, against a model of the handshake written as plain C from the WireGuard paper (harness/common.h). They show that receive.c's handshake checks, copied out of it, let only messages of the exact type and length through and check mac1 before the handshake code runs. They compare the portable C of BLAKE2s, Poly1305 and the two ChaCha20-Poly1305 AEADs with reference implementations written from RFC 7693, RFC 8439 and the XChaCha draft. Four of them put these pieces together the way the data path does, and that glue is assumed or copied, not verified.

• x_handshakeC file · 339 lines

  For two devices with any keys, preshared key, clocks and randomness, every step of a full handshake returns the model's result and writes the model's bytes. When both identities are usable, the Diffie-Hellman values agree and none of them is zero, the timestamp is not zero, B's boot clock is at least 20 ms and the one allocation succeeds, every step succeeds and each side's sending key is the other's receiving key. Clearing the keypairs frees everything.

• x_create_anyC file · 188 lines

  From any prior state of the device, the peer and its handshake, wg_noise_handshake_create_initiation and wg_noise_handshake_create_response return what the model returns, write exactly the model's message bytes and handshake fields, and change nothing else, on every failure path too.

• x_consume_initiation_anyC file · 194 lines

  wg_noise_handshake_consume_initiation on any 148 bytes, with any peers in any state, accepts exactly when the model does (the static key decrypts to a known peer, the timestamp is newer, the 20 ms flood limit holds, ...); it then updates that peer exactly as the model does, and on rejection it changes nothing.

• x_consume_response_anyC file · 170 lines

  The same for wg_noise_handshake_consume_response on any 92 bytes and any contents of the index table.

• x_replayC file · 128 lines

  Over any sequence of fresh and replayed initiations, with the clocks moving (the real-time clock also backwards), an initiation is accepted exactly when its timestamp is newer than every accepted one and the last acceptance was at least 20 ms earlier; a replay is always rejected and changes nothing.

• x_keypairsC file · 516 lines

  Over any sequence of session starts, key use, expiry, clearing, and gets and puts of references, the three keypair slots, every keypair, its reference count (with the saturation of the kernel's refcount_t), the index table and the frees agree with a model after every step, with no bound on references or sessions.

• x_handshake_clearC file · 91 lines

  From any state, wg_noise_handshake_clear zeroes exactly the handshake's session state, takes its entry out of the index table, and changes nothing else.

• x_config_anyC file · 177 lines

  The seven configuration functions of noise.c and cookie.c, called over any prior contents, set exactly what the model says (a degenerate private key gives an unusable identity) and change nothing else.

• x_cookie_macC file · 271 lines

  On any message of 32 to UINT_MAX bytes and any cookie state, wg_cookie_add_mac_to_packet and wg_cookie_validate_packet compute exactly the model's mac1, mac2 and verdict, the cookie secret is renewed once it is at least 120 seconds old, and nothing else changes.

• x_cookie_replyC file · 283 lines

  wg_cookie_message_create writes exactly the model's cookie reply, and wg_cookie_message_consume on any 64 bytes, with any peers and tables, updates exactly the cookie the model updates, or nothing.

• x_handshake_receiveC file · 622 lines

  Over any sequence of packets of any bytes and lengths, receive.c's validate_header_len and wg_receive_handshake_packet let only messages of the right type and length reach the handshake code, check mac1 (and under load mac2) before any of them, send exactly one cookie reply under load, and update the endpoint, timers and statistics only of the authenticated peer; a rejected packet changes nothing.

• x_counterC file · 83 lines

  Over any sequence of 64-bit nonces, the data path's replay window counter_validate accepts a nonce exactly when it is below the message limit, within 8128 of the highest accepted nonce, and not accepted before.

• x_transport_orderC file · 132 lines

  With the kernel's AEAD decryption and counter_validate run in receive.c's order (assumed, L15), for any sequence of received data packets (authentic, corrupted, replayed or random bytes), a packet with a bad tag leaves the replay window unchanged and delivers nothing, and an authentic one gets the window model's verdict.

• x_transport_keepaliveC file · 104 lines

  With the same assumed order (L15), a keepalive (a data packet with an empty payload) follows the same authentication and replay rules as other data packets and delivers nothing, and a packet too short to hold a tag is rejected without a read past its end.

• x_transport_lenC file · 115 lines

  For a data packet of any length and type word, the length check admits exactly the packets the length rules admit, and decryption never reads past the packet (for an admitted packet, decrypted as L15 assumes).

• x_transport_send_nonceC file · 77 lines

  The sending nonce, drawn as send.c draws it, never repeats or wraps, and sending is refused exactly from REJECT_AFTER_MESSAGES on. The spec contains a copy of send.c's nonce draw (send.c itself is not in the code under test), and the run ends before the counter would step from 2^63 - 1 to 2^63 (L16).

• x_prim_blake2sC file · 75 lines

  BLAKE2s (blake2s_init, keyed init, blake2s_update in any chunks, blake2s_final, and the one-shot blake2s()) computes RFC 7693's BLAKE2s for any key of 0 to 32 bytes, output length of 1 to 32 bytes and message, and zeroes its context.

• x_prim_poly1305C file · 68 lines

  Poly1305, fed in any chunks of any length up to PTRDIFF_MAX (2^63 - 1 bytes), computes RFC 8439's Poly1305 for any key and message, and zeroes its context.

• x_prim_aeadC file · 15 lines

  ChaCha20-Poly1305 encryption is RFC 8439's construction, and XChaCha20-Poly1305 encryption is that construction with the subkey that HChaCha20 derives from the key and the first 16 bytes of the nonce, and the last 8 bytes as the nonce, for any lengths of message and associated data up to PTRDIFF_MAX. Decryption of any bytes succeeds exactly when the reference tag verifies and leaves the output unchanged otherwise.

AI agents (Claude Opus 5.5 in Claude Code) wrote the first proof of these 19 specs.

Limits#

Each theorem is harness_safe whole_prog, where whole_prog is the spec linked with the kernel code it calls. By VST's adequacy theorem it means that for any value the spec draws, no run has undefined behaviour in CompCert's semantics of C and every check holds. That adequacy theorem is not yet instantiated in Rocq for QuickProof's environment. "Any" means every value up to the bounds in the first comment of each spec.

• Runs of more than one thread are not covered. Locks, RCU and atomics are those of a single thread.
• Termination is not proved. A run that never returns is not a counterexample.
• The rest of the driver is not covered: peer.c, device.c, netlink.c, send.c, timers.c, ratelimiter.c, allowedips.c, peerlookup.c, socket.c, queueing.c, receive.c's parsing of UDP and IP headers and its handshake queue, and the scatterlist versions of the AEAD.
• x_transport_order, x_transport_keepalive and x_transport_len assume that receive.c checks the tag before the replay window, as its code does.
• Constant time and erasure on free are not covered.
• The model in harness/common.h is written from the WireGuard paper, and reading it is the only check that it is WireGuard.
• X25519 itself, the other implementations of the primitives, other configurations, the unpatched source and binaries built by other compilers are not covered.
• The theorems rest on 13 axioms: standard logical ones and the declarations of VST's abstract malloc library. The result also trusts Rocq, VST, CompCert's semantics of C, clightgen, QuickProof's translation scripts, its model of the environment and qp verify (What a proof means).

How to check it#

You need 64-bit x86 Linux with Coq 8.20.1, CompCert 3.15 and VST 2.15 (Install), or QuickProof's Docker image. Check the proof with a QuickProof checkout of your own at v0.1.0, the release the repository pins:

git clone --branch v0.1.0 https://github.com/genproof/quickproof-public.git quickproof
git clone --recursive https://github.com/genproof/wireguard-auto-proofs-public.git
quickproof/tools/qp verify wireguard-auto-proofs-public --base contract

The code under test#

The code is Linux at commit 551c722f40809618230001baccf219193e22fc5a: noise.c and cookie.c (the handshake), receive.c and their headers, and lib/crypto/. It is built as an architecture without optimised crypto and without __int128 builds it: the generic C of BLAKE2s and ChaCha20, and Poly1305 and Curve25519 with 32-bit limbs. An x86_64 kernel builds other variants of Poly1305 and Curve25519.

The code carries two patches from our lib/crypto series: poly1305_update() and chacha_crypt() take size_t lengths (below). Idioms that VST cannot reason about are rewritten, and the kernel around the code is a shim of plain C for one thread. The repository's DEVIATIONS.md lists each change with its test. The changes are tested, not proved.

The bug the specs found#

On the unpatched code, x_prim_poly1305 and x_prim_aead are false at lengths of 4 GiB and more. poly1305_update() could copy past its 16-byte buffer, and the ChaCha20-Poly1305 functions used only the low 32 bits of their lengths. No caller in the kernel passes such lengths.

We sent patches to the linux-crypto list on 2026-10-12. Eric Biggers then converted Poly1305 and ChaCha to size_t lengths in his own series, "lib/crypto: Use size_t lengths for Poly1305 and ChaCha", which credits the report. On 2026-10-16 he applied it to the lib/crypto tree, libcrypto-next, with our follow-up for 32-bit arm and MIPS. The code proved here carries our two patches, not his series. Proving the specs again on his series is future work.

Maintained by Vladimir Kukharenko.