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 distance of the full-precision result. I contributed the complete mixed-precision floating point subsystem to TensorLib, Lean's 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 mixed precision reasoning 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.
• Error bounds- Mechanized a generic framework for worst-case error bounds in rounding operations, addition, and in multiplication.

📊

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