A compiler infrastructure from high-level languages to zero-knowledge proofs, SMT, and other *existentially quantified circuits*. [code] [paper]

A constraint solver and automatic theorem prover for Satifiability Modulo Theories (SMT). I've worked on its finite field solver, pythonic API, and proof system. [site] [code] [paper]

Prototype collaborative zkSNARKs: zero-knowledge proofs for distributed secret data. [code] [paper]

A dependently typed language for expressing SMT proofs. [code]

SNARK-friendly multiprecision arithmetic, hash-to-prime, Wesolowski proofs of exponentiation, and RSA accumulators. [code] [paper]

A programming language and interactive tool for classical geometry. [site] [code]

A programming language for algebra. A work in progress. [site] [code]

My electronic notebook. [code]