mrrrp mrrrp brrr formal verification go brrr

Monorepo for Tangled

OCaml tooling for tracing Xen guest address translation

Verified branch relaxing assembler in Isabelle/HOL with provably minimal bytecode layouts

Verified pixel compiler for TempleOS in Isabelle/HOL

seL4 pager with proven memory isolation and frame reuse

SMT x86_64 TSO model checking and minimum fence synthesis