\n
TA1 Scaffolding
\nWe can build an extendable, interoperable language and platform to maintain formal world models and specifications, and check proof certificates.
\n\n
Meet the TA1.4 (Sociotechnical Integration) Creators
\nWe’re funding six teams to address the essential link between advanced AI technology and society. They will explore how the technical aspects of Safeguarded AI, such as specifications and verification, can be aligned with societal values, ethical considerations, and effective governance mechanisms.
\nThe Creators in TA 1.4 come from a range of backgrounds spanning economics, law, policy, the social sciences, and practical philosophy. They will work together and across other technical areas to develop deliberation procedures, legal frameworks, and mathematical constructions that are directly applicable to building and deploying safeguarded AI in a responsible and beneficial manner.
\n","tabId":"","modules":[{"type":"creator-cards","data":{"type":"creator-cards","items":[{"title":"Law-following AI","description":"","teamLead":"Cullen O'Keefe, Director of Research, Institute for Law & AI","team":"Team: Janna Tay, LawAI","text":"
This team is exploring critical challenges within AI alignment, specifically how advanced AI agents conform to humanity’s rules of conduct as embodied in law. Their work will focus on building societal consensus around the need to have AI agents follow the law, and develop legal theories and policy specifications that would enable humanity to encode legal guardrails into AI behaviour.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Field Building for Better Formal Models of Society","description":"","teamLead":"Joe Edelman; Ryan Lowe, Meaning Alignment Institute","team":"","text":"This team is developing formal models of society that can provide genuine safety guarantees for AI systems and institutions. This work addresses a critical gap in formal safety guarantees for AI systems interacting with humans and human societies by replacing reductive preference-based models with context-rich alternatives. Their research teams are developing value-based welfare models, formal deliberation frameworks, explainable moral reasoning systems, and multi-agent negotiation protocols.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"AI-enabled Governance Models for Advanced AI R&D Organisations","description":"","teamLead":"Alex Petropoulos, Centre for Future Generations","team":"Team: Bengüsu Özcan, David Janků, Max Reddel, Centre for Future Generations","text":"This team will explore the potential for AI-enabled governance tools to be applied to AI R&D organisations. Their vision is to leverage AI systems as governance tools, with an ambition to design frameworks that simultaneously enhance oversight and accountability while continuing to support innovation. Ultimately, ensuring that AI development organisations can remain agile, responsible, transparent and secure as capabilities advance.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Privacy-preserving AI Safety Verification","description":"","teamLead":"Pascal Berrang, Mirco Giacobbe, University of Birmingham | Yang Zhang, CISPA Helmholtz Center for Information Security","team":"","text":"This team will develop the foundations of privacy-preserving AI safety verification, enabling the verification of AI safety guarantees without revealing any sensitive details about the underlying model or data. This technology will deliver mathematical assurances that AI systems adhere to safety specifications and uphold privacy of their models and data, crucial in applications where both safety and privacy are critical.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Aggregating Safety Preferences for AI Systems: A Social Choice Approach","description":"","teamLead":"Markus Brill, University of Warwick","team":"Team: Niclas Boehmer, HPI Potsdam; Paul Goldberg, University of Oxford; Davide Grossi, University of Groningen; Jobst Heitzig, Potsdam Institute for Climate Impact Research and Zuse Institute Berlin; Wes Holliday, UC Berkeley","text":"This team will address the critical challenge of aggregating diverse and often conflicting human perspectives on AI safety. They will develop a framework for aggregating human safety specifications for AI systems, with the goal of contributing to a “gatekeeper AI” that mitigates risks posed by AI agents. The core technology involves novel methods in the tradition of social choice theory to elicit and aggregate stakeholder preferences regarding acceptable risk thresholds and safety conditions.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Deliberative AI Specifications and Infrastructure","description":"","teamLead":"Aviv Ovadya, AI & Democracy Foundation","team":"Team: Luke Thorburn, Andrew Konya, Kyle Redman, Jim Chen, AI & Democracy Foundation; Flynn Devine, Boundary Object Studio; Amy Zhang and Kevin Feng, University of Washington; Michiel Bakker, MIT","text":"This team is building the deliberative infrastructure to ensure that powerful AI systems are developed in the public interest through democratic processes. Their work focuses on two interacting workstreams:
\n\n
TA1 Scaffolding
\nWe can build an extendable, interoperable language and platform to maintain formal world models and specifications, and check proof certificates.
\n\n
Meet the TA1.1 (Theory) Creators
\nOur TA1.1 Creators will look to unlock novel frontiers for representing different sources of uncertainty, with the ultimate goal of using this semantics to formally model and soundly over approximate a wide range of application domains and safety specifications, against which Safeguarded Al systems will later be verified. The intended output will be a single artefact that is a dissertation-length definition of these languages. With these mathematical representations and formal semantics in place, the programme's other TAs will produce world-models, safety specifications, and proof certificates.
\nOur TA1.1 Creators have been tasked with defining “syntax” (algebraic construction operators, and version-controllable serialisable data structures), and formal semantics, for language(s) that can be used by teams of humans – and, later, AI systems – to define “world models”, probabilistic specifications, neural network controllers, and proof certificates. These proof certificates present efficiently checkable arguments verifying that a controller composed with a world model satisfies its specification.
\nIn convening this group, we’ve brought together a wide range of relevant expertise in mathematical modelling (across dynamical systems, imprecise probability, category theory, type theory proof theory and more), as well as expertise in domains that will ensure these approaches are commensurable and computationally practical.
","tabId":"","modules":[{"type":"spacer-comp","data":{"type":"spacer-comp","cssSizeClass":"small","height":0}},{"type":"creator-cards","data":{"type":"creator-cards","items":[{"title":"Safety: Core representation underlying safeguarded AI","description":"","teamLead":"Team Lead: Ohad Kammar, University of Edinburgh","team":"Team: Justus Matthiesen; Jesse Sigal, University of Edinburgh","text":"This project looks to design a calculus that utilises the semantic structure of quasi-Borel spaces, introduced in ‘A convenient category for higher-order probability theory‘. Ohad and his team will develop the internal language of quasi-Borel spaces as a “semantic universe” for stochastic processes, define syntax that is amenable to type-checking and versioning, and interface with other teams in the programme—either to embed other formalisms as sub-calculi in quasi-Borel spaces, or vice versa (e.g. for imprecise probability).
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Axiomatic Theories of String Diagrams for Categories of Probabilistic Processes","description":"","teamLead":"Fabio Zanasi, University College London","team":"","text":"This project aims to provide complete axiomatic theories of string diagrams for significant categories of probabilistic processes. Fabio will then use these theories to develop compositional methods of analysis for different kinds of probabilistic graphical models.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"SAINT: Safe AI ageNTs – Formal certification of AI agents in the world","description":"","teamLead":"Alessandro Abate, University of Oxford Team","team":"Team: Virginie Debauche, Niko Vertovec, University of Oxford","text":"Building on an existing body of work, cognate literature and the certification of AI agents via “neural synthesis”, Alessandro and his team will look to advance beyond the synthesis of model-based certificates that are either Boolean or have specific probabilistic forms; move beyond the adherence by a single model of the AI agent or its environment; and to advance beyond the restrictive assumption of single, fixed specifications. The project will bridge between the use of SAT solvers and statistical approaches such as PAC.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"ULTIMATE: Universal Stochastic Modelling, Verification and Synthesis Framework","description":"","teamLead":"Radu Calinescu, University of York","team":"Team: Simos Gerasimou; Sinem Getir Yaman; Gricel Vazquez; University of York","text":"Radu + his team plan to develop a universal framework for the compositional definition, verification and synthesis of stochastic world models. When realised, this universal framework will support the modelling of probabilistic and nondeterministic uncertainty, discrete and continuous time, partial observability, and the use of both Bayesian and frequentist inference to exploit domain knowledge and data about the modelled context.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Quantitative Predicate Logic as a Foundation for Verified ML","description":"","teamLead":"Ekaterina Komendantskaya + Robert Atkey, University of Southampton/Heriot-Watt University; University of Strathclyde","team":"Team: Radu Mardare, Heriot-Watt University; Matteo Capucci, Independent","text":"This project aims to develop a unifying logical framework, Quantitative Predicate Logic (QPL), to provide the connection between specifications of low-level machine learning components and cyber-physical system specifications (CPS spec). The current state of saturation and fragmentation of the literature that concerns specification, verification, and spec-driven training of ML models suggests that a novel umbrella “foundation for verified ML” that unifies mathematical concepts coming from Empirical Risk Minimisation (ERM), Formal Verification, and Quantitative Reasoning is urgently needed. Ekaterina + Robert plan to define and establish such a unifying framework.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Learning-Theoretic AI Safety","description":"","teamLead":"Vanessa Kosoy, Association of Long Term Existence and Resilience (ALTER)","team":"Team: David Manheim, Association of Long Term Existence and Resilience (ALTER); Alexander Appel + Gergely Szucs, Affiliate Learning-Theoretic Employment and Resources (ALTER)","text":"The project aims to develop formal, theoretical foundations that ensure the safe and reliable functioning of AI systems, particularly those that may reach or surpass human-level intelligence. This includes but is not limited to developing mathematically rigorous theories concerning ambiguous online learning (i.e. online learning with partially-specified hypotheses) and infra-bayesian regret bounds.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Probabilistic Protocol Specification for Distributed Autonomous Processes","description":"","teamLead":"Nobuko Yoshida, University of Oxford","team":"Team: Adrián Puerto Aubel; Burak Ekici; Joseph Paulus; Dylan McDermott, University of Oxford","text":"Cyber-physical AI systems – which are often composed of concurrent autonomous components communicating via networks – are frequently unsafe, unreliable and non-robust. Nobuko and her team plan to develop a new theory of Probabilistic Session Types (ProST), which provides a formal interpretation using Probabilistic Petri Nets. ProST will provide correctness by construction, ensuring that each component follows a specified protocol during communication, enhancing the safety and reliability of these systems under uncertain conditions.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Philosophical Applied Category Theory","description":"","teamLead":"David Corfield, Independent Researcher","team":"","text":"This project plans to overcome the limitations of traditional philosophical formalisms by integrating interdisciplinary knowledge through applied category theory. In collaboration with other TA1.1 Creators, David will explore graded modal logic, type theory, and causality, and look to develop the conceptual tools to support the broader Safeguarded AI programme.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Double Categorical Systems Theory for Safeguarded AI","description":"","teamLead":"David Jaz Myers, Topos Research UK","team":"Team: Owen Lynch; Sophie Libkind; David Spivak, Topos Research UK; James Fairbanks, University of Florida","text":"This project aims to utilise Double Categorical Systems Theory (DCST) as a mathematical framework to facilitate collaboration between stakeholders, domain experts, and computer aides in co-designing an explainable and auditable model of an autonomous AI system’s deployment environment. David + team will expand this modelling framework to incorporate formal verification of the system’s safety and reliability, study the verification of model-surrogacy of hybrid discrete-continuous systems, and develop serialisable data formats for representing and operating on models, all with the goal of preparing the DCST framework for broader adoption across the Safeguarded AI Programme.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Monoidal Coalgebraic Metrics","description":"","teamLead":"Filippo Bonchi, University of Pisa","team":"","text":"Filippo and team intend to establish a robust mathematical framework that extends beyond the metrics expressible in quantitative algebraic theories and coalgebras over metric spaces. By shifting from Cartesian to a monoidal setting, this group will examine these metrics using algebraic contexts (to enhance syntax foundations) and coalgebraic contexts provide robust quantitative semantics and effective techniques for establishing quantitative bounds on black-box behaviours), ultimately advancing the scope of quantitative reasoning in these domains.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Doubly Categorical Systems Logic: A theory of specification languages","description":"","teamLead":"Matteo Capucci, Independent Researcher","team":"","text":"This project aims to develop a logical framework to classify and interoperate various logical systems created to reason about complex systems and their behaviours, guided by Doubly Categorical Systems Theory (DCST). Matteo’s goal is to study the link between the compositional and morphological structure of systems and their behaviour, specifically in the way logic pertaining these two components works, accounting for both dynamic and temporal features. Such a path will combine categorical approaches to both logic and systems theory.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"True Categorical Programming for Composable Systems Total","description":"","teamLead":"Jade Master + Zans Mihejevs, Glasgow Lab for AI Verification (GLAIVE) ","team":"Team: Andre Videla; Dylan Braithwaite, GLAIVE ","text":"This project intends to develop a type theory for categorical programming that enables encoding of key mathematical structures not currently supported by existing languages. These structures include functors, universal properties, Kan extensions, lax (co)limits, and Grothendieck constructions. Jade + team are aiming to create a type theory that accurately translates categorical concepts into code without compromise, and then deploy this framework to develop critical theorems related to the mathematical foundations of Safeguarded AI.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Unified Automated Reasoning for Randomised Distributed Systems","description":"","teamLead":"Alexandra Silva, University College London + Cornell University","team":"Team: Robin Piedeleu, University College London, Noam Zilberstein, Cornell University","text":"This project will look to extend Outcome Logic, a framework that captures correctness and incorrectness properties in programmes with effects, to handle randomisation and concurrency. Orthogonally, it will also look at string diagrammatic reasoning on probabilistic programs. By providing probabilistic descriptions of system behaviours and supporting compositional reasoning, the team will look to allow for scalable reasoning for complex systems.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Employing Categorical Probability Towards Safe AI","description":"","teamLead":"Sam Staton, University of Oxford","team":"Team: Pedro Amorim; Elena Di Lavore; Paolo Perrone; Mario Román; Ruben Van Belle; Younesse Kaddar; Jack Liell-Cock; Owen Lynch, University of Oxford","text":"Sam + team will look to employ categorical probability toward key elements essential for world modelling in the Safeguarded AI Programme. They will investigate imprecise probability (which provides bounds on probabilities of unsafe behaviour), and stochastic dynamical systems for world modelling, and then look to create a robust foundation of semantic version control to support the above elements.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Syntax and Semantics for Multimodal Petri Nets","description":"","teamLead":" Amar Hadzihasanovic, Tallinn University of Technology ","team":"Team: Diana Kessler, Tallinn University of Technology","text":"Amar + team will develop a combinatorial and diagrammatic syntax, along with categorical semantics, for multimodal Petri Nets. These Nets will model dynamical systems that undergo mode or phase transitions, altering their possible places, events, and interactions. Their goal is to create a category-theoretic framework for mathematical modelling and safe-by-design specification of dynamical systems and process theories which exhibit multiple modes of operation.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Two-dimensional Kripke Semantics and World Models","description":"","teamLead":"Alex Kavvos, University of Bristol","team":"","text":"This project aims to advance the theory of Two-dimensional Kripke Semantics (2DKS), which enhances traditional Kripke semantics by incorporating ‘evidence’ in state changes, aligned with an “information order” on states. Alex will look to create expressive logics and frameworks for modelling state-based computational systems that will also function as proof-relevant certificates to reasoning over systems with modal logic.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Supermartingale Certificates for Temporal Logic","description":"","teamLead":"Mirco Giacobbe, University of Birmingham ","team":"Team: Diptarko Roy, University of Birmingham; Alessandro Abate, University of Oxford","text":"The project aims to create a new theory of ‘supermartingale proof certificates’ for temporal logic specifications and ω-regular languages, with formal probabilistic guarantees. The theory will enable the development of learnable and efficiently checkable certificates for probabilistic systems that will extend and generalise all existing supermartingale certificates to date.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Hyper-optimised Tensor Contraction for Neural Networks Verification","description":"","teamLead":"Stefano Gogioso, Hashberg Ltd ","team":"Team: Mirco Giacobbe, University of Birmingham","text":"The project aims to develop ‘hyper-optimised tensor network contraction’ algorithms specifically optimised to reason about hybrid theories. These new algorithms will combine quantum simulation and automated reasoning technologies to push the boundaries in the compositional analysis of complex systems that integrate stochastic dynamics, hybrid software/cyber-physical systems and neural networks.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"A Computational Mechanics Approach to World Models via Multi-Scale Compositional Abstractions","description":"","teamLead":"Fernando Rosas, University of Sussex","team":"","text":"This project aims to develop a theoretical framework to optimise the design and analysis of AI world models. By identifying key variables and appropriate levels of granularity, Fernando will look to enable accurate simulations with minimal computational load. By introducing notions of ‘effective’ and ‘leaky abstractions,’ the framework will ensure optimal simulation of AI behaviours while balancing accuracy and efficiency. Beyond this, the project will look to set a new paradigm for world model analysis and design by improving existing world models, uncovering their compositional structure, and creating new ones.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"String Diagrammatic Probabilistic Logic: Specification and modelling languages","description":"","teamLead":"Pawel Sobocinski, Tallinn University of Technology ","team":"Team: Eigil Rischel, Tallinn University of Technology","text":"This project aims to combine advances in probabilistic modelling (Markov categories) with string diagrammatic logic (cartesian bicategories) to develop expressive graphical specification languages for probabilistic applications. Pawel’s team brings together experts from both fields to enhance string diagrams for probabilistic contexts, integrate them with first-order logic, and address the complexity of specifications.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Profunctors: A unified semantics for safeguarded AI","description":"","teamLead":"Nicola Gambino, University of Manchester","team":"","text":"This project aims to investigate the mathematical notion of a profunctor, which provides a unified and efficient concept for studying formal theories. It will explore open problems related to the category-theoretic structure of profunctors and related notions, such as symmetric sequences and symmetric multicategories. Key questions focus on tensor product for bimodules between symmetric multicategories and the differential operation for analytic functors. This will build on Nicola + team’s previous work.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Graded Modal Types for Quantitative Analysis of Higher-Order Probabilistic Programs","description":"","teamLead":"Vineet Rajani + Dominic Orchard, University of Kent","team":"","text":"This project aims to develop a compositional framework for specifying and reasoning about quantitative safety properties in machine learning, where algorithms often use randomness to make decisions under uncertainty. By building a graded modal type theory for a higher-order probabilistic programming language, Vineet + team will look to enable engineers to enforce cost optimality bounds on machine learning models directly through type checking.
","label":"","cardId":"","mediaType":null,"modules":[]}]}},{"type":"spacer-comp","data":{"type":"spacer-comp","cssSizeClass":"small","height":0}}]},{"title":"TA2 Machine Learning","text":"
TA2 Machine Learning
ARIA is launching a multi-phased solicitation for Technical Area 2 (TA2) to support the development of a general-purpose Safeguarded AI workflow. The programme aims to demonstrate that frontier AI techniques can be harnessed to create AI systems with verifiable safety guarantees. In TA2, we will award £18m to a non-profit entity to develop critical machine learning capabilities, requiring strong organizational governance and security standards.
Phase 1, backed by £1M, will fund up to 5 teams to spend 3.5 months to develop full Phase 2 proposals. Phase 2 — which will open on 25 June 2025 —will fund a single group, for £18M, to deliver the research agenda.
\nTA2 will explore leveraging securely-boxed AI to train autonomous control systems that can be verified against mathematical models, improving performance and robustness. The workflow will involve forking and fine-tuning mainstream pre-trained frontier AI models to create verifiably safeguarded AI solutions.
\n\n
Key Objectives of TA2 include:
\nKey Dates:
\nPhase 1 Application Deadline: 30th April 2025 [18:00 GMT]
\nPhase 2 Application Opens: 25 June 2025.
\nPhase 2 Application Closes: 1 October 2025.
\n
TA3 Real-World Use Cases
\nA safeguarded autonomous AI system with quantitative safety guarantees can unlock significant economic value when deployed in a critical cyber-physical operating context.
\n\n
Meet the TA3 Creators
\nWe are backing 9 teams of UK-based researchers with £4.9M to develop AI systems with unique quantitative safety guarantees to unlock transformative improvements in our critical infrastructure. This work aims to address the challenge of AI deployment in safety-critical sectors by combining scientific world models and mathematical proofs to develop robust safety assurances.
\nResearchers from diverse companies and organisations such as AstraZeneca, Mind Foundry, the University of Oxford, the University of Birmingham, and the University of York, will aim to demonstrate how safeguarded AI systems can help them to make significant improvements in vital sectors. For example, whether it can:
\nAccelerate life-saving medical breakthroughs by enabling faster and more reliable biopharmaceutical manufacturing and clinical trial design;
\nTransform the future of sustainable energy through optimised grid operations using advanced AI;
\nEnsure resilient and proactive infrastructure management using AI-driven predictive maintenance tools that can minimise disruptions and reduce costs;
\nAdvance safe and reliable autonomous transportation by enabling AI to effectively navigate complex and unpredictable driving scenarios.
\n","tabId":"","modules":[{"type":"spacer-comp","data":{"type":"spacer-comp","cssSizeClass":"small","height":0}},{"type":"creator-cards","data":{"type":"creator-cards","items":[{"title":"SAGEflex: Safeguarded AI Agents for Grid-Edge Flexibility","description":"","teamLead":"Thomas Morstyn; Jakob Foerster, University of Oxford ","team":"Yihong Zhou; Sofia Sampaio, University of Oxford","text":"
This team is looking to develop AI-based coordination of grid-edge flexibility at scale through multi-agent reinforcement learning (MARL). Despite MARL's successes elsewhere, safety concerns have hindered its adoption by power system operators. This team aims to address this by developing rigorous safety specifications, a test problem curriculum, and a software platform supporting design, benchmarking and scaling up of domain-specific safeguarded MARL solutions.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"SAINTES: Safe and scalable AI decisioN support Tools for Energy Systems","description":"","teamLead":"Dawei Qiu; Zhong Fan, University of Exeter","team":"Qiong Liu; Zhanhua Pan, University of Exeter","text":"This team is working on energy system optimisation through the development of AI-based decision support tools that are safe, scalable, and economically efficient. Their objective is to develop trustworthy and safe AI algorithms specifically tailored for energy system optimisation. The project comprises three main activities: (1) developing a physics-informed reinforcement learning (RL) algorithm to solve optimal power flow (OPF), (2) creating a scalable multi-agent reinforcement learning (MARL) algorithm for coordinating large populations of DERs, and (3) integrating these technologies into a digital twin whole-system energy model for testing and validation.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":" SAFER-ADS: Towards Safety Assurance of Frontier AI for Automated Driving Systems","description":"","teamLead":"Simon Burton, University of York","team":"Radu Calinescu; Kester Clegg; Jie Zou; Ioannis Stefanakos, University of York","text":"This team is focused on identifying how frontier AI models could be safely deployed within a full Automotive Driving Systems (ADS) context in open-world environments. The team will develop world models and safety specifications to evaluate how the Safeguarded AI methodology could scale to address increasingly complex environments, tasks and models. A safety argument that considers residual uncertainty in the assurance approach will also be developed in line with international standards.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Transforming Clinical Trial Design Using Safe and Reliable AI","description":"","teamLead":"Nijat Hasanli, Lindus Health; Nobuko Yoshida, University of Oxford","team":"Ece Kavalci, Software Engineer, Lindus Health; Adrian Puerto Aubel; David Parker, University of Oxford","text":"This team will focus on developing and validating advanced mathematical proofs and process modeling techniques to optimise clinical trial design. They will build a robust evaluation framework and performance benchmarks to test these models in real-world scenarios, ensuring they meet safety, regulatory, and operational requirements. These research outcomes will enhance their proprietary clinical trial design tool, envisioned as an intuitive, user-friendly platform that streamlines trial workflows, predicts outcomes, and mitigates risks.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Digital Custodians for Ageing Infrastructure","description":"","teamLead":"Nathan Korda, Mind Foundry","team":"Julia Bush; Mark McLeod, Claire Butcher; Harriet Bensted, Tom Bartley, Jane Williams, Mind Foundry; John Bennetts; Nicola-Ann Stevens, Ryan Ellesmere,WSP ","text":"Industry-focused steering group: Steve Roberts, Oxford University, Mind Foundry Co-Founder | Mike Osborne, Oxford University, Mind Foundry Co-Founder | Steve Denton, WSP
\nThis team’s ambition is to transform how infrastructure is maintained, making it both more cost-effective and sustainable. They will develop AI-driven agents designed to support proactive maintenance of the UK’s ageing civil infrastructure. They will use AI to quantify and forecast asset conditions, helping infrastructure managers make informed, proactive decisions. They will detail a curriculum of relevant high-stakes and high-impact use cases of AI that will then help the programme development of AI safeguards. These safeguards will provide formal guarantees that an AI model is safe to use, enabling industry adoption, and unlocking value.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"SAILS: Safeguarded AI for Logistics and Supply chain management","description":"","teamLead":"Dei Vilkinsons; Ciaran Morinan, HASH ","team":"Leah Pickering, HASH","text":"This team is developing solutions which make critical pharmaceutical supply chains more resilient and efficient through the use of AI. Their research focuses on areas of the plant-to-patient pipeline where AI can speed up decision-making, minimise waste, and better anticipate and respond to disruption, without compromising the safety or sustainability of the supply chain.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Safeguarded AI-Enabled Biopharmaceutical Manufacturing","description":"","teamLead":"Mirco Giacobbe; Leonardo Stella, University of Birmingham","team":" Paul Devine; Jared Delmar, AstraZeneca","text":"This team’s ambition is to develop a structured and reliable framework for the mathematical modelling of biopharmaceutical manufacturing processes. Their approach will incorporate formal guarantees of compliance with the industry’s rigorous safety and quality regulations to enable adoption across the pharmaceutical production process, accelerating drug discovery, and production, while significantly reducing cost.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Safeguarded AI for Energy Savings in Radio Access Networks","description":"","teamLead":"Marco Fiore; Paul Patras, Net AI ","team":"Alexis Duque; Samuel Knight; Puttatida Mahapattanakul; Rokas Gudavicius; Natalia Romankevich, Net AI","text":"The aim of this project is to revolutionise the way energy is saved in Radio Access Network operations (RANs) and promote the economic and environmental sustainability of future-generation mobile networks. The demonstration of safe and trustworthy AI-based solutions for the problem of radio element switch-on/off in RANs has the potential to address a major and critical challenge within the global mobile telco ecosystem.
","label":"","cardId":"","mediaType":null,"modules":[]},{"title":"Towards Large-Scale Validation of Business Process Artificial Intelligence (BPAI)","description":"","teamLead":"Nobuko Yoshida; David Parker, University of Oxford ","team":"Adrian Puerto Aubel; Joseph Paulus, University of Oxford","text":"This team’s work aims at providing quantitative guarantees to automated solutions in the field of Business Process Intelligence (BPI). This project will produce a workflow to analyse these systems and provide safety guarantees, based on the use of probabilistic process models and the probabilistic verification toolset PRISM. The team will collaborate with industrial partners to address relevant real-world problems and produce a set of benchmarks against which to assess AI solutions.
","label":"","cardId":"","mediaType":null,"modules":[]}]}},{"type":"spacer-comp","data":{"type":"spacer-comp","cssSizeClass":"medium","height":0}}]}],"alignCentre":false},{"type":"spacer-comp","cssSizeClass":"medium","height":0},{"type":"double-card","items":[{"title":"The Creator experience","text":"What you can expect as an ARIA R&D creator.","link":{"isActive":false,"text":"Learn more ","href":"/funding-opportunities/the-creator-experience","title":"about what to expect as an ARIA Creator"},"colour":null},{"title":"Applicant guidance","text":"Discover the process of applying for ARIA funding and find key resources.","link":{"isActive":false,"text":"Find out more ","href":"/funding-opportunities/applicant-guidance","title":"about the application process"},"colour":null}],"fullWidth":false},{"type":"spacer-comp","cssSizeClass":"medium","height":0}],"scriptsAtTop":" \n\n\n\n\n\n\n\n\n\n\n","scriptsAtBottom":"","id":2871,"languageCode":"en","pageName":"Meet the Creators","scrollSmoothness":0.0,"gtmCode":"GTM-T8Z5F55","topNav":{"logo":{"text":"ARIA - Home","href":"/media/hsxblxrf/logo-aria-black.svg"},"nodes":[{"text":"About us","href":null,"target":null,"id":null,"nodes":[{"text":"About us","href":"/about-aria","target":null,"id":"2207","nodes":[],"noOpener":false,"noReferrer":false},{"text":"Our team","href":"/about-aria/our-team","target":null,"id":"2159","nodes":[],"noOpener":false,"noReferrer":false},{"text":"Programme Directors","href":"/about-aria/our-team/programme-directors","target":null,"id":"2831","nodes":[],"noOpener":false,"noReferrer":false},{"text":"Reporting and policies","href":"/about-aria/reporting-and-policies","target":null,"id":"2160","nodes":[],"noOpener":false,"noReferrer":false}],"noOpener":true,"noReferrer":false},{"text":"What we do","href":null,"target":null,"id":null,"nodes":[{"text":"How we work","href":"/how-we-work","target":null,"id":"2817","nodes":[],"noOpener":false,"noReferrer":false},{"text":"Live opportunity spaces","href":"/opportunity-spaces","target":null,"id":"2215","nodes":[],"noOpener":false,"noReferrer":false},{"text":"Emerging areas","href":"/emerging-areas","target":null,"id":"2963","nodes":[],"noOpener":false,"noReferrer":false},{"text":"Activation Partners","href":"/activation-partners","target":null,"id":"2174","nodes":[],"noOpener":false,"noReferrer":false}],"noOpener":true,"noReferrer":false},{"text":"Funding","href":null,"target":null,"id":null,"nodes":[{"text":"Funding opportunities","href":"/funding-opportunities","target":null,"id":"2164","nodes":[],"noOpener":false,"noReferrer":false},{"text":"Applicant guidance","href":"/funding-opportunities/applicant-guidance","target":null,"id":"2162","nodes":[],"noOpener":false,"noReferrer":false},{"text":"Being funded by ARIA","href":"/funding-opportunities/the-creator-experience","target":null,"id":"2433","nodes":[],"noOpener":false,"noReferrer":false},{"text":"FAQs","href":"/funding-opportunities/faqs","target":null,"id":"2649","nodes":[],"noOpener":false,"noReferrer":false}],"noOpener":true,"noReferrer":false},{"text":"Careers","href":"https://aria-jobs.teamtailor.com/","target":"_blank","id":null,"nodes":[],"noOpener":false,"noReferrer":false}],"headerLinks":[{"target":"","isActive":false,"text":"Become a Programme Director","href":"/about-aria/our-team/programme-directors/cohort-3","title":""},{"isActive":false,"text":"Opportunity spaces","href":"/opportunity-spaces","title":""}],"menuLinks":[{"isActive":false,"text":"Contact us","href":"/contact","title":""},{"isActive":false,"text":"Terms of use","href":"/terms-and-conditions","title":""}],"activeItem":"2871","menuText":"Menu","menuTextClose":"Close menu","search":{"isActive":false,"text":"Search","href":"/search","title":""},"animationOffText":"Motion: Off","animationOnText":"Motion: On"},"footer":{"header":"Help us drive momentum ","text":"ARIA is a non-departmental public body, sponsored by the Department for Science, Innovation + Technology.","copyright":"Copyright 2026","headerLinks":[{"isActive":false,"text":"Contact","href":"/contact","title":""},{"target":"_blank","isActive":true,"text":"Careers","href":"https://aria-jobs.teamtailor.com/","title":""}],"socialHeader":"Follow our progress","footerLinks":[{"isActive":false,"text":"Privacy Policy","href":"/privacy-policy","title":""},{"isActive":false,"text":"Terms and Conditions","href":"/terms-and-conditions","title":""},{"isActive":false,"text":"Cookie Policy","href":"/cookie-policy","title":""},{"isActive":false,"text":"Accessibility Statement","href":"/accessibility-statement","title":""},{"isActive":false,"text":"Accessibility Support","href":"/funding-opportunities/accessibility-support","title":""},{"target":"_blank","isActive":true,"text":"Careers","href":"https://aria-jobs.teamtailor.com/","title":""},{"isActive":false,"text":"Supply to us","href":"/supply-to-us","title":""}],"socialItems":[{"link":{"target":"_blank","isActive":true,"text":"ARIA Research Twitter","href":"https://x.com/aria_research","title":""},"type":"x"},{"link":{"target":"_blank","isActive":true,"text":"LinkedIn","href":"https://www.linkedin.com/company/advanced-research-and-invention-agency","title":""},"type":"Linkedin"},{"link":{"target":"_blank","isActive":true,"text":"ARIA Research Substack","href":"https://ariaresearch.substack.com/","title":""},"type":"SubStack"}],"formText":"","formSubmit":"Sign up","formId":"","recaptchaSiteKey":"6LcuyY4bAAAAAE2OzRFfA7vDWyohfZXyl2uTuHLa","verificationToken":"","redirectUrl":null,"submitMessage":"","formTheme":""},"seo":{"title":"Meet the Creators | Safeguarded AI","description":"Meet the Creators working on ARIA's Safeguarded AI programme. Backed by £59m, this programme aims to develop the safety standards we need for transformational AI.","keywords":"safeguarded ai, aria programme research, funding research teams, programme teams, aria creator teams","includeInSitemapXml":true,"canonicalTag":""},"sharing":{"og":[{"property":"og:title","content":"Meet the Creators | Safeguarded AI"},{"property":"og:description","content":"Meet the Creators working on ARIA's Safeguarded AI programme. Backed by £59m, this programme aims to develop the safety standards we need for transformational AI."},{"property":"og:image","content":"https://aria.org.uk/media/ipab0gpu/safeguarded-ai-programme.jpg?width=600&format=webp&quality=100&v=1db669bb49aced0"},{"property":"og:url","content":"https://aria.org.uk/opportunity-spaces/mathematics-for-safe-ai/safeguarded-ai/meet-the-creators"}],"twitter":[{"name":"twitter:card","content":"summary_large_image"},{"name":"twitter:site","content":"@ARIA_research"},{"name":"twitter:title","content":"Meet the Creators | Safeguarded AI"},{"name":"twitter:description","content":"Meet the Creators working on ARIA's Safeguarded AI programme. Backed by £59m, this programme aims to develop the safety standards we need for transformational AI."},{"name":"twitter:image","content":"https://aria.org.uk/media/ipab0gpu/safeguarded-ai-programme.jpg?width=600&format=webp&quality=100&v=1db669bb49aced0"},{"name":"twitter:url","content":"https://aria.org.uk/opportunity-spaces/mathematics-for-safe-ai/safeguarded-ai/meet-the-creators"}]},"pageType":"programmePage"}