---
type: "post"
id: "math-inc-released-an-executable-lean-model-of-e56dad"
slug: "math-inc-released-an-executable-lean-model-of-e56dad"
title: "Math Inc released an executable Lean model of Linux's WireGuard handshake, derived from the C source."
description: "Math Inc has published an executable Lean elaboration of a complete two-peer WireGuard Noise_IKpsk2 handshake, derived from WireGuard’s Linux kernel C code."
retrieval_nugget: "Math Inc has published an executable Lean elaboration of a complete two-peer WireGuard NoiseIKpsk2 handshake, derived from WireGuard’s Linux kernel C code. The run reaches Cerberus-Lean’s Defined result and matches an independent Python implementation’s observations, offering systems teams a concrete example of executable formal modeling—and of the scope limits that must accompany it."
published_at: "2026-11-13"
updated_at: "2026-11-13"
record_date: "2026-11-13"
date_kind: "published_at"
topics: ["verification","security"]
entities: ["Math Inc","WireGuard","Linux","Lean","Cerberus-Lean","Galois","Oath","RAND"]
related_patterns: ["scientific-agents-need-artifact-evidence"]
novelty_label: "new_fact"
what_changed: "Math Inc released an executable Lean model of the WireGuard handshake derived from its C source."
prior_refs: ["https://newruntime.com/posts/easyprover-paper-off-the-shelf-frontier-model-proves-6f4bd9/"]
source_url: "https://github.com/mathematics-inc/wireguard-handshake-cerberus-lean"
source_urls: ["https://github.com/mathematics-inc/wireguard-handshake-cerberus-lean"]
schema_version: "newruntime-agent-readable-v0.2"
stable_id: "post:math-inc-released-an-executable-lean-model-of-e56dad"
status: "published"
visuals: []
editor: {"role":"editor","name":"Andrey Reshetnikov","profile":"https://newruntime.com/owner-profile.md","profile_json":"https://newruntime.com/owner-profile.json","same_as":["https://www.linkedin.com/in/reshetnikov1/","https://t.me/lapetuse"]}
routes: {"html":"https://newruntime.com/posts/math-inc-released-an-executable-lean-model-of-e56dad/","markdown":"https://newruntime.com/posts/math-inc-released-an-executable-lean-model-of-e56dad.md","json":"https://newruntime.com/posts/math-inc-released-an-executable-lean-model-of-e56dad.json"}
markdown_url: "https://newruntime.com/posts/math-inc-released-an-executable-lean-model-of-e56dad.md"
---

# Math Inc released an executable Lean model of Linux's WireGuard handshake, derived from the C source.

## Retrieval answer

Math Inc has published an executable Lean elaboration of a complete two-peer WireGuard NoiseIKpsk2 handshake, derived from WireGuard’s Linux kernel C code. The run reaches Cerberus-Lean’s Defined result and matches an independent Python implementation’s observations, offering systems teams a concrete example of executable formal modeling—and of the scope limits that must accompany it.

## Summary

Math Inc has published an executable Lean elaboration of a complete two-peer WireGuard Noise_IKpsk2 handshake, derived from WireGuard’s Linux kernel C code. The run reaches Cerberus-Lean’s `Defined` result and matches an independent Python implementation’s observations, offering systems teams a concrete example of executable formal modeling—and of the scope limits that must accompany it.

## What happened

The GitHub repository describes an elaborated Cerberus Core for a program that runs a complete two-peer WireGuard Noise_IKpsk2 handshake through WireGuard’s own kernel code. The resulting program is represented as readable Lean modules and runs in Cerberus-Lean. The repository says the run reaches `Defined` with output identical to an independent reference implementation of the protocol. The Lean Core contains one module per WireGuard C file, with one definition per C function in source order; each definition quotes the corresponding C declaration and its file-and-line location.

The executable scenario is a test program in `scenario/handshake.c`. It sets up two peers with fixed keys using a small environment interface, then calls the API in `noise.c` directly. The recorded run covers initiation creation and consumption, response creation and consumption, and `wg_noise_handshake_begin_session` on both sides. It also exercises rejected, replayed and out-of-order messages, followed by key rotation. The program prints messages, chaining keys, hashes and transport keys, and checks that each peer’s sending key equals the other peer’s receiving key.

