The glibc spike (rocq/glibc, docs/glibc-ir.md): programs linked with nanofil's IR of user glibc units, proved through the program logic, with libpizlo's zsys_write as the one trusted contract. Off the main path: nothing else imports these files, and neither the quick gate nor CI builds this.

nix build -L .#checks.x86_64-linux.nanofil-glibc

It compiles the proofs against the model's compiled theories (the nanofil-rocq model's objects), printing each file's time, reads every sentence back with parse.sh (web/rocq), and runs the native probe of the zsys_write contract with filcc. That the Code.v fixtures are nanofil's current products is rocq/glibc/code.sh's check, which needs the user glibc capture (survey/glibc/capture.nix) and is run by hand.