About Us
Our Project: Automated Reasoning for AI Verification Technology
We build software for the automated generation of proof obligations for the safety verification of reactive and cyber-physical AI systems, and the validity verification of proof certificates responding to these obligations. We envision a technology where AI systems produce formal proofs of probabilistic compliance with safety specifications, and will be working towards the seamless integration between automated reasoning and machine learning infrastructures.
- Modelling risks arise from erroneous or overly stringent assumptions about the digital or physical world in which a system operates.
- Alignment risks arise from the discrepancy between a system’s behaviour and the behaviour intended by the designer, user, or regulator.
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 computer science researcher specialising in cybersecurity, with a focus on safeguarding AI systems through rigorous verification. He leads efforts to make machine learning models demonstrably safe, grounded in real-world industrial applications.
Pascal Berrang
Pascal is an expert in the security and privacy of AI and blockchain systems and pioneered the concept of membership inference attack in ML models and co-invented ML-Leaks.
Marco Casadio
Marco finished his PhD at Heriot Watt University, his research interests involve verification and machine learning. More precisely, they involve enforcing logical constraints to neural networks through loss functions. His most recent work focused on ensuring robustness of NLP systems.
Marek Chalupa
Marek develops algorithms and tools for verification and monitoring of systems and led the development of the award winning software verification tool Symbiotic.
Mirco Giacobbe
Mirco specialises on the integration of machine learning and automated reasoning technologies for the formal verification of hardware and software and the safeguard of cyber-physical systems.
Abdelrahman Hekal
Abdelrahman specialises in AI safety and the formal verification of cyber-physical systems. He finished his PhD at Newcastle University and recently worked on verification of Neuro-Symbolic AI at Imperial College London's Safe AI Lab.
Edoardo Manino
Edoardo is an expert in neural network verification at the software and hardware level. He is an advocate for checking the implementation of AI systems. He holds ARIA opportunity seed funding on the safety of closed-loop AI systems in finite precision.
Greg Neustroev
Greg is a researcher in automated reasoning and formal methods, contributing to the development of safe and verifiable AI systems.
Amin Razavi
Amin designs confidentiality and trust protocols for decentralized systems, with a background spanning cryptography, secure hardware, pure mathematics, and computability theory. He is focused on secure computation under adversarial conditions and long-term infrastructure resilience.
Simon Schmidt
Simon develops technical AI-based solutions for customers. He obtained a PhD in mechanical engineering in computational mechanics, with focus on numerical simulation algorithms.
Ayberk Tosun
Ayberk is an expert in automated theorem proving with a focus on constructive mathematics in the foundational setting of Homotopy Type Theory. He obtained his PhD at Birmingham working in predicative pointfree topology.
Join Our Team
Job Advert
We are looking for talented individuals to join us in advancing the safety and security of AI systems.
Research Engineer, Verifiable Reactive Systems
Summary
A guardrail that works and a guardrail nobody can lie about are different things. You would build the second one.
Formal verification can establish that a system satisfies a safety specification across all of its runs, but conventionally requires the system to be disclosed to whoever is checking it. We have developed Zero-Knowledge Model Checking (ZKMC), which removes that requirement: a system-holder can prove to an external verifier that a secret system satisfies a public temporal specification, producing a portable certificate that anyone can check in milliseconds and that is cryptographically bound to the system actually deployed.
A system-holder proves that a committed reactive system such as a communication protocol or a decision-making system satisfies a temporal specification while revealing nothing about the system, so a mediation pipeline can be certified against public rules with its filter logic secret — and the certificate is portable, checkable by anyone in milliseconds, and cryptographically bound to the deployment serving traffic. Next comes runtime monitoring in zero knowledge and model checking under two-sided secrecy, for the auditor whose criteria cannot be published.
Our target is a production-grade demonstrator, open-sourced by mid 2027.
Project Overview
You own the software that makes it real: Zeroth's open-source Reactive Modules library, the proving pipeline underneath it, and the demonstrator. That means turning protocols into infrastructure, driving proving cost down, and telling a cryptographer when what they have specified will not run. The research sits with Birmingham and international partners; you decide what is buildable. Everything is open, and benchmarks are published whether or not they flatter us.
We hire at a range of levels and care more about what you have built than about how long you have been building.
Essential Qualifications
- Experience with ZKP systems (arkworks, Halo2, Plonky3, or comparable)
- Ability to write maintainable Rust, and an understanding of or willingness to learn Lean
- Track record of taking a specification written for a theory audience and producing a correct, measured implementation of it
- Rigour about measurement
Desired Qualifications
- Familiarity with folding and recursion schemes, and MPC frameworks
- Formal methods background: temporal logic, automata, model checking, runtime monitoring
- Open-source maintainership, or any track record of software other people depend on
Responsibilities
- Turn the ZKMC prototype into infrastructure: usable API, specification front end, commitment checking wired to a running system, benchmarks we are willing to publish
- Amortise per-event proving cost through folding, and shrink certificates through succinctness
- Implement zero-knowledge runtime monitoring and multi-party model checking from protocol specifications written for industrial applicability
- Build the demonstrator end to end: pipeline, agent harness, monitor, verifier client, audit path
- Profile the prover until you know exactly where the time goes, then move it
- Red-team our own implementation
Position Details
Contract type: 14-month fixed-term contract (October 2026 – November 2027)
Working pattern: Full-time (flexible working arrangements considered)
Location: Birmingham / hybrid / remote
Salary Range: £55,000–£75,000 p.a.
Zeroth Research is committed to fostering an inclusive and diverse working environment. We are an equal opportunities employer and welcome applications from all suitably qualified candidates regardless of age, disability, gender identity or expression, marital or civil partnership status, pregnancy or maternity, race, religion or belief, sex, or sexual orientation. We value diversity of thought, background, and experience, and we are committed to making reasonable adjustments throughout the recruitment process and employment to support accessibility and inclusion.