Working with Galois and Oath, with support from RAND, Math Inc is developing a new approach to proving the correctness of real-world software.
Math Inc has made significant progress toward mathematically proving that critical software behaves as intended, demonstrating that verification infrastructure for real-world C code can be built rapidly in Lean. It is applying AI across mathematical modelling, machine-checked proof construction, and the infrastructure needed to support both. Working alongside Galois and Oath, and with funding from RAND, the team is developing the tools and methods needed to bring formal verification to software that is already deployed in the real world.
WireGuard is a critical building block for secure networking, especially for datacenters. Tailscale alone reports more than 2.5 million active devices, with connections protected by WireGuard’s end-to-end encryption. The project focuses specifically on WireGuard’s handshake implementation in the Linux kernel, which establishes the cryptographic keys that devices use to communicate securely.
Math Inc’s ambition is to develop new directions in programming language research, proof engineering and verification infrastructure that can scale to the entire Linux kernel and billions of lines of systems C code. WireGuard’s deep kernel dependencies and subtle C semantics make it a demanding testbed for defining principled service boundaries, exposing undefined behavior, and building source-level models that capture permitted behavior across platforms.
The technical position piece Abstraction considered helpful sets out this approach and two concrete milestones. The released executable Cerberus-Lean model of the WireGuard handshake derives from the implementation’s C source through Cerberus’s Core representation. It runs a complete two-peer handshake scenario inside Lean, with explicit models of kernel services and results matching an independent reference implementation. A companion formalisation of Core’s semantics is linked to the interpreter by a refinement proof. Together, these milestones provide a foundation for the WireGuard correctness proof and the reusable verification infrastructure needed to tackle larger systems.
Traditionally, formal verification can require years of specialist engineering. Math Inc’s goal is to dramatically reduce that effort without compromising the rigor of the result.
Why it matters
Software underpins critical infrastructure, financial systems, communications, and national security. Yet even widely used, security-sensitive software can be difficult to verify.
Datacenters and neoclouds, the cloud providers built around AI workloads, depend on networks to connect their machines and services. WireGuard is one part of that infrastructure: it is used to encrypt traffic between nodes in Kubernetes clusters. Verifying WireGuard and the wider network infrastructure is therefore a critical step toward establishing the correctness of the systems that support AI training, inference and other cloud workloads.
Through formal verification, Math Inc is offering a stronger standard: mathematical evidence that software satisfies explicitly defined properties.
Math Inc is tackling this challenge with Gauss, its AI-driven system for automating mathematical proof generation. Rather than relying on AI to simply inspect code and suggest that it is correct, Gauss helps turn software behavior into formal statements that can be proved and checked mathematically.
What the project aims to deliver
- A machine-checked verification result: Work towards proving that the Linux kernel’s WireGuard handshake implementation satisfies its formal specification.
- More scalable verification: Reduce the specialist engineering and manual effort required to construct proofs, making it practical to tackle larger and more complex codebases.
- Better tools for verifying real-world code. Develop and improve the underlying verification infrastructure, including the capabilities needed to reason rigorously about C programs, their control flow, and their use of memory.
How Math Inc is approaching the problem
Math Inc is developing an approach that combines AI-driven proof generation with rigorous verification tools and decades of programming language and verification research. The aim is to automate the work of constructing proofs while retaining an independently checkable mathematical standard for the result.
A key part of this effort is the verification infrastructure itself. Math Inc is contributing to the open-source Cerberus project, developed primarily by Kayvan Memarian, PhD (Cantab), Assistant Research Professor at the University of Cambridge. Cerberus gives C programs a precise and empirically validated mathematical model grounded in ISO C, enabling machine-checked reasoning on top of it.
These capabilities matter because AI-driven verification depends on more than the quality of the AI model. The underlying tools must be able to represent real programs faithfully and support the reasoning required to prove their properties.
The long-term goal: scalable autoverification
Math Inc’s long-term goal is scalable autoverification of all future software: making rigorous, machine-checked guarantees a practical part of how software is built and changed.
As AI makes it possible to generate and modify code at greater speed and scale, the ability to establish that software behaves correctly becomes increasingly important. Verification must become more scalable too.
WireGuard is a concrete starting point for that ambition. The reusable semantic models, proof infrastructure and automation developed through this work are intended to scale to larger systems, including the Linux kernel and billions of lines of systems C code.