Position Details

Summary

Zeroth Research is a UK-based nonprofit research organisation dedicated to advancing AI safety through mathematical and computational methods. A guardrail that works and a guardrail nobody can lie about are two different things. You would build the second. You will own the engineering that takes Zero-Knowledge Model Checking from a research prototype to usable infrastructure. Our goal is a production-grade, open-source demonstrator by mid-2027.

The Opportunity

Formal verification can establish that a system satisfies a safety specification across all possible scenarios. Conventionally, however, the system must be disclosed to whoever verifies it.

Zero-Knowledge Model Checking (ZKMC) removes that requirement. A system-holder can prove that a secret system satisfies a public temporal specification without revealing the system itself. The result is a portable certificate that anyone can verify in milliseconds, cryptographically bound to the system actually deployed.

Consider a content-moderation pipeline: its operator could prove compliance with public safety rules without disclosing its proprietary filtering logic.

We are now extending this approach to zero-knowledge runtime monitoring and model checking under two-sided secrecy, where even the auditor’s criteria remain confidential.

Developed in close collaboration with the University of Birmingham and international research partners, this work brings together frontier research in cryptography and formal methods with practical systems engineering.

This position is funded by ARIA, the UK’s Advanced Research and Invention Agency, through its Safeguarded AI programme, which aims to build AI systems with verifiable, quantitative safety guarantees. It offers the opportunity to join the programme as a Creator, becoming part of ARIA’s community of researchers and engineers working towards this goal.

The Role

You will own the engineering that takes ZKMC from a research prototype to usable infrastructure, translating advances in cryptography and formal verification into correct, efficient, production-grade software.

This is not a role where you simply implement specifications handed down by researchers. You will make architectural decisions, challenge assumptions, identify what is computationally feasible and contribute to the design and evaluation of new protocols.

We work in the open. Code is published, performance is measured, and benchmarks are released whether or not they flatter us.

We welcome candidates at different levels of seniority. What matters most is what you have built, how you approach difficult engineering problems, and the judgement you bring to them.

Essential Qualifications

• Hands-on experience with zero-knowledge proof systems, such as arkworks, Halo2, Plonky3, or comparable frameworks
• Strong Rust programming skills, with an emphasis on correctness, maintainability and performance
• A track record of translating research papers, formal specifications or theoretical protocols into working, tested implementations
• Rigour in benchmarking and performance analysis, including the ability to distinguish real improvements from noise and explain technical trade-offs

Desired Qualifications

• Familiarity with folding schemes, recursive proofs, succinct proof systems or multi-party computation frameworks
• Background in formal methods, particularly temporal logic, automata, model checking or runtime verification
• Experience maintaining open-source projects or building software that other developers depend on

You do not need to meet every desirable qualification. We are particularly interested in people who can move confidently between mathematical ideas and practical systems engineering.

Responsibilities

• Turn ZKMC into infrastructure. Develop a usable API, a specification front end and commitment verification tied to a running system. Build a library that others can use and extend.
• Make proving practical. Improve proving performance through folding and succinctness, balancing efficiency, complexity and security.
• Implement new protocols. Translate research specifications for zero-knowledge runtime monitoring and multi-party model checking into correct, efficient implementations.
• Build the demonstrator end to end. Integrate the proving pipeline, agent harness, runtime monitor, verifier client and audit path into a working system.
• Measure and optimise. Profile the prover, identify bottlenecks and improve performance using reproducible benchmarks.
• Challenge the implementation. Test assumptions, investigate failure modes and ensure the system delivers the guarantees it claims.
• Build in the open. Write maintainable code, document design decisions and contribute to software that external developers and researchers can rely on.

How to Apply

If you're interested in joining Zeroth Research, we'd be pleased to hear from you.

To apply, submit your CV and, where available, links to your code, projects or academic profile.

We are particularly interested in understanding what you have built, the technical challenges you've tackled and your contribution to the projects you've worked on.

Applications will be reviewed on a rolling basis, and shortlisted candidates will be invited to an introductory discussion, followed by a technical interview.

For any queries about the role, please contact jobs@zeroth.org.

Position Details

Summary

Zeroth Research is a UK-based nonprofit research organisation dedicated to advancing AI safety through mathematical and computational methods. We are hiring two Machine Learning Engineers with complementary backgrounds: one to develop training procedures for neural certificates, and one to build LLM-based generation methods for proof search. Our goal is a production-grade, open-source demonstrator by mid-2027.

The Opportunity

For decades, proof search for system verification has relied primarily on symbolic algorithms. Machine learning now opens up new possibilities.

