Research Software

CirC
A compiler infrastructure from high-level languages to zero-knowledge proofs, SMT formulae, and other *existentially quantified circuits*. [code] [paper]
cvc5
A constraint solver and automatic theorem prover for Satifiability Modulo Theories (SMT). I wrote its finite field solver and its pythonic API. I've also contributed to its proof system. [site] [code] [paper]
Collaborative zkSNARKs
Prototype collaborative zkSNARKs: zero-knowledge proofs for distributed secret data. [code] [paper]
LFSC
A dependently typed language for expressing SMT proofs. [code]
Bellman Bignat
SNARK-friendly multiprecision arithmetic, hash-to-prime, Wesolowski proofs of exponentiation, and RSA accumulators. [code] [paper]

Independent Work

Construct
A programming language and interactive tool for classical geometry. [site] [code]
Khwarizmi
A programming language for algebra. A work in progress. [site] [code]
notebk
My electronic notebook. [code]