The extracted Rocq validator as a gate on the compiler's -O products (rocq/gate.sh, docs/rocq.md): every checked module nanofil -O gives its backend, for the IR and C corpus (tests/, cproc, c-testsuite) and for each translation unit of GNU hello, zlib, Lua and SQLite, goes to the model's --module mode, which judges it as Validate.v's [valid] does, the validator Soundness.v's [valid_no_unchecked] is proved sound for. The check fails on any module the model rejects; modules with functions outside the model's subset are counted, not failed.

nix build -L .#checks.x86_64-linux.nanofil-rocq-gate

The driver is rocq.nix's model.driver, which needs only Extract.v's import closure, 14 of the theories, each its own derivation; it does not wait for the rest of the model. The packages compile once each, in their own derivations, through nanofil-cc's terms mode, which takes the objects from filcc so the builds still link; only src/ and bin/ reach them.