A dynamic language and bytecode vm

Envision a future where everyone can read all the code of an educational operating system.

ABC: System for Sequential Logic Synthesis and Formal Verification

A programming language and model of computation that matches the optimal λ-calculus reduction algorithm perfectly.

FLINT (Fast Library for Number Theory)

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

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

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

property testing and verification front-end for Rust

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