AI in Kry10's world

Ask five people at Kry10 what "we're working on AI" means and you will get five different answers, because it isn't just one thing. I think about it in four categories:

1. how we use AI on ourselves,
2. how we help others design with it,
3. how we host it on a device, and
4. how we give safe access to it in the cloud.

Here's where we actually stand on each, including two pieces of real, current work.

1. Internally, we use AI like many others: checking the grammar in our own documentation, aligning processes that have grown as our company scales, the everyday productivity work that most companies are doing right now.

One of our formal methods engineers has also been experimenting, on work outside any client-restricted project, with AI helping to write formal verification syntax. It's the mechanical layer, not the reasoning, and that is exactly what AI is suited to. Early days, but promising.

2. Separately, we have also been running a more substantial effort, having AI work through our own documentation, catch the logical errors in it, and build a context file. We are, in effect, building a training set so that AI can help build future systems. That is not a finished product, but it is the groundwork for an external design capability, robustly developed before we put anything in front of a customer.

An external design capability is where AI eventually helps someone else build a system on our platform by describing what they need in plain English rather than writing it from scratch. We are not there yet in any shippable sense, but the ARPA-H groundwork above is a direct step toward it.

3. If you want to see AI doing real work today, I’d point you to on-device applications, such as small models doing one narrow job, hosted on hardware small enough to fit inside the device itself.  Our engineering team is actively working on hosting small models on machines a similar size to a Raspberry Pi. This capability could be suited to decisions such as a power network deciding in real time which line to route electricity down based on temperature and load, or a vehicle's vision system deciding where to turn. There would be no human in this loop, and no need for a data centre.

4. The fourth category, safely accessing a frontier model in the cloud, isn't about improving the model, it’s about guarding the model and its end user. This is where formal verification will really come into play, to protect the value of frontier model (regardless of how many billions of parameters it is and the billions of dollars it cost to train) and its users. Protecting those, and the physical infrastructure underneath them, is squarely formal verification's job, not AI's.

Kry10 is currently testing whether formal verification can be used to restrict what a model can do and access on a local machine. We have the first example of this running now. And it’s exciting!

None of this is finished, most of it is early, but that’s where we stand right now. It’s the clearest answer I can give you to "what is Kry10 actually doing with AI." ®

At Kry10, our job is to strengthen the foundations beneath the critical systems that society depends on every day. Kry10 provides mathematically proven foundations that help keep critical services resilient by design. KOS, our formally verified operating system, is built on seL4®, the world’s most highly assured operating system kernel. Our OT Network Guard extends that foundation to the boundary between trusted systems and untrusted networks, wherever that boundary appears.

As part of the Cyberargentur EVIT (Ecosystem Formally Verifiable IT – Provable Cybersecurity) Program, Kry10 is partnering with Proofcraft to explore how to build modern critical and cyber-physical systems based on seL4® that are verified, performant and dynamic.

This project is a wide-ranging verification and research project to improve the status of seL4® and Kry10 OS’s functionality and assurance in both use of multiple cores and user-space verification.

Kry10.com

LinkedIn: Kry10

LinkedIn: Boyd Multerer