Projects

Mixed-Precision Floating Point in Lean 4

ML training increasingly relies on narrow floating point formats (fp8, bf16) for performance, but their rounding and overflow behavior is subtle and poorly specified. Having these semantics mechanized in a proof assistant means we can eventually prove error bounds — e.g., that a mixed-precision matmul accumulation in fp8 --> fp32 stays within a known ULP distance of the full-precision result. I contributed the complete mixed-precision floating point subsystem to TensorLib, Lean's tensor library for verified numerical computing. My work adds IEEE 754 floating point formats across five PRs (~3,600 LOC), building up from the encoding layer through type promotion to PBT including:

Bit-exact encoders/decoders for float16, bfloat16, fp8_e4m3, fp8_e5m2, and fp8_e3m4 — handling subnormal numbers, ±infinity, NaN propagation, and round-to-nearest-even tie-breaking. Each encoder is verified against Google's ml_dtypes reference implementation via compile-time #guard checks (~200 across the codebase).
A 16-dtype type promotion lattice — the join function that determines the result type when two different dtypes interact (e.g., what happens when you add an fp8 tensor to a float32 tensor). This includes lossless cast analysis, commutativity guarantees, and deliberate divergences from NumPy where NumPy gets it wrong (e.g., join(e4m3, e3m4) returns none rather than silently overflowing).
Overflow saturation semantics for cross-dtype casts — inf/NaN handling, per-dtype integer saturation bounds, and unsigned wrapping behavior matching NumPy's casting rules.
Property-based testing using Lean 4's Plausible framework: round-trip correctness (encode → decode → encode), arithmetic commutativity for each fp format, join commutativity across all dtype pairs, and cast-round-trip verification.
Mixed-precision tensor operations — matmul, dot product, and element-wise arithmetic that correctly promote operands through the cast graph before computation.

Challenges:

The fp8 formats are tricky. fp8_e4m3 and e3m4 trade off range vs. precision (e4m3 max is 448, e3m4 max is 15.5), and each format has different NaN/infinity conventions (e4m3fn has no infinity, e5m2 does, e3m4 does). Getting round-to-nearest-even correct at the boundary between subnormal and normal numbers, and at the overflow edge where double-rounding through fp32 can disagree with a single-precision round, required careful bit-level reasoning validated against the reference.

📊

Pint: A small trusted kernel with dependent intersections, unions, and index erasure

A compact, syntax-directed calculus equipped with a bidirectional type checker supporting dependent intersection and union types, subtyping, and explicit coercions. The system incorporates index and coercion erasure to ensure that program equivalence is preserved at runtime, while maintaining soundness and compatibility with an implicit, bidirectional checking discipline. Finally, we generalize the framework to a quantitative resource setting, following McBride’s graded type theory, allowing Pint’s irrelevance and erasure mechanisms to be expressed via graded quantities. This subsumes ad-hoc erasure techniques and enables principled, resource-aware typing within the calculus

Pint on the Rocqs

Aims to mechanize the complete Pint calculus in Rocq, including dependent intersection and union types, subtyping, and coercions. The project formalizes Pint within a small, verifiable kernel, quantifying proof size, isolating axioms, and ensuring that the trusted computing base remains minimal. In addition, we develop a domain-specific language (DSL) for embedding imperative and object-oriented programs into the mechanization, enabling practical program verification within the formalized system.

Composition of Sigma Protocols

TBD

Interactive Zero Knowledge Proofs for Quadratic Residues in EasyCrypt

Zero knowledge proofs (ZKP) have gained popularity recently due to their ability to protect data while also being efficient. Interractive ZKP's allow a prover to convince a verifier about the validy of some statement without revealing any meaningful information beyond the truth of the statement itself. In this project, we studied a Sigma-protocol for quadratic residues and formalized its security properties in the EasyCrypt proof assistant. We provided machine-checked proofs of completeness, soundness, and honest-verifier zero-knowledge within a game-based framework. A more detailed report can be found here

Row Level Security in Databases

This project implements Row-Level Security (RLS) for a SQLite database using Haskell and the LIO (Labeled IO) library for information-flow control. We model database tables as Haskell data types and associate each row with dynamically constructed DCLabels encoding secrecy and integrity policies. Security is implemented in a secure database layer that extends basic database operations with label-based checks, ensuring that data flows only when permitted by the canFlowTo relation. The system supports secure insertion, querying, and deletion of customer records, with multiple versions exploring role-based access control through labels representing administrators and regular users. Serialization and deserialization of labels enable persistent storage in SQLite, and prepared statements are used to safely interface between Haskell and SQL. This work demonstrates how fine-grained information-flow control using Haskell LIO can be used to enforce security policies in databases. Slides can be found 🎞 here