Verified Software Assumes What Its Arithmetic Requires: An Axiom Census of Four Rocq Developments

Abstract

A machine-checked proof of a program's correctness is conditional on whatever the development assumes, and for deployed software that condition is the whole point. Four Rocq developments are censused with one source-level instrument: the CompCert verified C compiler, fiat-crypto, whose generated field arithmetic ships in BoringSSL, the Iris concurrent separation logic with its std++ prelude, and the Verified Software Toolchain. The proportion of files transitively reaching an axiom ranges from 0.0% to 65.6%, and none of the four appears to have taken a position on classical logic. CompCert reaches 65.6% because it verifies floating point, floating point requires the real numbers, and the Rocq reals are built classically; fiat-crypto is integer arithmetic throughout and requires no axiom-carrying module at all. The assumption base is determined by what the software computes. A raw axiom count conflates at least three things here: assumptions about an interface the proof cannot see, statements that are true and provable but left unproved, and declarations that assert nothing. In fiat-crypto's full dependency tree the most widely inherited axiom, reached by 856 files, is a test fixture. In the Verified Software Toolchain a lemma its own comment describes as false is admitted and then used twice inside a built proof of AES key expansion, reported as PrincetonUniversity/VST#867; a second admitted proof in the same file has no remaining subgoals and fails only because Qed does not terminate, and a dependency report renders the two identically.