Formally verifying that a system meets its safety and security specifications means producing machine-checkable artefacts that together constitute a formal proof. At Zeroth Research, we have developed specialised proof tactics for verifying a wide range of systems. These tactics reduce proof search to the search for certificates, such as Lyapunov functions, supermartingale certificates and inductive invariants.

Our tactics define the conditions a valid certificate must satisfy. What’s missing is an efficient way to find these certificates at scale. We are exploring two approaches: learning neural certificates directly, in the style of reinforcement learning, and generating certificates as symbolic expressions using large language models.

Both positions are funded by ARIA, the UK’s Advanced Research and Invention Agency, through its Safeguarded AI programme, which aims to build AI systems with verifiable, quantitative safety guarantees. They offer the opportunity to join the programme as a Creator, becoming part of ARIA’s community of researchers and engineers working towards this goal.

The Roles

You will own the machine learning side of certificate synthesis, including loss design, sampling strategies, counterexample-guided search and network architecture.

This is not a role where you simply tune hyperparameters of a fixed method. You will design experiments, propose and test training procedures, challenge existing approaches and develop alternative solutions when necessary.

We work in the open. Code is published, performance is measured, and benchmarks are released whether or not they flatter us.

We welcome candidates at different levels of seniority. What matters most is what you have built, how you approach difficult engineering problems, and the judgement you bring to them.

Neural Certificate Learning

We are especially interested in candidates with one of two backgrounds:

• Reinforcement learning. Supermartingale conditions are Bellman-type inequalities, and learning a controller together with its certificate is constrained policy optimisation. You bring experience in value learning, actor-critic methods, exploration and making unstable training converge.
• Structured learning, such as graph neural networks. Many of our systems have explicit structure, including stochastic Petri nets, networks of interacting components and automata. You bring architectures and training methods that exploit this structure, including message passing, equivariance and generalisation across system sizes.

In this role you will:

• Make training scale. Design loss functions, sampling schemes and network architectures that exploit the structure of the problem.
• Co-train controllers and certificates. Learn policies alongside the certificates that prove them correct, understanding when the two objectives conflict.

In addition to the essential qualifications below, you will have at least one of:

• Hands-on experience with deep reinforcement learning beyond running existing baselines, including policy-gradient, actor-critic or value-based methods.
• Hands-on experience with neural networks that exploit problem structure, such as graph neural networks.

Language-based Certificate Generation

• LLM-based generation. Many certificates, such as Lyapunov functions or inductive invariants, have compact symbolic forms. A language model proposes candidate formulas, a formal verifier checks them, and any counterexamples feed back to the model so it can refine its next attempt. You bring experience building LLM systems beyond prompting, including fine-tuning, search over generations and learning from verifier or execution feedback.
• Syntactic search. Certificates can also be found by searching directly over the space of expressions, using genetic algorithms, evolutionary methods or other program-synthesis techniques, sometimes with an LLM acting as a smart mutation or proposal operator. You bring experience with search methods that generate, combine and refine structured outputs against an external checker.

In this role you will:

• Generate symbolic certificates. Develop methods in which language models propose candidate certificates and refine them using verifier counterexamples.
• Bring agents into proof construction. Enable AI agents to participate efficiently in building formal proofs using Zeroth Research’s verification infrastructure.

In addition to the essential qualifications below, you will have hands-on experience building LLM systems beyond prompting, including fine-tuning, search over generations or learning from verifier or execution feedback.

Essential Qualifications

• Hands-on experience with PyTorch or JAX, including diagnosing training that is unstable or does not converge
• Strong Python skills, with an emphasis on correctness, performance and maintainability
• A track record of translating machine learning research papers into working, tested implementations
• Rigour in benchmarking and performance analysis, including the ability to distinguish real improvements from noise and explain technical trade-offs
• An understanding of Lean, or the willingness and ability to learn it

Desired Qualifications

• Experience with Lyapunov, barrier or other certificates, safe and constrained reinforcement learning, or counterexample-guided synthesis
• Familiarity with neural network verification, such as bound propagation (auto_LiRPA, α,β-CROWN) or SMT solvers
• Background in formal methods, particularly temporal logic, automata, model checking or runtime verification
• Experience maintaining open-source projects or building software that other developers depend on

You do not need to meet every desirable qualification. We are particularly interested in people who can move confidently between mathematical ideas and practical systems engineering.

Responsibilities

• Build the pipeline end to end. Turn your methods into a working system, not a collection of experiments.
• Close the loop with verification. Integrate learning with formal verification so that every reported certificate is checked, using verifier feedback to guide and improve learning.
• Challenge the implementation. Critically review your work, test assumptions, investigate failure modes and ensure the system delivers the guarantees it claims.
• Build in the open. Write maintainable code, document design decisions and contribute to software that external developers and researchers can rely on.

