A run is the execution of one function of a module from its initial memory, step after step, to an outcomeoutcome nanofilAn outcome is how a run ends: a return, unreachable, undefined behaviour, a trap, unchecked, or running out of fuel. interp.pl and the model give the same outcomes term for term, which is what the outcome gate compares. or forever. The theorems quantify over every state a run reaches, not over its outcome, so a run that never ends is covered too.

• Prolog: interp:run/5interp.plrun+M, +Fn, ?Args, +Fuel, ?OutcomenondetOutcome is the result of calling the function Fn of module M on Args and executing at most Fuel blocks. With unknown Args each solution constrains them to the inputs that take one path; see run_prepared/5. prepares the module and runs the function under a fuelfuel nanofilThe interpreter's bound on executed blocks: each block entered costs one unit, and running out ends the run out_of_fuel, which proves nothing (interp:run/5). bound.

• Rocq: Run.v's Driver runs over any runtimeruntime Fil-CThe runtime is what Fil-C does around one thread's program, natively libpizlo.so with FUGC: where a new object goes, what free does, and what the collector may change while the program waits at a safepoint. The model does not define it; it states it as one page of axioms, Module Type Runtime (Runtime), each with a native test in tests/c/prog/axiom-*.c., from initial_memory, by run and run_steps; Semantics.v's reachable and Machine.v's mreachable are runs as relations. ExternalMachine.v adds labelled runs through external callsexternal call nanofilAn external call is a call to a symbol the module does not define, in practice libc. The core model sends only free to the runtime and is stuck at every other. A contract is Campaign 4's trusted description of one external function: its ABI, the caller's premises, the roots it may write, what it may release or allocate, its observations and its endings..

• The theorems' form: "along every run of a checked module that starts readyready nanofilA runtime is ready in a memory when its own state and that memory agree well enough that its next allocation is fresh. Readiness is the runtime's invariant: the axioms about allocation and the address space are stated only for ready states.", as in soundnesssoundness of checking nanofilSoundness of checking is the validator's theorem: every run of every valid checked module avoids unchecked, so the checks the validator demands, and those it lets a pass remove or reuse, are enough, and a check that fails is the run's whole story. It does not say a check never fails: a module that reads past an array is valid and traps.'s valid_no_unchecked.

The subtlety: two bounds. The run's own fuel counts blocks entered and ends with out_of_fuel, which proves nothing; the extracted driver's gas, taken by run_steps in halves up to 2^60 steps, is never the limit in practice. Campaign 7 quantifies over reached states so that neither plays a part.

Defined in Run.v and Machine.v.