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

A constraint solver and automatic theorem prover for Satifiability Modulo Theories (SMT). I wrote its finite field solver. I also wrote its pythonic API and contributed to its proof system. [site] [code]

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

A dependently typed language for expressing SMT proofs. I've touched most parts of it. [code]

A SNARK-friendly implementation of multiprecision arithmetic, hash-to-prime, Wesolowski proofs of exponentiation, and RSA accumulators using the Bellman library. [code] [paper]

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

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

The program that manages my electronic notebook. [code]