Selected Research

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.

Prove equivalence between a human-readable program and a weight-sparse LLM circuit.

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.