Selected Research

Autoformalization of CPython Powersort found a performance bug for 1 TB lists.

A measure of technique novelty for formal proofs, relative to a historical Lean corpus.

An end-to-end SMT-encodable Transformer architecture with formal proofs.

Pipeline to translate Rust GPU code into Coq semantics for memory model proofs.

Type system to enforce privacy regulations, including GDPR and HIPAA.

Language and type system to statically enforce differential privacy.