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

Recent progress in neural theorem proving has been driven largely by mathematics-oriented and, more recently, by verification-condition and repository-scale benchmarks. These settings are valuable, but they do not directly test whether a model can synthesize machine-checkable proofs about concrete low-level implementations under an industrial proof-engineering stack. We address this gap with *s2n-bignum-bench*, a benchmark derived from AWS *s2n-bignum*, a formally verified library of hand-tuned big-integer assembly routines for ARM and x86. The current corpus packages $\mathbf{2{,}301}$ HOL Light proof obligations as standalone `setup.ml`/`query.txt` tasks spanning big-integer arithmetic, elliptic-curve routines, ML-KEM, SHA-3/Keccak, and shared ISA infrastructure. Each task reproduces the relevant proving environment, exposes the theorem statement to be proved, and expects a tactic expression that is accepted by HOL Light within a fixed timeout. The benchmark spans five categories so that one can separate generic HOL Light fluency from ISA-specific reasoning. We release the extraction pipeline, retrieval utilities, an offline evaluator with syntax/type pre-checking and integrity checks based on axiom-difference and forbidden-tactic detection, paired verbatim and obfuscated query variants, and a checkpointed assessment workflow to support iterative feedback-driven $\operatorname{pass}@K$ studies and future step-level proof construction workflows. Initial zero-shot baselines using GPT-5.3-based and other frontier models solve at most $\mathbf{6.35}$% of the problem set (when provided only with the goal term), highlighting the difficulty of HOL Light tactic synthesis for low-level verification obligations under trusted ISA semantics. The code to set up and use the benchmark is available at [s2n-bignum-bench](https://github.com/kings-crown/s2n-bignum-bench).