sketches of different programming language ideas

A formal verification of an abstract SAT solving transition system.

Tiny fast HTML5 game engine with many features and no dependencies.

Auto formalization of the CLRS text book

Because `model.fit()` isn't an explanation

A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.

A certified RISC-V Interpreter with Hoare-logic in Lean

A minimalist HDL built entirely from logic gates for education and experimentation. Compiles circuits to C so that they can run anywhere

Completeness of the Iris separation logic framework

Formalizing the stable marriage problem and the Gale-Shapley algorithm in Lean

The mechanized formalization of logical pinning, a lightweight borrowing model and proof discipline for precise reasoning about container-internal pointers.

OCaml .mlx syntax dialect with JSX syntax expressions

From Zero to QED: An informal introduction to formality with Lean 4

Library for structural temporal logic proofs over coinductive, free monads with effects and choice.

Trace monoids in Cubical Agda

Code and Materials for an interactive online course on Logic (part of Strathclyde's CS208 Logic and Algorithms module)

ProbLog is a Probabilistic Logic Programming Language for logic programs with probabilities.

Formalizing RFC 9535

Modern scientific computing for OCaml

OCaml - Oxidized!

Description of Model Checking Intermediate Language

Functions and proofs about game trees in Rocq, implemented as rose trees.

SMTscope automatically analyses and visualises SMT solver execution traces.

The source of Walnut

The Walnut Theorem Prover webpage

A regex crate using Brzozowski derivatives.

Artifact generator for the paper "Incremental Forward Reasoning for White-Box Proof Search" (submission to CADE 30)

Can I make an *optimizing* compiler under 1k lines of code?