I study topics related to formal methods, cryptography, and distributed systems.

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]