Safeguarded AI (Part 2)

60 people, including a lot of category theorists, are meeting in Edinburgh for the £59 million UK project called Safeguarded AI. I talked about it before here.

The plan is to build software that will let you precisely specify systems of many kinds, which an AI will design, and verify that what the AI designed meets your specifications. So: it’s not about building an AI, but instead, building a way to specify jobs for it and verify that it did those jobs correctly!

The director of this project, David Dalrymple, has changed the plan recently. There were many teams of category theorists designing formalisms to get this job done. David Jaz Myers at Topos Research UK was supposed to integrate all these formalisms. That would be a huge job.

But recently all but a few teams have been cut off from the main project—they can now do whatever they want. The project will focus on 3 parts:

1) The “categorical core”: a software infrastructure that lets you program using category theory concepts. I think Amar Hadzihasanovic, my former student Owen Lynch, and two others will be building this.

2) “DOTS”: the double operadic theory of systems, a general framework for building systems out of smaller parts. This is David Jaz Myers’ baby—see the videos.

3) Example applications. One of these, building colored Petri nets, will be done by my former student Jade Master. I don’t know all the others.

By September 2026, David Jaz Myers, Sophie Libkind, Matteo Capucci, Jason Brown and others are supposed to write a 300-page “thesis” on how this whole setup works. Some of the ideas are already available here:

• David Jaz Myers and Sophie Libkind, Towards a double operadic theory of systems.

It feels funny that so much of the math I helped invent is going into this project, and there’s a massive week-long meeting about it just a ten minute walk away, but I’m not involved. But this was by choice, and I’m happier just watching.

I apologize for any errors in the above, and for leaving out many other names of people who must be important in this project. I’ve spoken to various people involved, but not enough. I’m going to talk to David Jaz Myers tomorrow, but he wants to talk about what I’m really interested in these days: octonions and particle physics!