How to Apply

If you're interested in joining Zeroth Research, we'd be pleased to hear from you.

To apply, submit your CV and, where available, links to your code, projects or academic profile.

We are particularly interested in understanding what you have built, the technical challenges you've tackled and your contribution to the projects you've worked on.

Applications will be reviewed on a rolling basis, and shortlisted candidates will be invited to an introductory discussion, followed by a technical interview.

For any queries about the role, please contact jobs@zeroth.org.

Position Details

Summary

Zeroth Research is a UK-based nonprofit research organisation dedicated to advancing AI safety through mathematical and computational methods. We are hiring one Research Engineer in Formal Methods with expertise in the modelling and verification of multi-agent systems, communication and message-passing protocols, and compositional modelling. Our goal is a production-grade, open-source demonstrator that integrates with the Scaling Trust Arena.

The Opportunity

Coordination and interaction between AI agents, in both the digital and the physical world, is the next frontier for AI. It opens up enormous opportunities, but it also introduces new risks. As AI agents negotiate autonomously, and potentially self-regulate, alongside humans in multi-agent settings such as financial systems and robotics, we need to ensure that these systems meet essential safety and security criteria.

Formally verifying that a system meets its safety and security specifications means producing machine-checkable artefacts that together constitute a formal proof. At Zeroth Research, we develop modelling frameworks for cyber-physical multi-agent systems, together with tactics for their formal verification. These tactics reduce proof search to the search for certificates, such as Lyapunov functions, supermartingale certificates and inductive invariants.

This position is funded by ARIA, the UK’s Advanced Research and Invention Agency, through its Scaling Trust programme, which funds the infrastructure and research for AI agents to coordinate securely on our behalf, across the digital and physical worlds. It offers the opportunity to join the programme as a Creator, becoming part of ARIA’s community of researchers and engineers working towards this goal.

The Role

You will own the formal methods side of the Dovetail project, developing modelling frameworks that are amenable to code and proof generation, with a level of trust that goes beyond existing AI technologies.

This is not a role where you simply use language agents and autoformalisation to generate protocols and proofs. AI can be trusted to find proofs, but a proof is only as good as the theorem it proves: the definitions and specifications must capture what we actually mean. You will develop a formalisation scaffolding that checks that the model of a system and its specification match their intended semantics.

To this end, we aim to develop a representation of reactive, message-passing systems that captures real-world critical infrastructure, including physical constraints where relevant, so that we can capture the security of cyber-physical multi-agent systems and defend them against both digital and physical attacks.

We work in the open. Code is published, performance is measured, and benchmarks are released whether or not they flatter us.

We welcome candidates at different levels of seniority. What matters most is what you have built, how you approach difficult engineering problems, and the judgement you bring to them. We are especially interested in candidates with a background in formal methods and an appetite for harnessing frontier AI to generate correct-by-construction multi-agent systems.

Essential Qualifications

• Experience in formal verification, in particular model checking, or equivalent qualifications and experience
• A track record of translating research papers into working, tested implementations
• Rigour in benchmarking and performance analysis, including the ability to distinguish real improvements from noise and explain technical trade-offs
• Familiarity with Lean and ideally Rust, or the willingness and ability to learn them

Desired Qualifications

• Experience with reactive synthesis and game theory, temporal logic or automata theory
• Experience harnessing LLM agents
• Experience maintaining open-source projects or building software that other developers depend on

You do not need to meet every desirable qualification. We are particularly interested in people who can move confidently between mathematical ideas and practical systems engineering.

Responsibilities

• Develop a representation for cyber-physical multi-agent message-passing systems. Working alongside Zeroth engineers and Scaling Trust Creators, build a representation framework for multi-agent interaction.
• Instrument AI tools to generate code and proofs of correctness. Integrate LLM agents with formal verification so that every reported certificate is checked, using verifier feedback to guide and improve learning.
• Evaluate on real-world communication protocols. Critically review your work, test assumptions and investigate failure modes against critical codebases modelled within our framework.
• Build in the open. Write maintainable code, document design decisions and contribute to software that external developers and researchers can rely on.

How to Apply

If you're interested in joining Zeroth Research, we'd be pleased to hear from you.

To apply, submit your CV and, where available, links to your code, projects or academic profile.

We are particularly interested in understanding what you have built, the technical challenges you've tackled and your contribution to the projects you've worked on.

Applications will be reviewed on a rolling basis, and shortlisted candidates will be invited to an introductory discussion, followed by a technical interview.

For any queries about the role, please contact jobs@zeroth.org.