Selected Research

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

Prototype of a formal verifier for safety properties of Rust CUDA kernels.

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

Language and type system to statically enforce differential privacy.