Developing correct-by-construction world models for verification of frontier AI
Developing correct-by-construction world models for verification of frontier AI
Project Details
Updated 10/25/26 · By grantmaking.aiProject summary
We aim to develop the theory and practice of SDCPNs (Stochastic Dynamic Colored Petri Nets) so that they may serve as a suitable world model for verification of AI. SDCPNs are a flexible data structure, as well as scientific model, which has application to self-driving cars, power-grid management, supply chains, agent-based epidemiology and more. SDCPNs are categorical and compositional, meaning that they can be trusted structurally while scaling to the size of real world problems.
What are this project's goals? How will you achieve them?
We are creating a control theory and probablistic model checking framework for SDCPNs which is analogous to the theory of Stochastic Differential Equations (SDEs). We are doing this in the language of category theory so we may leverage compositionality to scale SDCPN analysis to real-world problems.
In particular, we are making proof-of-concept implementations alongside peer reviewed papers which prove the correctness of these implementations. We will continue to work with the other groups in the SGAI program to develop the mathematics and software necessary to develop a next generation AI verification system.
How will this funding be used?
As we are already funded by ARIA, this funding will be used as a cash-float and contract extension. Since our above grant payments are in arrears these funds will allow us to pay our bills on time as well continue our work beyond the 1-year contract.
Who is on your team? What's your track record on similar projects?
Jade Master: Project lead, over 8 years of experience in academic theoretical computer science, started Coherence Research to apply her work on compositionality and Petri nets to the problem of AI-safety. Started a spin-off company (GLAIVE research) for phase 1 of the SGAI programme, which has recieved a 2-year grant from Renaissance Philanthropy to study machine generated proofs.
Dylan Braithwaite: Currently managing the above spin-off. Finishing a Ph.D in applied category theory.
Timotej Tomandl: Years of experience in Agda formalization of categorical concepts.
Sean Watters: Ph.D in categorical model checking and type theory.
What are the most likely causes and outcomes if this project fails?
The SGAI program fails to have a suitable world model engine. The technology of AI gatekeeping is never sufficiently developed and AI continues to be unsafe.
How much money have you raised in the last 12 months, and from where?
279,000 GBP from Advanced Research and Inventions Agency (ARIA)
People
Updated 10/25/26 · By grantmaking.aicreator
Funding Details
- -
- -
- -
- -
- -
- -
- -
- $39,009
- -
- -
[Progress update]
What progress have you made since your last update?
We have further developed the categorical foundations of SDCPNs and their generalizations as well developed an initial approach to their model checking using Monte Carlo optimization (which is now in use in Petrinaut)
The team has taken on two new contractors who are experts in Petri net theory and stochastic control theory.
What are your next steps?
We have been continued on to Phase 3 of the SGAI program with new projects and goals. These include:
Developing a temporal logic for SDCPNs which optimizes the model based on a safety spec, improving on the Monte Carlo method we have already developed.
Using category theory to generalize SDCPNs to related models and develop compositionality theorems to manage their state space explosion.
Generalizing region theory with categories to allow for correct-by-construction synthesis of SDCPNs and related structures.
Supporting the other SGAI teams so that our combined final output will be based on rigorous foundations.
Is there anything others could help you with?
After the SGAI program ends in November 2027 there will still be more work to do on the theory of model checking SDCPNs and their generalizations. We are already putting out feelers for potential funding sources which would allow us to do this work.