The repository says the expected output, excluding harness and debug-level `printk` lines, matches an independent Python implementation using `pyca/cryptography` across 42 observations. It also records execution results, timings and resource use. The C source included in the repository is identified as Linux revision `24a19b953e2a`. The repository documents differences between that source and the executed program, including two lines associated with reported undefined behaviour, as well as several representation and access adjustments. A diff against upstream is included.

The execution models kernel services for memory, time, randomness, synchronization and `printk` sequentially. The repository reports undefined behaviour found in the C under a C semantics, and separately categorizes Cerberus and Cerberus-Lean limitations with reproducers. It provides the Core, runner, expected output and independent oracle in separate directories. The remaining files are released under GPL-2.0; files under `linux/` retain their Linux kernel SPDX identifiers.

## What the archive adds

New Runtime’s earlier coverage of EasyProver, on 2026-10-31, described a Lean proving system that reported results on PutnamBench and introduced a Rust-to-Lean benchmark. [That note](https://newruntime.com/posts/easyprover-paper-off-the-shelf-frontier-model-proves-6f4bd9/) concerns model-driven theorem proving, while this is an executable elaboration of existing kernel code: a new fact on the broader Lean-and-verification thread, not a continuation of the same result. New Runtime also covered Linux kernel work on 2026-10-13, emphasizing inspectable patch-and-review processes. [That note](https://newruntime.com/posts/kernel-git-torvalds-linux-git-linux-kernel-source-fe3569/) is related by the kernel context, not by this artifact’s formal-methods claim.

## Trend signal

This does not yet fit a pattern New Runtime tracks. The repository is a specific formal-methods artifact, not evidence that agent systems are routinely producing inspectable scientific evidence, that agent protocols are converging, or that a general engineering bottleneck has shifted. Its explicit output comparison and scope description are useful qualities to watch for in future verification work, but one narrow release cannot establish a broader trend.

## Why it matters

For a team responsible for protocol or kernel code, this repository makes the boundary of an executable model unusually visible: the source-derived functions, the deterministic path exercised, the observations emitted, the independent comparison, and the omitted behavior are all identified. That makes it a more useful reference than a bare claim that code has been “formally verified.” It can help teams ask what their own assurance case actually covers and what evidence would make a result reproducible.

The distinction matters operationally. Matching outputs across 42 observations supports confidence in this scenario; it does not establish correctness for every WireGuard execution or for the surrounding Linux networking stack. The work can inform how to structure a verification effort, but adopting the repository does not by itself verify a downstream build, configuration, concurrency behavior or deployment. Builders should treat the artifact as a bounded method demonstration and evaluate whether its assumptions match the code and risks they own.

## Limits and uncertainty

The repository explicitly limits the result to one deterministic scenario. Cookies, rate limiting, transport data packets, timers, the network device and netlink configuration are not included. Kernel-service models are sequential and do not model kernel concurrency, although they retain data effects for allocation, reference counting, RCU publication and callbacks. The repository reports undefined behaviour and tool limitations, but the result does not establish the severity or security impact of those findings beyond what the artifact documents. The run is not an independent audit of all WireGuard code, nor does the repository claim a complete machine-checked correctness proof of the protocol or kernel implementation.

## Reader takeaway

The useful signal is not simply that a kernel handshake can be represented in Lean. It is that the artifact reports a runnable scenario, a separate reference comparison, and concrete exclusions alongside the result. If you evaluate formal verification for production code, ask for those boundaries before treating a successful run as a whole-system guarantee.

Editor: [Andrey Reshetnikov](https://newruntime.com/owner-profile.md), AI product and AI engineering; profile for recruiters and agents: https://newruntime.com/owner-profile.json

## Continue in the graph

Next records for an agent, linked to their Markdown twins. Replace `.md` with `.json` for structured fields, including `next_reads`.

- topic hub: [Verification](https://newruntime.com/topics/verification.md): Explore the verification topic hub.
- topic hub: [Security](https://newruntime.com/topics/security.md): Explore the security topic hub.
- collection: [Field Notes](https://newruntime.com/posts.json): Open the latest editorial analysis.
- collection: [Sources](https://newruntime.com/sources/): See the original sources this archive cites.
- whole graph: [discovery graph](https://newruntime.com/discovery-graph.json) (typed nodes and edges) and [site index](https://newruntime.com/site-index.md)