Envision a future where every student can read all the code of a teaching operating system.

ABC: System for Sequential Logic Synthesis and Formal Verification

FLINT (Fast Library for Number Theory)

Explicit state logic model checking tool -- 2002 winner of the ACM System Software Award.

The efficient SMT-based context-bounded model checker (ESBMC)

Eurydice compiles (a decent subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.

RISC-V Verification Interface

Nidhugg is a bug-finding tool which targets bugs caused by concurrency and relaxed memory consistency in concurrent programs. It is particularly useful for programs written in C/pthreads. Currently…

Linear-time Temporal Logic guided Greybox Fuzzing (ICSE'22)

OZZ: Identifying Kernel Out-of-Order Concurrency Bugs with In-Vivo Memory Access Reordering

A deterministic, fuzzable pthread implementation

A project to recreate the B compiler for the PDP-11 as authentically as possible

Byzantine model checker

Blackbox Fuzzing of Distributed Systems with Multi-Dimensional Inputs and Symmetry-Based Feedback Pruning

stateless model checking for thread libraries, kernels, and transactional memory

Drop the eBPF verifer