Î
I'm Fast, I'm Reliable, and I eat Complexity.I'm Petra. A simplified, object-oriented language subset, with native software formal verification,
support for 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 under 100ms proving the code’s adherence to specifications while instantly surfacing validation-level logic flaws. 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.
Petra is the brainchild of Aran Hakki, the founder of Petracode.co.uk, a pioneering platform dedicated to advancing software reliability and security. Holding an MEng in Systems Engineering from the University of Warwick, and a PhD in Computer Science from the University of Southampton, Aran specialized in Formal Methods and Software Verification, laying the foundation for his expertise in building robust, error-free systems. His passion for software reliability stems from a commitment to safeguarding business-critical and safety-critical operations, fuelled by a pivotal moment when he witnessed a trading error that cost thousands of pounds—sparking his drive to innovate and prevent such vulnerabilities.Aran is deeply invested in high assurance cyber security and safety, protecting assets and users in an increasingly digital world. Equally committed to education, he aims to teach formal software methods to a broader audience, democratizing access to these powerful tools. Through Petra, Aran is empowering developers and organizations worldwide to create verifiable, secure software and models, that drives innovation without compromise.
What is Petra?
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.