Senior Research Scientist · AI and Formal Methods Engineer · PhD Mathematician
Independent contractor with the Beneficial AI Foundation and Kodamai · Based in Rome
I work at the intersection of formal verification, cryptography, and AI.
I contract with the Beneficial AI Foundation as a Senior Research Scientist, contributing to Signal Shot. My current focus is post-quantum cryptography formalisation in the secure-messaging project.
Separately, I contract with Kodamai as an AI engineer, building verified agentic infrastructure using ideas from category theory, type theory, and neuro-symbolic AI.
My background is in pure mathematics. I completed a PhD in Algebraic Geometry and a postdoc at KTH Royal Institute of Technology.
Lean 4 specifications and machine-checked proofs for secure messaging protocols, with a focus on post-quantum cryptography.
Mathematically grounded orchestration for specialised enterprise agents at Kodamai.
Research developed from part of my PhD thesis and published in the Journal of the Institute of Mathematics of Jussieu.
Contributed to the Lean 4 formal verification of the curve25519-dalek cryptographic library, including coordinating pull-request reviews.
Contributed formalised algebraic geometry to Lean's mathematical library.
Lean 4 · Rust · Python · Aeneas/Charon · SMT solvers