GIMSO, garbage in, memory safety out, is Fil-C's promise. Fil-C's LLVM pass, FilPizlonator, gives every module a memory-safe meaning, however buggy or adversarial its code. Each operation does what C means or ends in a Fil-C panictrap 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., and no access touches bytes its capabilitycapability Fil-CA capability is the authority half of a Fil-C pointer: which object, if any, its address may be used to access. In the model a capability is an identity, never bounds; the object's current bounds live in its region, so freeing through one alias empties what every alias sees. does not cover. It does not promise that a program never panics, nor does it remove bugs that stay inside memory safety, such as integer overflow or wrong logic.

• nanofil states the same promise in two halves. Pizlonatingpizlonate nanofilTo pizlonate is to make Fil-C's checks explicit: turn unchecked IR into checked IR, each access becoming a check and a raw access that names its proof, and each pointer operation a flight (after FilPizlonator, Fil-C's LLVM pass; pizlonate:pizlonate_module/2). makes every check explicit, and 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. accepts only checked IR whose every access is covered. 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. then proves that an accepted module never makes an access unchecked (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., valid_no_unchecked).

• GIMSO's document describes pointers at rest as if their capabilities lived in a shadow address space. Fil-C implements that space with the auxaux Fil-CAn object's aux allocation, as large as its payload: where Fil-C keeps the lowers of the pointers stored in the object, slot for slot, while their intvals sit in the object's bytes. The aux word in the object header points at it; it is null for an object no pointer was ever stored into, which the collector then scans as a leaf. A pointer store must *ensure* it exists, which may call the runtime; a pointer load reads it. allocation.