SMT x86_64 TSO model checking and minimum fence synthesis
seL4 pager with proven memory isolation and frame reuse
Verified pixel compiler for TempleOS in Isabelle/HOL
Verified branch relaxing assembler in Isabelle/HOL with provably minimal bytecode layouts
OCaml tooling for tracing Xen guest address translation
Monorepo for Tangled
mrrrp mrrrp brrr formal verification go brrr