People ask what it's like to write a kernel in Rust. The honest answer: writing it is fine. Testing it is a different problem.
A normal Rust application fails loudly. A kernel fails quietly — and takes everything else with it. So when I started building the Cyphera Kernel, I knew I'd need more than unit tests.
Here's what I actually use.
Rust's type system is not enough
I know, I know. Rust is supposed to prevent memory bugs at compile time. And it does — for safe code. But a kernel has to touch hardware. Map memory. Manage page tables. Issue syscalls. That means unsafe, and unsafe means the compiler stops holding your hand.
For the Cyphera Kernel, all unsafe is isolated inside a single layer called frame/. The kernel/ crate is #![forbid(unsafe_code)] — it cannot physically call unsafe code directly. Only frame/ can. This is the framekernel pattern: quarantine unsafe into a controlled pool, build the rest on top of it.
But quarantining unsafe doesn't prove it's correct. For that, you need different tools.
MIRI: your tests, run under a memory interpreter
MIRI has been part of the Rust toolchain since around 2019-2020. It's still officially marked "experimental." A lot of experienced systems programmers haven't heard of it — not because they missed something, just because it didn't exist when they built their mental models.
MIRI is an interpreter for Rust's MIR — the compiler's intermediate representation. Run your test suite under MIRI and it checks every memory operation at runtime: use-after-free, out-of-bounds access, data races, undefined behavior.
It's slow. You don't run MIRI on your hot path. You run it on the tricky stuff: allocator logic, synchronization primitives, pointer arithmetic in frame/.
The Cyphera Kernel has 153 or more MIRI tests. Nothing glamorous about that number — it's just the test suite we run under MIRI instead of native execution. When a MIRI test fails, it's not "wrong answer." It's "this code invokes undefined behavior."
That's a different class of bug.
Kani: proving properties, not just testing inputs
MIRI catches bugs in code you exercise. Kani proves properties hold for all inputs within a bounded model — a fundamentally different guarantee.
Kani is a bounded model checker built by AWS, first released publicly in 2022. If you learned Rust before 2023 you may have zero exposure to it. It's not obscure — it's just that new.
Here's a concrete example from the kernel. The frame allocator's core invariant: no two live allocations ever overlap. A unit test can verify this for a handful of scenarios. Kani proves it for all possible inputs simultaneously.
#[kani::proof]
fn try_alloc_preserves_no_overlap_one_region() {
let mut t = one_region_tracker(); // symbolic — kani::any() inputs
assert!(t.no_overlap_invariant());
let req_start: u8 = kani::any();
let req_len: u8 = kani::any();
let ok = t.try_alloc(req_start as u32, req_len as u32);
assert!(t.no_overlap_invariant()); // still holds, for every possible input
}kani::any() generates a symbolic value representing every possible u8. The SAT solver either finds an input that breaks the assertion, or proves no such input exists.
Another one I like: the lock hierarchy. Deadlocks in kernels happen when two threads acquire the same locks in different orders. The Cyphera Kernel has a documented lock hierarchy — Global → CPU runqueue → vmspace → futex table → ... — and Kani proves the order-checker enforces it correctly:
#[kani::proof]
fn vmspace_then_global_rejected() {
let mut h = HeldSet::empty();
assert!(h.try_acquire(LockId::Vmspace));
assert!(!h.try_acquire(LockId::Global)); // must be rejected
}That's not a test. That's a proof. The deadlock pattern cannot happen, by construction.
118 or more Kani proofs, covering the frame allocator, VMA bookkeeping, signal masks, seccomp filters, ELF relocation, futex bit-set logic, and more.
Fuzzing: because parsers eat attacker-controlled input
MIRI and Kani test your logic. Fuzzing tests your parsers against an adversary.
Fuzzing itself isn't new — AFL has been around since 2013. But cargo-fuzz, the Rust-native harness, only appeared in 2017. The ergonomics for Rust are recent even if the concept isn't.
The ELF loader is the first thing the kernel calls when executing a binary. An attacker who can craft a malformed ELF can potentially crash the kernel at exec time — before your process even starts. So we fuzz it:
fuzz_target!(|data: &[u8]| {
let elf: ElfFile<FileHeader64<Endianness>> = match ElfFile::parse(data) {
Ok(e) => e,
Err(_) => return, // graceful reject, fine
};
// Walk program headers, section headers, borrow segment bytes —
// anything that panics or crashes on arbitrary input is a finding.
for ph in elf.elf_program_headers() { ... }
});24 or more fuzz harnesses. ELF parsing, BPF programs, ext4 directory entries, inodes, superblocks, clone() argument decoding, socket address parsing, TAR archives. All the places where the kernel reads data it can't trust.
The honest state
153 or more MIRI tests, 118 or more Kani proofs, 24 or more fuzz harnesses, 58 or more userland syscall exercisers. That's where we are.
Is it enough? No. The full lock-order runtime assertions aren't done yet. Kani's SAT bounds mean some proofs model 1-2 elements where the real data structure is unbounded — the invariant holds by argument and audit, not by proof. There are corner cases we haven't found yet.
And when something does break, we'll know which layer it came from.
Would we go further?
Yes. Obviously. Full seL4-level formal verification — machine-checked proofs, TLA+ for concurrency invariants, the whole thing — is the dream. Firms like Galois do exactly that kind of deep work, and we'd love to work with them someday. We're also a bootstrapped one-person startup, so… Patreon TBD.
For now: MIRI, Kani, and fuzz. It's not seL4. It's what we could build, doing it right, with the best tools available in 2025. Whether we got it right is a question we'd genuinely love someone like Galois to answer.