All systems
Being builtoperating systems2026

workaOS

This is the deepest thing we build, and it is why the rest comes out right. workaOS does not lean on Linux: it is a no_std kernel that boots through the Limine protocol, requests its own framebuffer and works identically under BIOS and UEFI. On top sits a capability model where authority is granted explicitly and everything else is denied, plus an append-only hash-chained log: if something had an effect, there is an entry that proves it.

Stack

  • Rust no_std
  • Limine
  • QEMU/KVM
  • virtio-vsock
  • virtio-blk
  • Kani
  • SMP

Receipts

No receipt, no effect.

  • Boots under both BIOS and UEFI, with verifiable serial outputCheck it with: scripts/qemu-test.sh --firmware bios | --firmware uefi
  • The image rebuilds bit-for-bit identicalCheck it with: scripts/repro-check.sh
  • The ledger hash chain is verified at runtimeCheck it with: cap::ledger::verify_chain()
  • No authority means no dispatch: deny is the defaultCheck it with: cap::table — missing_authority_never_dispatches
  • Real Chromium inside a microVM over real vsockCheck it with: qemu-test.sh --test cu1b_chromium → CU1B-CHROMIUM-OK
  • The kernel audit runs strict, with zero pending rowsCheck it with: node gates/reaudit-os.mjs --strict

What we do not claim

We do not claim formal verification. The Kani harnesses are written but do not run as a gate, and that is stated in PROOFS.md rather than hidden. An invariant passing under QEMU is evidence, not a proof over all possible inputs.

Talk to usAll systems