Math PhD · AI Engineer · Formal Methods
AI Lead at Beneficial AI Foundation · AI Engineer at Kodamai · Based in Rome
I work on formal verification and the AI tooling around it. At the Beneficial AI Foundation I lead AI tooling and verify cryptographic code in Lean 4. At Kodamai I build agentic systems on foundations from dependent type theory and category theory. Before industry I did a PhD in algebraic geometry (motivic homotopy theory) and a postdoc at KTH. The math background is why I treat a proof as the unit of trust, in code as much as in theorems.
AI Lead, Beneficial AI Foundation
- Lead AI tooling for the formal verification team: autoformalization and LLM-assisted proof writing
- Verify curve25519-dalek in Lean 4, the elliptic curve library behind Signal's protocol
AI Engineer, Kodamai
- Building agentic systems on foundations from dependent type theory and category theory
A merged PR into Lean's core math library. leanprover-community/mathlib4#29728
Formalizing a production cryptographic library (Ristretto, Montgomery reduction, the Elligator map) against Mathlib's elliptic curve modules. Also feeds data generation for autoformalization. https://github.com/Beneficial-AI-Foundation/curve25519-dalek-lean-verify
700+ lines on topological Krull dimension theory. https://github.com/ADA-Projects/Lean-AG
Italian to English pipeline for technical lectures. BLEU ≥ 40, COMET ≥ 0.75 on scientific content, latency under 4s. Whisper ASR, translation, Kokoro TTS. Led the team.
Lean 4, Python, Rust. Verification toolchain: Aeneas/Charon (Rust to Lean 4), SMT solvers.
PhD in Mathematics, algebraic geometry and motivic homotopy theory, University of Duisburg-Essen Postdoctoral researcher, KTH Royal Institute of Technology Pi School of AI fellow
Website: https://a-dangelo.com LinkedIn: https://www.linkedin.com/in/alessandro-d-angelo-644213355/