s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs

Balaji Rao; John Harrison; Soonho Kong; Juneyoung Lee; Carlo Lipizzi

Source-linked AI summary

s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs

Balaji Rao, John Harrison, Soonho Kong, Juneyoung Lee, Carlo Lipizzi

arXiv:2603.14628v2Mar 15, 2026cs.PLcs.AIcs.CRcs.LO

TL;DR

Competition-style theorem-proving benchmarks do not establish whether LLMs can construct proofs about real implementations. This paper introduces s2n-bignum-bench, which turns verified industrial cryptographic assembly routines into machine-checkable HOL Light proof-synthesis tasks. GPT-5.3-Codex solves 4.4% of problems in medium-effort mode and 5.3% in high-effort mode, providing an initial baseline for this setting.

Problem
Existing mathematics-oriented benchmarks do not by themselves demonstrate LLM ability to construct proofs about real-world implementations.
Method
The benchmark extracts formal specifications from verified s2n-bignum assembly proofs and asks LLMs to generate proof scripts accepted by HOL Light under fixed evaluation conditions.
Results
GPT-5.3-Codex achieves a binary proof-completion rate of 4.4% in medium-effort mode and 5.3% in high-effort mode over the full benchmark.
Takeaways & Limitations
s2n-bignum-bench provides a reproducible testbed for evaluating theorem proving and verification-oriented reasoning beyond competition mathematics.
Takeaways & Limitations
Type-annotation obfuscation works for only approximately 70% of the problem set because HOL Light’s printer and parser are not fully Pollack-consistent.

Abstract

from arXiv · show

