Π

I'm Petra. A new way to code reliably.

Join us.

What we do?

We use our Petra software development method and tooling to align code, proof and natural language, for trust and safety, de-risking complex software and models. Additionally we offer Petra training, tools and consulting services to your technology team and partners.

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 business 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.Fully integrates with existing code, workflows and IDEs such as IntelliJ, using a linter for Java, C++ and more.

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.

How can I find out more?

Read our case study, click services to book a web call, send us an email, or back our Kickstarter!

Join us.

Petra is being developed and maintained by Petracode Ltd (16684944), London, UK.