An outcome is how a run ends: a return, unreachable, undefined behaviour, a traptrap Fil-CA trap is a Fil-C check failing, which upstream calls a Fil-C panic or safety error (filc_safety_panic): the run ends trap(Reason), terminal and uncatchable. Because nothing follows it, a check is a pure assertion, which is why a check proved never to fail can be deleted without changing behaviour., 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)., or running out of 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).. interp.pl and the model give the same outcomes term for term, which is what the outcome gate compares.

outcome is defined in Semantics.v; Transport.v's eoutcome encodes it back as interp.pl's term. interp.pl also has unknownasmM, Xs for asm_fixed, outside the core subsetcore subset nanofilThe core subset is the part of checked filc-mode IR that the Rocq model runs and validates: the integer, pointer and proof classes, floats, check and every reuse form, the raw accesses, flight, poll edges, direct calls, check_function with raw_call, free, named locals and variadics. A function that uses anything else decodes to IOutside..

unchecked is the one a valid module never reaches (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., valid_no_unchecked). Campaign 7 sorts the others into panics and not: formal.md, What counts as a panic.

The subtlety: in the model UB comes only from an invalid float-to-integer conversion; plain mode's ubout_of_boundsA, Size is outside the subset.