Projects

Some stuff I’ve worked on.

ChainCert — Proof-producing computation in Lean 4 and Sage. Sage emits a certificate of its computation of the homology groups of a simplicial complex and the Lean kernel checks it independently. Right now it does Smith normal form and simplicial homology. Docs.

Lean-HoG — (Contributor) A Lean 4 library for verified computational graph theory. I fixed bugs in the build, path resolution, widgets, and certificate scoping.

ScenicProver — Contract-based verification for autonomous systems, built on Scenic.