Math PhD | AI Engineer | Formal Methods

Research Engineer at Beneficial AI Foundation | AI Engineer at stealth startup | Based in Rome

I build AI systems at the intersection of automation and formal verification. At Beneficial AI Foundation, I develop AI tooling for formal code verification and work on verifying cryptographic implementations in Lean4. At a stealth startup, I build B2B agentic automation systems at scale, leveraging formal methods for reliable and verifiable AI agents. My background in pure mathematics (PhD in Algebraic Geometry) provides a foundation for rigorous approaches to both AI safety and automated reasoning.

Research Engineer at Beneficial AI Foundation

• Developing AI-assisted tooling and automation for formal code verification
• Verifying Rust cryptographic implementations in Lean4

AI Engineer at stealth startup

• Building B2B, reliable, agentic automation systems at scale
• Working at the intersection of agent orchestration and formal verification

AI & Formal Methods PyTorch • Hugging Face • Lean4 • Verus (learning) • Interactive Theorem Proving

Programming & Infrastructure Python • Rust (learning) • Git • Linux • Docker • Google Cloud Platform

Specialized

• AI tooling for automated verification
• Formal verification of cryptographic code
• Multi-agent systems and LLM orchestration
• Real-time NLP and speech processing
• Mathematical modeling and proof formalization

• Formal verification of curve25519-dalek, a cryptographic library used in Signal's protocol
• Contributing to data generation for future LLM training on auto-formalization
• Technologies: Lean4, formal verification, cryptographic verification, Rust

Formalizing mathematical foundations in Lean4 proof assistant

• 700+ lines of verified code for topological Krull dimension theory
• Successfully contributed to mathlib4 (Lean's core math library): Krull-PR
• Technologies: Lean4, formal verification, type theory

Production-ready Italian-English translation pipeline for technical lecture environments

• BLEU ≥40, COMET ≥0.75 on scientific content with ≤4s latency
• Complete streaming pipeline: Whisper ASR → Translation → Kokoro TTS
• Team leadership in agile development environment
• Technologies: Whisper, FastWhisper, Kokoro TTS, Qwen2.5, PyTorch, CUDA

PhD in Mathematics (Algebraic Geometry, Motivic Homotopy Theory) - University of Duisburg-Essen

Postdoctoral Researcher - KTH Royal Institute of Technology

Pi School of AI Fellow - PiSchool

LinkedIn: alessandro-d-angelo

Old Academic Website: sites.google.com/view/alessandro-dangelo