\paragraph{Undefined behaviour and fuzzing harnesses.}
\label{sec:ub}
Run on our C semantics, the test programs of tiny-regex-c and cJSON reach two cases of undefined behaviour that
GCC~15.2 builds with the default sanitizers do not show: forming a pointer one element before a string literal in
\code{matchstar}, and comparing pointers into distinct objects in \code{cJSON\_SetValuestring}~\cite{cjson919}. On the
OSS-Fuzz harnesses that Theorem proved at the binary level~\cite{theoremossverify}, agents and the orchestrator proved
in Lean~4 that, in our C semantics (where allocation always succeeds and library calls run our models), the unmodified
cJSON 1.7.18 harness terminates without undefined behaviour below $2^{61}$ bytes (proved across four versions of the
semantics, after a parse-only variant below $2^{63}$ bytes) and the unmodified yajl-ruby 1.4.3 harness does so below
$2^{31}$ bytes. Three further theorems cover copies with a small source change: with seven lines added to
\code{print\_string\_ptr} in cJSON 1.7.18~\cite{cve202616554}, the whole-harness statement holds below $2^{63}$ bytes on
64-bit and below $2^{31}$ bytes on a 32-bit build, and with one line changed in \code{yajl\_lex\_number}, that
function's contract holds across all \code{unsigned int} lengths below $2^{32}$. All of these harness theorems lie
outside the pre-registration (which covered a seed-corpus sweep and an unfinished attempt on yajl-ruby), use only
Lean's three standard axioms and pass kernel replay; the technical report gives the effort tables, the static-scan
bounds and the per-version module counts.