Abstraction considered helpful

Machine code offers a common (ish) target across languages, compilers and runtimes. One view is that, at that level, broad properties such as memory safety are simple to state, and the AIs can figure out the necessary intermediate steps and proof infrastructure. In this perspective, such binaries are privileged sources of truth, bypassing the need to consider different languages and toolchains.

Because we do (ultimately) care about proving binaries correct, it is tempting to spend a few million tokens on doing that directly instead of deliberately building layers of semantic (mathematical) abstractions. If I were Big Token, I would welcome this approach. Perhaps the AI discovers useful abstractions along the way, though I and many who have tried this have seen current models create some atrocious results.²Footnote 2×Eventually, the models will be able to make useful abstractions along the way, and initially, I posit they will look similar to the ones I advocate for in this piece. It’s also tempting to privilege binaries when building language or software models from existing implementations, with lesser or no regard to the source code and processes that produced those binaries. In this approach, one aims for observational agreement via differentially fuzzing and fixing the model.

The situation reminds me of Leslie Lamport’s famous paper, “Composition: A way to make proofs harder”.³Footnote 3×Lamport, 1997. Composition: A way to make proofs harder, https://doi.org/10.1007/3-540-49213-5_15 Proving theorems directly over binaries implicitly echoes his arguments that “hierarchical decomposition does not simplify the total proof [...] it usually adds extra work [...] of writing the extra intermediate-level specification [and] restricts how the proof is decomposed”.

Simply stated, the hope is to save work by skipping layers of (sometimes leaky) abstractions. Even if this turns out to be true, interpreting any proof still takes work. Let’s consider a recent and impressive demonstration by Basis, for deriving an operational semantics for the pedagogical WHILE language from a reference C interpreter compiled to RISC-V. This is a great idea because RISC-V has a blessed formal Sail specification,⁴Footnote 4×There are also some who believe that creating a formal specification of an instruction set architecture was not historically the main blocker for verification of binary programs; this is a view which reflects priorities very different to ours. Sail has a Lean backend, and Lean has ports of the Iris separation logic and MachCSL frameworks. They summarise it as follows.

A person who wants to trust the result reads the statement [..], the hypothesis Loaded, and the two short definitions of Halts and Diverges

Loaded is a loaded definition in this theorem, carrying the memory layout of the abstract syntax and the interpreter state. So trust in their result requires understanding that,⁵Footnote 5×Or proving the relation between the abstract syntax and its memory representation is an isomorphism; likewise for the interpreter state. and a meta-assumption that the binary interpreter captures the intent of the WHILE semantics.

In turn, that meta-assumption is based on inspecting the C source and the binary's outputs. As far as I can tell, the C sources are visible to agents, meaning that source-level abstractions could be guiding the Lean definitions and proofs anyway, just informally. This has the downside of leaving more room for error, and more errors require more tokens to correct later.

This method of automating the derivation of a mechanised big-step semantics, which abstracts a binary reference interpreter, is clever, handy, and a valuable first step, but not sufficient. As I will demonstrate later, obtaining a semantics which is useful or captures intent requires further effort.

For example, for a language semantics, we would want to establish that it is neither too permissive nor too restrictive.⁶Footnote 6×With respect to extant or potential implementations, thus defining an envelope of allowed behaviours. From a narrow technical perspective, four ways to validate properties of a specification are:

1. Manually reading it, to validate intent.
2. Testing (including differential fuzzing) it, to validate observations.
3. Proving implementations satisfy it, to validate it as an abstraction target.
4. Proving useful properties from it, to validate it as an abstraction basis.

More broadly, Sewell et al.⁷Footnote 7×Sewell et al. (private correspondence). Escaping the quicksand: Mapping the way out. list sixteen social and technical criteria they believe specifications should meet.⁸Footnote 8×Such as being agreed upon by stakeholders, a single source of truth, maintainable, sufficiently abstract, sufficiently permissive, well-scoped, well-validated, mathematically precise, executable, mechanisable, useful for tooling, compositional across layers and components, and elucidating. While it’s laudable to aim for an entirely “bug”-free semantics, it is unrealistic for any large, real-world system such as RISC-V itself, or C: at the very least, the intent changes over time.⁹Footnote 9×Credit to Peter Sewell for this point. There are also concrete practical issues when dealing with instruction set architectures (ISAs) directly, such as their sheer size, which needs clever work-arounds,¹⁰Footnote 10×Sammler et al., 2022. Islaris, https://doi.org/10.1145/3519939.3523434 reasoning about the relaxed concurrency models they support,¹¹Footnote 11×Hammond et al., 2024. AxSL, https://doi.org/10.1145/3632863 and connecting those two ideas.¹²Footnote 12×Pérami et al., 2026. ArchSem, https://doi.org/10.1145/3776650