Neurosymbolic approaches leveraging Large Language Models (LLMs) with formal methods have recently achieved strong results on mathematics-oriented theorem-proving benchmarks. However, success on competition-style mathematics does not by itself demonstrate the ability to construct proofs about real-world implementations. We address this gap with a benchmark derived from an industrial cryptographic library whose assembly routines are already verified in HOL Light. s2n-bignum is a library used at AWS for providing fast assembly routines for cryptography, and its correctness is established by formal verification. The task of formally verifying this library has been a significant achievement for the Automated Reasoning Group. It involved two tasks: (1) precisely specifying the correct behavior of a program as a mathematical proposition, and (2) proving that the proposition is correct. In the case of s2n-bignum, both tasks were carried out by human experts. In \textit{s2n-bignum-bench}, we provide the formal specification and ask the LLM to generate a proof script that is accepted by HOL Light within a fixed proof-check timeout. To our knowledge, \textit{s2n-bignum-bench} is the first public benchmark focused on machine-checkable proof synthesis for industrial low-level cryptographic assembly routines in HOL Light. This benchmark provides a challenging and practically relevant testbed for evaluating LLM-based theorem proving beyond competition mathematics. The code to set up and use the benchmark is available here: \href{https://github.com/kings-crown/s2n-bignum-bench}{s2n-bignum-bench}.

1 INTRODUCTION

Existing theorem-proving benchmarks largely emphasize competition mathematics, leaving uncertain whether LLM reasoning transfers to practical implementations. s2n-bignum-bench addresses this gap with a machine-checkable benchmark for verified low-level cryptographic code, accompanied by reproducible evaluation and integrity mechanisms.

Existing benchmarks emphasize competition-style mathematics, motivating broader evaluation of LLM reasoning on practical engineering tasks.
s2n-bignum-bench tests whether LLMs can synthesize machine-checkable proofs about verified low-level cryptographic implementations.
The benchmark packages 2,284 proof obligations as isolated context–query tasks with stable identifiers and standalone artifacts.
Its pipeline supports offline evaluation and detects unsound submissions through axiom, placeholder, and parser-level integrity checks.
Type-annotation obfuscation is included to mitigate contamination from memorized theorem statements.

2 BACKGROUND AND RELATED WORK

Interactive theorem provers provide kernel-checked verification for structured proof generation, while established benchmarks primarily cover formalized competition mathematics and newer work extends toward software verification.

LCF-style interactive theorem provers ultimately have derivations checked by a small trusted kernel producing theorem values.
In neural theorem proving, LLMs propose proof steps and interactive theorem provers verify them, requiring structured and verifiable reasoning.
MiniF2F contains 488 formalized Olympiad-level mathematics problems translated across multiple proof systems.
Recent benchmarks extend evaluation toward verification conditions, repository-scale software verification, and context- or project-level generalization.

3 MOTIVATION

Existing theorem-proving evaluations do not fully test machine-checkable reasoning about industrial low-level cryptographic assembly. s2n-bignum supplies a corpus where proofs connect decoded instructions and machine state to mathematical specifications.

This reasoning involves architectural state, aliasing, and endianness, distinguishing it from math-centric proving and higher-level verification-condition proving.
Each proof starts from register and memory preconditions and establishes a mathematical postcondition after executing decoded ARM or x86 instructions.
The proof process decomposes programs at program-counter offsets, rewrites through ISA-specific semantics, and simplifies symbolic machine states.
Industrial low-level cryptographic assembly proofs remain underrepresented despite their security and reliability relevance.

4 S2N-BIGNUM-BENCH CONSTRUCTION

The benchmark extracts theorem goals from the open-source s2n-bignum repository and supplies self-contained HOL Light contexts for proof synthesis. Problems are categorized by goal type and can be developed interactively through OCaml tooling.

Each task is extracted from a top-level HOL Light theorem binding while its original proof body is replaced by CHEAT TAC.
The accompanying context inlines required OCaml modules, definitions, constants, and previously proved results to reproduce the source proving environment.
Problem identifiers combine architecture, filename, theorem name, and occurrence index to distinguish repeated theorem names.
The benchmark contains 311 bit-vector, 552 program-state, 859 functional-correctness, and 562 generic problems.
HOL Light artifacts can be used with interactive development environments built on the OCaml REPL.

5 EVALUATION

The benchmark validates submitted HOL Light proofs through syntax, integrity, and kernel-checking procedures, while restricting access to original proof bodies. A preliminary GPT-5.3-Codex baseline completes 4.4% of problems in medium-effort mode and 5.3% in high-effort mode.

Answer submission and grading: Submitted proof expressions undergo syntax and type pre-checking before full evaluation, catching malformed tactics and immediate parser or type errors.The pre-check compiles a generated .synchk.ml file containing the submitted expression in the benchmark context.
Answer submission and grading: Each problem receives one of five verdicts—OK, FAIL, CHEATING, TIMEOUT, or ERROR—and binary kernel-checked proof completion is the primary metric.Official comparisons should fix the proof-check timeout, hardware setting, and submission budget.
Integrity and contamination defenses: The model is not given original proof bodies or tactics from other theorems, although it may receive machine-code context needed to understand each specification.This restriction is intended to preserve benchmark validity.
Initial baseline experiments: 4.4% binary proof-completion rate is achieved by GPT-5.3-Codex in medium-effort mode, rising to 5.3% in high-effort mode over the full benchmark.The authors describe these figures as a preliminary baseline rather than an exhaustive estimate of current model capability.
Integrity and contamination defenses: The evaluation rejects submissions using CHEAT TAC or introducing forbidden axioms, checking HOL Light’s axioms() output before and after execution.A changed axiomatized-theorem list marks the result as CHEATING.
Integrity and contamination defenses: An OCaml parser rejects syntactically complex submissions that do not form one valid expression before proof evaluation.This defense targets attacks resembling SQL injection.

6 CONCLUSION

s2n-bignum-bench benchmarks machine-checkable proof synthesis for deployed low-level cryptographic assembly in HOL Light. Its current release focuses on functional correctness, with relational properties identified as a future extension.

6 CONCLUSION: The benchmark evaluates whether systems can construct sound proofs about real low-level implementations under trusted ISA semantics.It is intended as a reproducible testbed beyond competition mathematics, using isolated artifacts, offline evaluation, and integrity checks.
6 CONCLUSION: The current release focuses on functional correctness, while constant-time discipline and equivalence properties suggest future extensions beyond extensional correctness.The passage connects these relational properties to recent HOL Light developments around s2n-bignum.

A A GUIDE FOR CHALLENGERS

The official repository provides setup guidance for exploring the benchmark problem set.

A A GUIDE FOR CHALLENGERS: The official repository walks challengers through benchmark setup and points to the experimental protocol overview as a starting place.The guidance is intended to help users begin exploring the problem set.

A.1 EXPERIMENTAL PROTOCOL OVERVIEW

The preliminary experiments assess whether language models can synthesize HOL Light tactic proofs using the benchmark workflow and a closed-source reasoning model accessed through Codex-CLI.

A.1 EXPERIMENTAL PROTOCOL OVERVIEW: Preliminary pass@1 experiments evaluate whether current language models can synthesize HOL Light tactic proofs for s2n-bignum-bench.The experiments follow the benchmark workflow described in the repository documentation.
A.1 EXPERIMENTAL PROTOCOL OVERVIEW: The primary reported baseline uses a closed-source reasoning model accessed through Codex-CLI, with the zero-shot prompt and evaluation scripts available in the official repository.The configuration provides the stated baseline protocol for the experiments.

A.2 BENCHMARK PREPARATION AND PROBLEM RETRIEVAL

The benchmark is built by extracting theorem metadata from pinned HOL Light and s2n-bignum sources, yielding 2,284 standalone problems. Each problem includes a boolean goal and the setup needed to establish its HOL Light proof context, and problems can be retrieved in two equivalent formats.

2,284 problems are extracted from pinned HOL Light and s2n-bignum sources as the benchmark corpus.The construction follows the repository workflow and extracts theorem metadata before packaging problems.
Each problem contains a HOL Light boolean term in query.txt and a setup.ml preamble for establishing its proof context.
Problems can be retrieved either as a flat CSV or as a directory tree containing problem-specific query.txt files.The two retrieval formats are provided as equivalent options for inference.

A.3 PROMPTING AND INFERENCE PIPELINES

The pipeline uses a standardized zero-shot HOL Light prompt and evaluates generated tactic expressions through staged syntax checking, proof execution, and verdict collection. It profiles human proofs to assign bounded per-problem timeouts, then reports preliminary GPT-5.3-Codex results of 4.4% and 5.3% proof completion in medium- and high-effort modes.

A.3 PROMPTING AND INFERENCE PIPELINES: The zero-shot prompt asks the model to prove a HOL Light boolean term in THEN form without CHEAT_TAC or new_axiom.It includes one worked example and requires only a tactic expression as output.
A.3 PROMPTING AND INFERENCE PIPELINES: GPT-5.3-Codex is run through codex-cli in a restricted read-only sandbox, with responses recorded alongside problem identifiers and metadata.Unexpected tool-related CLI events are logged for auditing but not used in evaluation.
A.6 CONSTRUCTION OF THE PROBLEM TIMEOUT MAPPING: Per-problem timeouts are derived by repeatedly profiling ground-truth proofs because proof-check times range from milliseconds or seconds to multiple hours.The measured prove secs value captures proof execution inside HOL Light while excluding compilation overhead.
A.6 CONSTRUCTION OF THE PROBLEM TIMEOUT MAPPING: Light and heavy problems receive different safety margins, with each timeout bounded between 120 and 10,800 seconds.The map uses runtime categories and variance-aware scaling instead of one blanket timeout; category defaults remain a fallback for unprofiled problems.
A.7 EVALUATION PIPELINE: The challenger may use its own inference strategy, but evaluation expects one answer.txt file under each problem-id directory.
A.7 EVALUATION PIPELINE: Evaluation proceeds through syntax checking, HOL Light proof execution with axiom-count checks, and collection of one verdict per problem.Verdicts are OK, FAIL, CHEATING, TIMEOUT, or ERROR.
A.7 EVALUATION PIPELINE: 743 medium-effort and 766 high-effort answers passed syntax checking and reached proof execution out of 2,284 problems.Answers that did not compile as valid OCaml/HOL Light tactic expressions were excluded at the syntax-check stage.
A.7 EVALUATION PIPELINE: 101 / 2,284 problems (4.4%) were solved in medium-effort mode versus 121 / 2,284 (5.3%) in high-effort mode, a gain of +20 proofs.The gains concentrate in program state (+12) and generic (+7) categories; aggregate timeouts and errors were 44 and 3 versus 47 and 4.