Tiny verified SAT-solver

Compilation and Verification of Data-Centric Languages

Limbo is a work-in-progress, in-process OLTP database management system, compatible with SQLite.

Monadic Constraint Programming framework

A PPX deriver that automates differential testing for OCaml modules

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

A fast and ergonomic concurrent hash-table for read-heavy workloads.

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

A language for mental models

Simple, boilerplate-free operations on tree shaped data types. Port of the Uniplate Haskell library into Rust.

JSON in Coq

Wasm Analysis Framework For Lightweight Experiments

A Gallina compiler with C 17 as an intermediate representation

Direct proof that strict orders on listable types are well-founded

Verified Chess Verifier

Ph.D. development - CompCert with symbolic values

Irmin is a distributed database that follows the same design principles as Git

Verified Rust for low-level systems code

Runtime and runner for a compiler from SQL to JavaScript

An LR(1) parser generator and visualizer created for educational purposes.

An implementation of the Karp-Miller coverability tree algorithm in Haskell

Source code for my Master's Thesis

VSCode extension that is designed to help automate writing of Coq proofs.

Using CertiCoq to implement a library for formally verified set in C

VimR — Neovim GUI for macOS in Swift

SMT solver for theory of uninterpreted functions with equity