Testing

A test that cannot fail on the bug it targets is not a witness.

Horus has been bitten by gates that passed because they checked the property the author had in mind. The 2026-07 critical finding did that. The rule since is mechanical. .github/gate-pairs.yml pairs each gate with the arm that restores the defect. The arm must go red. A marker the test looks for is one write, so a torn line cannot be counted twice. A boot that dies before the interesting line is not a pass.

260 QEMU integration targets, and 360 control arms that must go red

Those two figures are derived from .github/gate-pairs.yml. Adding them together and calling the sum "tests" hides which layer you mean. The Makefile names 620 smoke-* targets. The run page states that count in the place the checker reads.

159 security properties, and 44 Kani proofs gate a merge

Every row in SECURITY.md names a witness that exists. tools/check_invariants.py fails the build otherwise. A witness that is only a positive boot, with no control arm, is named in .github/positive-boot.yml. The same job fails if that list and the table disagree. The census does not add the arms (roadmap 4.21). The Kani harnesses are classified in .github/kani-harnesses.yml, and every one of them gates. Miri runs the Rust tests that are in scope, and the scope file says which modules it skips and why. A proof whose nightly arm comes back successful has become vacuous: an assumption ate the inputs that mattered.

What this does not prove: the kernel as a whole, a refinement down to the C, or the filesystem server. Formal verification is narrow. That is limitation 5.5, and it is open.

The nightly jobs are real, and they do not block a merge.

Fuzzing runs each Rust parser target for ten minutes. A crash fails the run and uploads the input. The Kani control arms re-run every recorded mutation and require the proof to fail. The ruleset audit compares the live branch ruleset with the checked-in classification. The compare timing run times the password compare and the AEAD tag compare, and fails if its clock cannot separate a planted variable-time compare of the same length. It does not show the primitives are constant-time. That is limitation 5.4, and it is open. A red run of the fuzz workflow or the Kani control arms opens one issue, and does not open a second while that issue is open. A nightly Clang build links the kernel and the userspace that kernel includes, and fails if the compiler is missing or the link produces no kernel. It does not gate a merge. None of these runs on a pull request, so none of them can be a required check. They are listed as exemptions on purpose: deleting the workflow is a failed classification, not a silent pass.

The pull-request installs of PyYAML accept only the files recorded for version 6.0.3. A wheel that claims that version and is not in the list does not install.