The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).

The Z3 Theorem Prover

Libraries useful for Dafny programs

The Rosette solver-aided host language, sample solver-aided DSLs, and demos

a proof-of-concept programming language based on Call-by-push-value

Extensions to the cubical stdlib category theory for categorical logic/type theory

Verified Rust for low-level systems code

Pokémon battle simulator.

A webapp that reads your articles to you while you're on the subway

Scalable Architecture for SMR Protocols

How to create an OS from scratch