Campaign 3's evidenceevidence nanofilEvidence is whatever discharges an access's requirement, the authority over the bytes it touches. Today it is a check immediately before the access, an earlier heap check whose live fact still holds, or a reuse form's trust: for renew a dominating check, for renew_if a guard's span test. invariant over whole runs (docs/formal.md, Campaign 3, Proof persistence; docs/rocq.md, The evidence invariant over runs).

Evidence.v proves ir.pl's evidence passevidence pass nanofilThe evidence pass is the validator's forward walk over a checked function: it tracks live facts and accepts each raw access only where its own check, a live fact or a reuse rule covers it. It visits the blocks once, in order; a block's entry facts are the meet over its incoming edges, with nothing carried over a poll edge or from a block not yet visited. sound one instruction and one edge at a time. This file carries that along every runrun nanofilA run is the execution of one function of a module from its initial memory, step after step, to an outcome or forever. The theorems quantify over every state a run reaches, not over its outcome, so a run that never ends is covered too. of Machine.v's machinemachine nanofilThe machine of a runtime R, MachineR, is what one thread's program sees run under R: Semantics.v's steps, plus R's allocations and R's actions at safepoints. mstep is its step relation and mreachable its runs.: in each state a run of a checked module reaches, the facts the pass computed for the running frame's position hold (inv, stated in Invariant.v), so a raw access the pass accepted by a live fact, or took with its own check, gives no 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). (run_access_not_unchecked). Walk.v reads the pass back block by block and position by position, and Steps.v says what each kind of step does to the frame.

At a safepointpoll Fil-CA safepoint is a point where the thread may run signal handlers and answer the collector. The collector frees nothing the program can name there, but a handler the program installed may free an object under the rest of the program. A pollcheck is a safepoint on an edge: a jump target poll(L), a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1, ir:polls_every_cycle/1). before an instruction the pass relies on facts across, the 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. changes no region: every runtime spares the pass's facts (Invariant.v's spares_any, from Runtime.v's collector_live), so the theorems take no hypothesis about safepoints. Until 2026-11-09 spares was one, because a pointer store whose aux must be allocated exits to the runtime (filc_exit_with_allocation_root in filc_runtime.c), where a deferred signal handler may free the checked object, and the store lands in the freed object's retained memory, safe natively by retention but unchecked in the model. A handler is the program's code, and installing one ends a run in the model, so that case is now a constraint on verifying handlers: one must not free an object whose check is in flight.

Decisions