Specifying verified x86 software from scratch

Mario Carneiro

arxiv: 1907.01283 · v1 · pith:CVVJJ4HGnew · submitted 2019-07-02 · 💻 cs.LO

Specifying verified x86 software from scratch

Mario Carneiro This is my paper

Pith reviewed 2026-05-25 10:50 UTC · model grok-4.3

classification 💻 cs.LO

keywords x86-64ELF binariesdynamic semanticsformal specificationPeano arithmeticmachine codesystem callsinput-output behavior

0 comments

The pith

A framework specifies and proves the input-output behavior of x86-64 ELF binaries inside first-order Peano arithmetic.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a minimal framework to describe and prove facts about how x86-64 executable files take input and produce output. It encodes only the necessary details of machine-code execution and Linux system calls inside a logic no stronger than first-order Peano arithmetic. The accompanying verification language and checker are likewise reduced to the smallest set of features needed for general proofs. A sympathetic reader would care because the approach lets verification begin directly at the binary level with an unusually small set of trusted definitions.

Core claim

The dynamic semantics of x86 machine code, together with enough information about Linux system calls to handle simple input and output, can be specified inside a logic equivalent to first-order Peano arithmetic so that concrete facts about the observable behavior of ELF binaries become provable.

What carries the argument

The specification of the dynamic semantics of x86 machine code together with selected Linux system-call details for input-output.

If this is right

IO properties of binaries become provable without any intermediate source language or compiler model.
The trusted base for verification stays limited to the arithmetic logic and the minimal proof checker.
Simple system-call specifications suffice for end-to-end proofs of observable program behavior.
The same style of specification can be reused for other binaries once the machine semantics are fixed.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same minimal-logic technique could be applied to verify compiler output by checking the emitted binary directly.
Extending the system-call model to more calls would test how far the arithmetic base remains sufficient.
The method suggests a route to machine-checked proofs of entire software stacks that begins at the instruction level.

Load-bearing premise

The observable input-output behavior of x86-64 programs under Linux can be captured completely and accurately by axioms no stronger than first-order Peano arithmetic.

What would settle it

An x86-64 ELF binary whose actual input-output trace on a real machine differs from every possible model definable in first-order Peano arithmetic.

read the original abstract

We present a simple framework for specifying and proving facts about the input/output behavior of ELF binary files on the x86-64 architecture. A strong emphasis has been placed on simplicity at all levels: the specification says only what it needs to about the target executable, the specification is performed inside a simple logic (equivalent to first-order Peano Arithmetic), and the verification language and proof checker are custom-designed to have only what is necessary to perform efficient general purpose verification. This forms a part of the Metamath Zero project, to build a minimal verifier that is capable of verifying its own binary. In this paper, we will present the specification of the dynamic semantics of x86 machine code, together with enough information about Linux system calls to perform simple IO.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper gives a minimal x86-64 and Linux syscall spec inside Peano arithmetic for the Metamath Zero self-verifier project.

read the letter

This paper gives a minimal x86-64 and Linux syscall spec inside Peano arithmetic for the Metamath Zero self-verifier project. The core contribution is a direct specification of dynamic machine semantics and enough system call behavior to talk about I/O on ELF binaries, all written in a first-order logic stripped down to what is needed for efficient checking. They also describe a custom verification language and proof checker built with the same minimalism in mind. That combination is new for this line of work and directly serves the goal of a verifier that can check its own binary with a tiny trusted base. The repeated stress on saying only what is required and avoiding extra machinery is consistent and useful for anyone thinking about trusted computing bases in verification. The paper does a clean job explaining the design choices and how they fit the larger Metamath Zero effort. The x86 model and syscall interface are presented as fresh content for the project rather than a rehash of prior formalizations. The main limitation is that the text stays at the level of describing the specification. There are no worked examples of actual proofs about I/O behavior or machine-checked derivations shown, which makes it hard to judge how complete or accurate the model turns out to be in practice. Soundness therefore rests on the claim that the spec was written carefully, without independent checks visible here. This is for people already working on minimal proof systems or low-level binary verification. Readers outside that niche will find the motivation clear but the details narrow. The thinking is coherent and the formal grounding is the point of the work, so it deserves a serious referee even if the current version is mostly definitional.

Referee Report

0 major / 2 minor

Summary. The paper presents a simple framework for specifying and proving facts about the input/output behavior of ELF binary files on the x86-64 architecture. The specification is performed in a logic equivalent to first-order Peano Arithmetic, with a custom verification language and proof checker designed for minimalism and efficiency. It includes the dynamic semantics of x86 machine code along with sufficient Linux system call details to handle simple I/O, as part of the Metamath Zero project to construct a minimal verifier capable of verifying its own binary.

Significance. If the specifications and machine-checked proofs hold as described, the work is significant for formal verification of low-level systems. The focus on extreme simplicity in the logic, specification, and checker directly supports the goal of minimizing the trusted computing base, and the self-verification aspect of Metamath Zero is a strong point. The provision of a direct specification of x86 semantics and system calls in a weak logic (rather than a derivation from prior fitted results) is a concrete strength.

minor comments (2)

The abstract states that the logic is 'equivalent to first-order Peano Arithmetic,' but the manuscript should explicitly state the precise axiom set used (e.g., which induction schema or arithmetic operations are included) to allow readers to verify the claimed equivalence.
Section describing the x86 dynamic semantics should include a short table or list of the supported instructions and addressing modes, as the claim of 'simple' coverage is central to the minimality argument.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation of minor revision. No major comments appear in the provided report.

Circularity Check

0 steps flagged

No circularity: direct formal specification with no fitted predictions or self-referential derivations

full rationale

The paper presents a framework for specifying the input/output behavior of ELF binaries on x86-64 inside a simple first-order Peano Arithmetic logic, as part of the Metamath Zero project. No equations, parameters, or predictions are fitted to data; the work consists of direct axiomatic specifications of machine semantics and Linux system calls. The derivation chain is self-contained as a manual formalization rather than any reduction of outputs to prior fitted inputs or self-citations. No load-bearing steps match the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract only; no explicit free parameters, additional axioms, or invented entities are described beyond the stated equivalence to first-order Peano arithmetic.

axioms (1)

domain assumption The specification logic is equivalent to first-order Peano Arithmetic
Explicitly stated in the abstract as the foundation for the framework.

pith-pipeline@v0.9.0 · 5641 in / 1096 out tokens · 38603 ms · 2026-05-25T10:50:33.253895+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

the specification is performed inside a simple logic (equivalent to first-order Peano Arithmetic)
IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

theorem execXASTMul ... readEA k sz (RM_EA k rm) src

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.