Math Inc Runs WireGuard's Linux Handshake Inside a Formal Proof Engine

Math Inc, working with Galois and Oath and funded by RAND, has released an executable formal model of the WireGuard handshake in the Linux kernel. Derived from the implementation’s C source, the artifact runs a complete two-peer scenario inside Lean, a programming language and theorem prover. It is the first public component of a larger effort to produce a machine-checked correctness proof.

Tests sample selected executions, while formal verification uses mathematical proofs to cover every behavior allowed by a stated model. Building those proofs for production C often requires years of specialist work. Math Inc plans to use its Gauss proof-generation system to reduce that cost, although the current release does not yet measure Gauss’s speed or effectiveness.

A runnable model, scoped tightly

Executing the model shows that the translated program can reproduce the expected sequence under controlled conditions. A universal correctness theorem must quantify over all permitted inputs, states, and environmental behavior while proving that the implementation satisfies a separate formal specification.

WireGuard forces kernel-scale questions

WireGuard is a VPN protocol whose handshake authenticates peers and establishes session keys for encrypted traffic. Its Linux implementation depends on kernel facilities for timers, networking, concurrency, memory allocation, and cryptography, so verification cannot treat the handshake as an isolated function.

Math Inc cites Tailscale’s deployment of WireGuard across more than 2.5 million active devices, along with its use for traffic between Kubernetes nodes. Those deployments make the code operationally relevant, while its kernel dependencies expose the service boundaries that any broader verification system must model.

The company’s stated ambition extends from this handshake to the wider Linux kernel and eventually to billions of lines of systems C. WireGuard provides a compact target for finding missing semantics, weak abstractions, and performance limits before attempting larger subsystems.

The case for staying close to C

Formal verification can begin from source code, compiler intermediate representations, binaries, or machine code. Binary-level proofs describe the instructions that execute and avoid uncertainty about compiler output, but they also inherit registers, stack frames, calling conventions, and concrete memory layouts.

Math Inc’s source-level argument favors preserving the structure available in C. A single C operation can expand into many machine instructions, and source abstractions allow proofs to focus on program state and control flow without repeatedly reconstructing the programmer’s intent from assembly.

A source-level theorem still needs a justified path to the executable binary. That path can rely on a verified compiler, translation validation, or an explicit assumption that the compiler preserves the behavior of defined C programs. The released WireGuard artifact focuses on ISO C semantics and does not verify the compiler’s output.

From C source to Lean traces

The pipeline uses Cerberus, an open-source semantics for ISO C developed primarily by Kayvan Memarian at the University of Cambridge. The current flow has five stages:

1. Cerberus parses the Linux kernel’s WireGuard handshake source.
2. It elaborates the program into Core, a small first-order functional language that makes C evaluation rules and many undefined-behavior conditions explicit. Core sits at roughly the same abstraction level as static single-assignment representations used by compilers to expose data flow.
3. The Core interpreter executes inside Lean.
4. Controlled models replace kernel services for time, networking, concurrency, and allocation.
5. The resulting trace is compared with an independent reference implementation.

Mocked services turn external kernel behavior into explicit interfaces that the model can control. Those interfaces also define the current proof boundary: any eventual theorem must state their assumptions precisely or replace them with verified implementations.

An alignment fault surfaces in C

While processing the handshake, the team found undefined behavior involving conversion from a u8 * carrying one-byte alignment to a __be64 * requiring eight-byte alignment. The latter is the kernel’s type for a big-endian 64-bit value. C11 §6.3.2.3#7 requires the converted pointer to satisfy the target type’s alignment rules.

Source semantics exposes that violation before compilation. A binary analysis begins after the compiler has selected instructions and applied assumptions permitted by the C standard, which can obscure the source-level condition that enabled an optimization or memory access.

Core’s interpreter gets a semantic anchor

Math Inc also released a mechanized operational semantics for Core and a refinement proof connecting Cerberus’s executable interpreter to that semantics. An operational semantics is a mathematical rulebook for how each program step changes state. The refinement proof shows that interpreter executions conform to those rules.

Future proof tools can target the smaller mathematical semantics while retaining a proved connection to the interpreter used for execution. Developing that connection also exposed a Core control-flow bug: hoisted label expressions could refer to variables that had moved out of scope.

The universal proof remains open

Math Inc plans to use Gauss, its AI system for proof generation, to prove that the handshake implementation satisfies a formal specification. A complete result will need to make several elements explicit:

• The protocol properties being proved, such as authentication, key establishment, replay handling, and key rotation.
• The inputs, states, schedules, and failure modes covered by the theorem.
• The assumptions attached to mocked kernel services and cryptographic primitives.
• The treatment of concurrency and interactions between peers.
• The connection from ISO C semantics to compiled kernel code.
• The trusted computing base, including Lean, Cerberus, the compiler path, and any external axioms.

Gauss’s contribution cannot be evaluated from the executable scenario alone. Useful evidence would include proof completion rates, elapsed time, human review effort, generated proof size, and the cost of updating proofs when the kernel code changes.

Real kernel C strains the tooling

Running production kernel code through Cerberus and its Lean port exposed between 40 and 50 missing cases or performance problems, according to Math Inc. The team is helping address those issues upstream, expanding the tools beyond the subset of C exercised by smaller verification examples.

Upstream fixes will determine whether other projects can reproduce the workflow without maintaining private patches. They will also reveal how much engineering is required when the same pipeline encounters additional kernel idioms, architecture-specific code, and larger state spaces.

Evidence required at the next milestone

The next release can establish whether the project advances from executable semantics to practical verification by publishing:

• A machine-checked theorem for the handshake and its formal specification.
• A precise inventory of assumptions and unverified boundaries.
• Coverage beyond one deterministic execution scenario.
• A documented connection between the source theorem and compiled kernel code.
• Reproducible measurements of Gauss’s automation, runtime, and human workload.
• A maintenance test showing how the proof responds to a realistic source change.