A 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 validatorsvalidator 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. judge each, and must agree.

• rocq/mutants.pl prints up to 150 mutants per item; judge_valid applies each change, computes valid_items of the whole module and compares it with 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 verdict; rocq/valid.sh runs it.

• The mutation campaign is the full matrix, checks.x86_64-linux.nanofil-rocq-full, run only when asked. The routine check sets NANOFIL_MUTANTS=0 and compares base verdicts only.

• Mutants test rejection as well as acceptance; eight bugs planted in Validate.v were each caught.

The subtlety: a mutant is outside, not judged, when it is itself 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., or changes a signature, data or alias that an outside function refers to.

See rocq.md, The validator and its gate.