Hence whilst privileging binaries as a source of truth is appealing and useful in limited circumstances (such as for dazzling announcements), it is not a panacea. At the very least, semantics such as ISA models must be bootstrapped using methods similar to those used to develop the same for source languages; getting them adopted as official references is a separate task. For the Sail RISC-V specification, which grew out of work at the Universities of Cambridge and Edinburgh, SRI International and Bluespec, it took years of further work to be adopted by RISC-V International as the official “golden model”.

In fairness to Lamport, he did clearly state when he thought composition¹³Footnote 13×In this quote, Lamport was talking about component-wise decomposition theorems; I believe the same can be said for the hierarchical composition. was worth the extra work: “when the computer does a lot of it for you”. Humans create and benefit from abstractions to factor out common patterns of repeated work. Conversely, discarding source structure by shifting to lower-level representations loses information, meaning agents could spend more tokens repeating themselves, or recovering any abstractions from the bottom up.

A concrete example of this is in expressing control flow. The Cerberus semantics for C works by elaborating C into Core, a relatively simple, mostly standard, executable first-order functional language. Similar to C compilers, it translates different kinds of loops and early returns into one general goto-like control-flow construct, called “run” (goto) and “save” (labels). The semantics of this construct are unusual but effective. However, they have the side-effect of losing the natural ‘nesting’ of loops during execution.¹⁴Footnote 14×Makwana, 2026. CN: Theory and engineering for verifying C (Sec. 16.1). https://github.com/dc-mak/PhD-Thesis/releases/download/latest/main.pdf#page=175 This in turn means that any general-purpose reasoning rule for this construct would be unergonomic to use.¹⁵Footnote 15×https://github.com/rems-project/cerberus/issues/913

Binary code represents control-flow similarly, and suffers from the same problem: framing unused resources outside a loop invariant (thus allowing invariants to be nested compositionally), requires additional information.¹⁶Footnote 16×Gillian-C illustrates the additional machinery. It compiles loops to jumps while annotating instructions with a stack of enclosing loop identifiers. The verifier compares these stacks and their lengths to recognise entry and exit: it sets aside resources outside the invariant on entry, checks invariant re-establishment on a back-edge, and restores the saved frame on exit. Thus its loop-framing mechanism relies on source-derived nesting information preserved as annotations alongside the goto-based code. At that level, any difficulties caused by lost abstractions must either be accepted or reconstructed from the available information.¹⁷Footnote 17דa substantial fraction of our proofs concerns registers, stack frames and memory layout, which source-level abstractions would hide.”, Chaudhuri et al., 2026. https://google-deepmind.github.io/code-verification/ It is important to note that language semantics are definitional, they cannot be ‘verified’, only validated.

