Π

I'm Fast, I'm Reliable, and I eat Complexity.I'm Petra. A Simplified, High-Performance Computing, Object-Oriented Language Subset, with native Software Formal Verification, for Real-Time AI, Simulation and Decision Engines.Supports Java, C++ and more, deploying to CPU and Hardware Accelerators.

Case Study.

Our case study validates that Petra secures critical business logic by enforcing mathematically proven state transitions. We verified a complex algorithmic trading strategy in just 77ms proving the code’s adherence to specifications while instantly surfacing validation-level logic flaws. For autonomous decision engines, this technology provides a "deterministic safety layer" that transcends probabilistic testing, by guaranteeing that state changes obey strict regulatory and operational axioms, Petra ensures high-stakes automated systems never execute undefined or unsafe behaviours.

About.

We are an innovation lab that's been building the "containment layer" for autonomous AI agents from the ground up. Powerful AI such as LLMs are now being granted execution privileges, therefore probabilistic safety filters are insufficient. We are developing a formally verified runtime environment—a "mathematical sandbox"—that enforces safety axioms at the code level, and Petra is at the core of this technology.

What is Petra?

Petra is the most concise and scalable way to build and formally verify large and complex systems.
Watch our video below to learn more:

How does it look?

Have you every wanted to prove your critical systems correctly transition between states?
Petra makes this possible, through its all-in-one integrated formal modelling and software development language standard, allowing you to manage complexity using simplified formal methods:

/* Light = Power X Control = {on} X {on,off} = {(on,on),(on,off)} /
public final class Light {
     private final Power power = new Power(); / Power = {on} /
     private final Control control = new Control(); / Control = {on,off} /     @Initial
     public boolean off() { return power.on() && control.on(); } / off = {(on,on)} /
     public boolean on() { return power.on() && control.off(); } / on = {(on,off)} /     public void toggle() {
         if (off()){
             control.turnOn();
             assert(on()); / unreachable state {(on,off)} /
         } else if (on()){
             control.turnOff();
             assert(off()); / unreachable state {(on,on)} */
         }
    }
}

How it works?

1. Model / DevelopUse Petra's language standard to formally model complex systems. The models are just executable programs, hence they can also replace/upgrade current software components.

2. VerifyAt the touch of a button, automatically verify state transitions with fast results, even for large object-oriented systems, thanks to Petra's abstraction oriented design.

3. Explainable FeedbackUnlike traditional formal methods, our error messages are explainable, relating directly to the states encoded within the applications language domain.

Benefits?

Object-oriented, Fast.Fully integrates with existing code, workflows and IDEs using a linter for Java, C++, etc. Executes on Accelerated Hardware.

Developer friendly.Petra is the easiest and most comprehensive formal method to learn for everyday developers. Just learn the rules, write code and press verify.

Flexible to adopt.Use as much or as little of Petra as you like. Use it to manage complexity by modelling and/or developing complex systems from the ground up, or use it to rewrite specific components.

Join us.

Petra is now being developed and maintained by
Cognition Box Technologies Ltd (16683272), London, UK.

Π