A capability-secure operating system derived from mathematical first principles — designed, machine-checked, implemented, and booted on bare metal.
VERA (Verified, Effect-typed, Reference-capability Architecture) began as one question: can an operating system be "solved" mathematically? You can't derive a single provably-optimal OS — it is a multi-objective problem with no total order — but you can derive a coherent design from theory, prove its core properties, implement it, and run it. This repository is that full arc, from a theorem to a kernel that enforces the theorem on a machine with no other software on it.
Author: Ideatrino
- docs/ — Architecture, formal core (calculus + theorems), and completion.
- reference/vera_proof.py — The noninterference core, machine-checked in Z3 over an arbitrary lattice.
- reference/ — A running kernel + adversarial fuzzer, EDF scheduler, persistence, and covert-channel meter (dependency-free Python).
- kernel-userspace/ — A Rust kernel where forging a capability is a compile error.
- kernel-baremetal/ — The proven model booting in 64-bit long mode, enforcing its guards with no OS beneath it.
Most OS security is bolted on: a process runs with all your authority, so one bug in a PDF viewer can read your keys. VERA makes unauthorized action unrepresentable rather than merely forbidden. Authority exists only as unforgeable capabilities; a program cannot name what it was not handed. An information-flow lattice tracks taint, so once you read a secret you cannot write it anywhere a lower observer can see — a property (noninterference) this repo proves, not just tests.
Machine-checked proof (the headline): cd reference && pip install -r requirements.txt && python3 vera_proof.py
Full reference suite: cd reference && python3 run_all.py
Compile-time unforgeable capabilities (needs Rust): cd kernel-userspace && cargo run
Boot the bare-metal kernel (Linux/WSL, rustup nightly + qemu + grub): cd kernel-baremetal && rustup target add x86_64-unknown-none && ./build.sh
Proven: the noninterference unwinding conditions, machine-checked in Z3 for every lattice (reference/vera_proof.py); confinement and other guards enforced structurally.
Assumed: in the bare-metal kernel, unforgeability is enforced by Rust module privacy, not a formally verified microkernel on capability hardware. Production VERA would build on an seL4-class kernel and CHERI-class silicon.
Fundamentally open (uncloseable by anyone): covert timing channels are bounded, never zero — reference/vera_covert.py measures the residual in bits/second; and undecidability caps automated verification of arbitrary programs. Physics and mathematics, not to-dos.
Stands on real research: seL4, CHERI, KeyKOS/EROS, HiStar/Asbestos, the Decentralized Label Model (Myers & Liskov), and the Goguen-Meseguer/Rushby unwinding theorems. Its contribution is the synthesis and the end-to-end demonstration from proof to boot.
Proprietary — All Rights Reserved. Copyright (c) 2026 Ideatrino. Source-available for personal evaluation and academic study only; any commercial use requires a paid license from the author — see LICENSE.