Every build checked
Two checks are only worth something if they run on the kernel that ships. The gate builds sysk's kernel through sysi, runs sysi refine and sysi validate on that same build, and keeps the kernel only if both pass.
What the gate does
make sysk-gate runs tools/sysk-gate.sh on the sysk checkout beside this one (../sysk, or SYSK=...). The script never touches that checkout: it copies sysk into build/sysk-gate/sysk and builds there, with a sysp whose build command is sysi asm --as-c. sysk's own Makefile then runs as usual, and the kernel it links is sysi's. Step through it; the lines of the script that do each step are marked.
The last gate
The last line each check printed, the last time the gate ran in this checkout before the docs were built (build/sysk-gate/refine.txt and validate.txt keep each check's whole report):
When refine says no
sysi refine sorts every function into one of four outcomes: checked, failed (a goal z3 could not prove, or an error), too slow (over --budget-s, which the gate sets to BUDGET, 60 seconds unless given), or not checked (out of scope: today, a function with a cell-swap). It exits 0 only when every function was checked. A function that was too slow or not checked has not failed, but it has not been shown to refine either, so the gate does not pass. Try it:
The scripts
Each says what it does in its first lines (quoted from the files as they are now):
The three single-check scripts and the gate share sysk_build from tools/sysk-build.sh, so they build the kernel exactly as the gate does, each in its own directory under build/. tools/sysk-check.sh is the odd one out: it writes its own wrapper, and runs sysk's whole test suite (raco test tests in the copy) with every kernel the tests build going through sysi, as RV64 assembly by default or as sysi's C with BACKEND=c. It needs QEMU; the gate does not run it.
Both checks lower the program again. sysi refine and sysi validate each take the sources and the build's arguments, not the build's output files: each lowers the sources itself, and validate compiles the result again to get the allocator's map, then checks the ELF the build linked against it. If validate's module were not the one the build compiled, the ELF would not match and validate would fail. What joins the two checks is that both lower the same files with the same arguments: the module refine checks is the one validate checks the machine code against.