Projects
Building tools at the intersection of AI and formal verification.
Lean4 Rust Code Verification
Formal verification of the curve25519-dalek cryptographic library in Lean4.
Lean4 Algebraic Geometry
700+ lines of verified Krull dimension theory. Mathlib4 contributor.
Speech Translation System
Production-ready Italian–English pipeline with ≤4s latency.
Previously in academia — PhD under M. Levine (Duisburg-Essen), postdoc with D. Rydh (KTH). Research in motivic homotopy theory and derived algebraic geometry.
arXiv publications