This problem is not unique to C semantics: Rust semantics also face similar problems. Its origin (and ultimately its solution¹⁸Footnote 18×https://github.com/rems-project/cerberus/pull/1005) relies on a deep understanding of SSA.¹⁹Footnote 19×Ghalayini and Krishnaswami, 2024. https://doi.org/10.48550/arXiv.2411.09347 Solving this problem is hard, but its potential benefits are great - we can reduce proof effort in verifying loops, test loop invariants at runtime more efficiently, and even automatically infer a certain class of loop invariants.²⁰Footnote 20×Klose and Mueller, 2026. https://doi.org/10.1145/3839488

Working at the source level offers the opportunity to integrate agents into specification engineering: an approach which recognises the importance and difficulty of working with large specifications in their own right, an under-appreciated and highly timely line of research. Aside from the ones mentioned so far (ISAs, inferring loop invariants), examples include optimising interpreters,²¹Footnote 21×Rao et al., 2025. https://dl.acm.org/doi/10.1145/3704858 inferring pre- and post-conditions,²²Footnote 22×Spies et al., 2024. https://dl.acm.org/doi/10.1145/3656413 and integrating specifications into existing workflows via testing and fuzzing,²³Footnote 23×Aamer et al., 2026. https://dl.acm.org/doi/10.1145/3808278 to find bugs and increase assurance incrementally, on the way to a full proof.

At Math Inc, our vision of the AI and formal verification revolution, autoverification, centers the expertise, taste and collaboration required to harness and build high-quality specification engineering tools and shared semantic models. Not doing so would be akin to viewing mathematics only in terms of proofs, ignoring the importance of definitions, theory building, and communication.

Our bet is that specification engineering and semantic models will provide more predictable, reliable, scalable, maintainable and comprehensible autoverification with fewer tokens.

We are turning this vision into a reality by tackling an ambitious research project: autoverify Linux’s implementation of the WireGuard handshake. Working with Galois and OathTech, with support from RAND, Math Inc aims to combine and advance state-of-the-art programming language and verification research with Gauss, our agent for autoformalisation, to create a system for scalable autoverification.

WireGuard is a widely used protocol for secure, encrypted network connections. The handshake establishes the cryptographic keys that devices use to communicate securely. Traditionally, this work can require years of specialist engineering. Our goal is to dramatically reduce that effort without compromising the rigour of the result.

Today, we are releasing two important milestones towards realising that goal.

1. An executable, mechanised model of the WireGuard handshake protocol, derived from the original C source. We have carefully defined kernel API boundaries²⁴Footnote 24×Major boundaries include: time, networking, concurrency, allocators. Plain C code for cryptography and handling data structures are kept. for the handshake C code, and then used that to derive an executable, mechanised model of the handshake, with mocked inputs for testing. By doing so, we have (a) found an instance of UB²⁵Footnote 25×Conversion of u8* with alignment 1 to __be64* with alignment 8 (C11 §6.3.2.3#7)., and (b) tested trace agreement down to the API boundary. As mentioned earlier, this is the payoff of working at the source level: catching errors in code or modelling earlier and cheaper, thus providing incremental benefit en route to a full proof.²⁶Footnote 26×QuickChick for Rocq, and Bennet/Darcy for C, extend this principle.

A key part of this effort is the choice of a semantic model of C. Math Inc is using and contributing to the open-source Cerberus C semantics, 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. Using its Lean port, maintained by OathTech, we parsed, elaborated (into Core), and executed (using its Core interpreter) the handshake code inside Lean. We believe Cerberus is unique in its ability to accurately and executably model real-world code at this scale, and provides a valuable stepping stone towards proving WireGuard’s handshake correct.

Each of those properties brings its own challenges and benefits. For accuracy, a source-level semantics defines the envelope of allowable compilations: it is more permissive than a binary, thus requires more general reasoning, but will factor out much work for any binary-level proofs. For execution, WireGuard is in the middle of the stack, thus requires its kernel services boundaries to be defined and mocked in a principled and scalable manner. We believe this is a first for code of this size, and this approach will enable us to parallelise and “tunnel to the middle”²⁷Footnote 27×Like the Gotthard Base tunnel, which commenced work on 5 sections at once, dramatically reducing construction time. for verifying large stacks of software, like the Linux kernel. Lastly, for scale, one line of C can represent many lines of lower-level representations: around 1.2K lines of C handshake code expands to a large amount of Core, (similar in abstraction level to SSA) which makes most UB explicit. This simplifies reasoning, but requires large scale specification engineering to handle.

Applying Cerberus to the WireGuard handshake benefits Cerberus too. We have found almost 40 new gaps or performance issues with Cerberus or its Lean port, issues only apparent when working at this scale. By finding and collaborating on fixes, our work at Math Inc not only uses these shared semantic models, but actively participates in improving them. This ties into our second milestone.

2. A substitution-based mechanised formalisation of Core’s operational semantics, guided by Chapter 6 of Memarian (2022). It abstracts away implementation-related details of Cerberus’ interpreter, whilst proving the latter refines the former. By doing so, we (a) found a design bug for jumping to labels,²⁸Footnote 28×Expressions inside Core’s label map are pre-computed per function and are effectively hoisted out to the top-level. Doing this means they lose their original lexical position, and so, may refer to out-of-scope variables. and (b) opened the door to simplifying and optimising Core in a formally verified way, and building verification infrastructure atop it.

Note that our semantics is formally linked with a refinement theorem to the existing implementation. We do not support the status quo of verification teams developing custom, ad hoc, non-executable, varyingly validated, unauthoritative or proprietary semantics for shared infrastructure. Technically, developing semantic models is its own domain of expertise and needs to be recognised and supported as such. Socially, semantic models need to be agreed upon by stakeholders, as with RISC-V’s Sail golden model, ISO TS 6001, Arm’s official ASL specification, and WebAssembly, or aiming towards it, as Cerberus does.

These milestones demonstrate our willingness and ability to solve practical engineering and open research problems, which will only expand as we tackle the following questions.

• What is the most convenient and sound representation of Cerberus’ Core semantics for a wide range of specification engineering tooling, beyond program logics?
• How can we ergonomically and faithfully reason about C code using read-copy-update (RCU) under the Linux kernel memory model?
• How could we compositionally extend C source proofs to realistic models of binaries?
• Given there is no verification without specification, how do we help programmers express their intent,²⁹Footnote 29×https://xkcd.com/568/, panel 2. and integrate specifications into their existing workflows?

Our ambition is not just a verification, but a system for scalable autoverification. WireGuard’s handshake provides a concrete, real-world test of that ambition and an opportunity for us at Math Inc to collaboratively advance the research, tools, methods and engineering practices needed to formally verify critical software.