Making Intelligent Systems Safe, with Mathematical Certainty
Meet the Experts
Our Team
Our team combines world-class research expertise with real-world industry experience to advance the safety and security of AI systems.
Luca Arnaboldi
Luca is a cybersecurity researcher who leads efforts to make machine learning models demonstrably safe through rigorous verification, grounded in real-world industrial applications.
Pascal Berrang
Pascal works on the security and privacy of AI and blockchain systems. He pioneered membership inference attacks and ML-Leaks, and recently co-invented zero-knowledge model checking.
Marco Casadio
Marco works at the intersection of verification and machine learning, enforcing logical constraints on neural networks through loss functions, with a focus on the robustness of NLP systems.
Marek Chalupa CTO
Marek develops algorithms and tools for the verification and monitoring of systems, and led the development of the award-winning software verification tool Symbiotic.
Mirco Giacobbe CEO
Mirco combines machine learning and automated reasoning to formally verify hardware, software and cyber-physical systems. He pioneered the neural certificates and zero-knowledge model checking.
Igor Konnov
Igor works on the automated verification of distributed and blockchain protocols, and led the development of Apalache, a symbolic model checker for TLA+, and the Quint specification language.
Edoardo Manino
Edoardo works on neural network verification at the software and hardware level, with a focus on the safety of closed-loop AI systems in finite precision.
Greg Neustroev CSO
Greg is an expert in reinforcement learning and stochastic analysis, and a pioneer of neural supermartingale certificates for the verification of continuous-time systems.
Thomas Pani
Thomas works on the specification and verification of distributed systems, and co-developed Quint, an executable specification language, and the Apalache model checker.
Amin Razavi
Amin designs confidentiality and trust protocols for decentralised systems, focusing on secure computation under adversarial conditions and long-term infrastructure resilience.
Diptarko Roy
Diptarko works on the formal verification of stochastic systems. He pioneered supermartingale certificates for ω-regular properties and machine learning methods for certificate generation.
Sarah Sallinger
Sarah works on formal methods for systems engineering, with a focus on probabilistic hyperproperties, controller synthesis, and Heisenbugs.
Ayberk Tosun
Ayberk works on automated theorem proving, with a focus on constructive mathematics in the foundational setting of Homotopy Type Theory.