Î
I'm Petra. Beyond Testing — Software that is Correct by Construction.
Why wait for production to find a failure? Petra brings mathematical rigor to your critical logic and Agentic AI, proving your software is safe and secure before it ever runs.
Why Now?
Testing is no longer enough for software and agentic AI due to complexity.
We cannot trust humans or AI to come up with the necessary test cases to prevent critical failures, there are too many possibilities and the test cases have become too complex to reason about.We need a better approach, and simplified formal verification is the answer. Formal verification can prove behaviour across entire ranges of values automatically, with no possibilities missed.Traditionally, formal verification has been difficult to apply and does scale well, however Petracode fully automates formal verification, integrated within the Java ecosystem, in a way that's scalable and easy for developers to use.
How I work?
I'm a verifiable, object-oriented subset of Java, C++ which I formal verify by reading your code, not replacing your environment. Run on your own terms; deploy to any CPU or GPU Accelerator.Built for businesses where precision, speed and reliability is critical.
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, 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.
Pricing.
| ÂŁ | Community | Professional | Enterprise |
|---|---|---|---|
| Price | Free (education and commercial testing) | ÂŁ249/user/month | Custom Pricing |
| Builds | 3 standard verification builds/hour | 30 fast verification builds/hour | Unlimited fast verification builds/hour |
| Hosting | Public GitHub | Private GitHub | Custom Repo |
| Languages | Java | Java | Java / C++ |
| Verification Depth | Entire program tree excluding leaves | Entire program tree excluding leaves | Entire program tree including leaves |
| Tools | N/A | N/A | IDE Verification Plugin |
| Execution | CPU | CPU | CPU / GPU |
| Support | Community | Professional | Enterprise |
Support.
Community.- GitHub- Discord- Stack Overlow
Professional.- AI Expert Voice/Text Chatbots- Access to training courses and quizzes
Enterprise.Extends Professional with:- Access to advanced training courses and quizzes- Custom training courses- Custom tooling
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.
Subscribe.
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 users and assets 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.