The logic spikes (rocq/spikes, docs/logic.md): the same program proved never to panic by a hand-rolled logic, by Iris on an early language, and by the program logic in theories (Logic.v). Off the main path: nothing else imports them, and the quick gate and CI do not build this; the program logic itself is in the model.

nix build -L .#checks.x86_64-linux.nanofil-logic-spikes

It checks that ListSumCode.v is what nanofil makes of listsum.c, then compiles the spikes against the model's compiled theories (the nanofil-rocq model's objects), printing each file's time. Then parse.sh reads every spike sentence back (web/rocq), with its Iris fixture.