Limitations

These are the limits that should change a decision.

Horus is research-grade. It should not be trusted with anything you cannot afford to lose. The gating set is 147 checks with 12 exempted. The 12 are the contexts of the workflows that do not run on a pull request, not twelve unused jobs. Each security property names a witness. A witness that is only a positive boot, with no control arm, is named in .github/positive-boot.yml. That list includes the central dispatch property. The census does not add the arms. The machinery is not a review.

• 5.1Nobody reviews a change before it lands

  The ruleset requires a pull request and does not require an approving review. One maintainer cannot turn that on without either blocking every merge or adding a bypass, and a bypass undoes the gating. The honest claim is thoroughly automatically verified. Roadmap 4.1 waits on a second person.

• 1.23A program's execute right is advisory if you can read it

  SYS_SPAWN_IMAGE runs the bytes it is given. System trees are rebuilt from verified modules and refuse every change. A user's own file, and the output of TCC, can be run by any task that can read it. Closing this is roadmap 5.4: spawn from a file capability that carries EXEC.

• 1.24Below a session root, fs_server is the reference monitor

  The kernel bounds the session by the union of its grants. Inside that union, a bug in fs_server is a bug in the policy. A grant names a path. An account that can create a name can choose the object another account receives. Mode bits do not include the administrator. A capability with no grant set, held by system tasks and not by a login, can rename a file under a grant. Roadmap 5.10, after filesystem phase 2, is the kernel-side bound. It waits on decision D8.

• 2.9A machine with no TPM is not measured, and it says so

  A machine with a TPM halts when measurement fails and refuses to format a volume it cannot seal. A machine with no TPM still boots, says so at install and at every login, and the volume records that it was created with no TPM. Rollback is still open: an unanchored volume is accepted, the counter moves once per boot, and there is no export to another machine (roadmap 5.7). A kernel update still changes the pin and locks the old seal out until roadmap 5.8 reseals first.

• 5.4The cryptography is unaudited and not shown constant-time

  ChaCha20, SHA-256, BLAKE2b, Argon2id and the AEAD are from-scratch no_std Rust with no third-party crate. They wrap the volume key, every block, every password and the CSPRNG. Tests check how they are used. They do not audit the primitives. Writing new primitives is not the fix. An audit, or a vendored hash-pinned implementation, is a maintainer decision (roadmap 5.15). A call-graph check refuses a variable-time compare on the password path and the AEAD, and a nightly run times those compares. Roadmap 4.20 landed that. It does not close this finding.

• 2.12Hardware support is narrow, and DMA is not always confined

  Install works on IDE and on SD or eMMC. SATA is identified and not read or written. NVMe is a self-test. There is no USB, so a machine without PS/2 has no keyboard. One network driver completes ARP and nothing above it. Where the firmware has no IOMMU, a bus-mastering device reaches memory and the boot says so. A build that refuses that configuration is roadmap 5.14. The default research build will keep booting.

• 5.3The releases carry no signature and no provenance

  Five install ISOs, each with a checksum, from an unsigned tag. From v0.4.1-alpha on, the ISO rebuilds to the same bytes from its tag if the compiler, Rust, GRUB, xorriso and mtools match the versions listed beside it. Nobody else has a script that checks that for them yet. Roadmap 4.4 and 4.11.

• 5.5Formal verification covers the security core, not the kernel

  Kani proves properties of capability derivation, lookup, revocation, the ELF validator, the user-address checks, the random pool, the login throttle and the page-pool counts. Every harness gates a merge. There is no refinement proof and no TLA+ specification. Two unsound TLA+ specifications were removed on 2026-09-10. A model of the concurrent protocols, nightly, with a seeded bug in each, is roadmap 5.11.

• G-14Ring 0 still holds the filesystem, the accounts and the loader

  The capability engine is not the whole kernel. The on-disk store, password hashing and program loading run at the same privilege. A defect there is a kernel defect. Moving them out is roadmap 2.7a, and it is not started. The register entry is 1.42.