My goal is to make secure systems as easy to build as insecure ones.

Towards this goal,
I use cryptography, compilers, and automated reasoning
to improve *programmable cryptosystems*.
Programmable cryptosystems
(such as zero-knowledge proofs,
multi-party computation,
and homomorphic encryption)
are powerful tools for
building systems
with strong privacy and security guarantees—without cryptographic or security expertise.

zkPi: Zero-Knowledge Proofs for Lean Theorems

We build the first zero-knowledge, succinct proofs for Lean theorems.
One potential application is safety proofs for proprietary software.
[preprint]

Split Gröbner Bases for Satisfiability Modulo Finite Fields

We improve an SMT solver for finite fields by splitting up the Gröbner basis it uses.
[preprint]

An SMT-LIB Theory of Finite Fields

We propose an SMT-LIB standard for finite fields.

Generating and Exploiting Automated Reasoning Proof Certificates

We make the case for automatically constructible and checkable proofs of
program correctness.
[paper]

Bounded Verification for Finite-Field-Blasting (in a Compiler for Zero Knowledge Proofs)

We explore automatic verification
for a finite-field blaster:
a key component of compilers for zero-knowledge proofs.
Along the way, we find 4 bugs in an existing finite-field blaster.
[preprint]

Satisfiability Modulo Finite Fields

We build finite-field reasoning into an SMT solver.
This is a key tool for automated cryptographic verification.
[preprint]

Silph: A Framework for Scalable and Accurate Generation of Hybrid MPC Protocols

Leveraging CirC, we build a high-performance compiler to hybrid
multi-party computations using a clever integrating of graph partitioning and
integer-linear programming.
[preprint]

Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers

We study producing a single refutation
for an unsatisfiable formula
solved with divide-and-conquer parallelism.
[preprint]

Collaborative zk-SNARKs: Zero-Knowledge Proofs for Distributed Secrets

cvc5: A Versatile and Industrial-Strength SMT Solver

Flexible Proof Production in an Industrial-Strength SMT Solver

We present the design of cvc5’s proof system.
[paper]

R2E2: low-latency path tracing of terabyte-scale scenes using thousands of cloud CPUs

We build a massively
parallel ray-tracer
for massive scenes
using serverless executors.
[code]

Efficient Functional Commitments: How to Commit to a Private Function

We allow the evaluator of a secret function
to

*prove*that they are evaluating that function uniformly. The might be applicable to credit scores or bail decisions. [preprint]
CirC: Unifying Compilers for SNARKs, SMT, and More

SAT Solving in the Serverless Cloud

High-level high-speed high-assurance crypto

We explore the design of high-level programming languages
for cryptography.

Parallelization Techniques for Verifying Neural Networks

We explore parallelization techniques and heuristics for
verifying properties of small neural networks.
[paper]

Scaling Verifiable Computation Using Efficient Set Accumulators

DRAT-based Bit-Vector Proofs in CVC4

We experiment with a variety of techniques for integrating
the DRAT proofs of a SAT solver into an SMT bit-vector solver.
[paper]

Clustering the Space of Maximum Parsimony Reconciliations in the Duplication-Transfer-Loss Model

We build clustering and evaluation algorithms
for joint evolutionary histories (cophylogenies).
These algorithms run in time

*sub-linear*in the size of the sets that they cluster. [paper]