To pizlonate is to make Fil-C's checks explicit: turn unchecked IRchecked IR nanofilThe two stages of the IR. Unchecked IR leaves Fil-C's checks implicit in every load and store at a p address; checked IR states every check, every raw access and the proof it uses, so the validator can see that each access is covered. A module's stage is read off its vocabulary, never a flag (ir:module_stage/2). into checked IR, each access becoming a checkcheck Fil-CAn access check: check(Lo, Hi, Rights, Align) of a pointer P traps unless P's capability permits Rights on [P+Lo, P+Hi) with P+Lo Align-aligned, and otherwise yields P as a proof of class a. check_local does the same for a named local, and check_function yields a function proof of class f (ir:op_kind/2, pizlonate:checked_access/4). and a raw accessraw access nanofilA raw access is a checked-stage memory access that does no checking of its own and names the proof that covers it: raw_load, raw_store, raw_load_pointer, raw_store_pointer, raw_cas and raw_call (ir:covered_access/6). that names its proofproof nanofilA proof is a temporary of class a or f, the result of a check: it holds the checked pointer itself and certifies that the check passed. A raw access names the proof it relies on, so evidence is structural (ir:proof_use/6)., and each pointer operation a flightflight nanofilA flight builds a pointer from two independent sources: flight(D, Op, Args, Lower) computes D's address with copy, add or sub over l values and pointer addresses, and takes its capability from the pointer Lower names, or none (pizlonate:flight_inst/2). Making the pair proves nothing about access; no check, getter, memory access or safepoint happens inside it. (after FilPizlonator, Fil-C's LLVM pass; pizlonate:pizlonate_module/2pizlonate.plpizlonate_module+M₀, -MdetM is the unchecked module M0 with every check explicit and a poll on every edge to a block at or before its source in block order. In a plain module, whose addresses are not Fil-C pointers, only the polls are added.).

The pizlonation oracle compares the unchecked and checked runs in the interpreterinterpreter nanofilThe interpreter is interp.pl, nanofil's executable meaning of the IR: a relation from a module, a function, arguments and fuel to an outcome, with CLP(Z) integers so that it runs in every direction. The Rocq model transcribes it, and the outcome gate checks that the two agree on every run line of the corpus. (main:pizlonation_verdict/4main.plpizlonation_verdict/4not documented). The formal model starts at pizlonation's output. See pizlonation.md.