Signal Shot: Secure Messaging Formalisation
Contributing Lean 4 specifications and machine-checked proofs for secure messaging protocols, with a focus on post-quantum cryptography.
Projects
Building at the intersection of formal verification, cryptography, and mathematically grounded AI.
Lean 4 curve25519-dalek Verification
Contributed to the Lean 4 formal verification of the curve25519-dalek cryptographic library, including coordinating pull-request reviews.
curve25519-dalek-lean-verify on GitHubLean 4 Algebraic Geometry
700+ lines of verified Krull dimension theory. Mathlib contributor.
Speech Translation System
Production-ready Italian–English pipeline with ≤4s latency.
Published Research
KW-Euler Classes via Twisted Symplectic Bundles
Journal of the Institute of Mathematics of Jussieu
Developed from part of my PhD thesis, this paper builds the theory of twisted symplectic bundles and applies it to computations of KW-Euler classes in motivic homotopy theory.
Read the published paperPreviously in academia: PhD under M. Levine (Duisburg-Essen), postdoc with D. Rydh (KTH). Research in motivic homotopy theory and derived algebraic geometry.
arXiv publications