Soundness of checking is the validator's theorem: every run of every valid checked module avoids uncheckedunchecked nanofilunchecked(Why) is the outcome of a raw access its capability does not allow, or of a reuse form whose trust was false: a check was missing or too weak, which only a broken pass produces. It is neither undefined behaviour nor a trap, so it refines nothing (interp:raw_res/2)., so the checks the validatorvalidator nanofilThe validator decides whether a module is well formed and, in checked IR, whether every access is covered by evidence that still holds. Every producer of checked IR must get its output past it, and Soundness.v proves that a module it accepts never runs to unchecked. 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.

• valid_no_unchecked in Soundness.v, over every 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., with the hypotheses that the module is checked by Validate.v's valid and that the run 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. (sparesspares nanofilspares says that at a safepoint just before an instruction the evidence pass keeps facts across, the runtime changes no region. Every runtime meets it, so the generic soundness theorem, once stated under it, no longer takes it as a hypothesis., once a hypothesis too, is a lemma for every runtime, spares_any); interp_valid_no_unchecked is its instance under the interpreter's runtime, closed. Its proof hands each source of unchecked to a run theorem: run_doomed_checked, run_access_checked, run_reuse_checked, run_guard_checked, and the axiom free_checked.

• On the Prolog side it is the claim that ir:valid_module/1ir.plvalid_module+MsemidetM is a well-formed module. When it is not, throws nanofil_error(Message) describing the first problem found, so callers get a diagnostic rather than a silent failure. A few terms outside the grammar (an item, instruction or jump of no known shape) make it fail instead.'s rule is sound, which ir.pl argued and the mutantmutant nanofilA mutant is a checked module with one item changed, inserted or deleted: a check deleted or moved, its bounds, rights or alignment changed, a raw access's offset moved by one, a free inserted between evidence and its use, a reuse form given another proof, a poll edge removed, or a data object's or alias's linkage, target or name changed. Prolog's and Rocq's validators judge each, and must agree. gate tests.

Not to be confused with trap-freedom of one program, Campaign 7's never_panics, which is per program and builds on this. External calls other than free are stuck, so the theorem says nothing past them.

See rocq.md, No run is unchecked and formal.md, The claims, kept apart.