PETRA - A Java Library for critical enterprise systems.

We have developed a revolutionary way to program and verify complex Java software, in order to evolve systems faster, more securely, with lower risk and at a lower cost.

  1. Simplify Reasoning with PETRA

The PETRA paradigm simplifies reasoning and programming of complex software.


  • A Java DSL

  • Naturally Parrallel and Distributed

  • Purely functional and Object-oriented

  • Simple to learn with minimal operations and syntax

  • Graph Programming with State

  • Robust and fault tolerant

  • Turing Complete

  • Expressive

  • Scalable

2. Verify with Exhaust

Systems created using PETRA can be automatically verified for correctness using the Exhaust system.

Exhaust uses intelligent fuzzing to dictionary attack PETRA defined flows, in order to prove or disprove reachability.

3. Deploy

Once verified choose to run in-process or deploy to cloud and enjoy Hazelcast’s distributed computing performance and fault-tolerance.

PETRA provides the same logical output across 3 modes of operation:

DIS - Distributed across a Hazelcast cluster (

PAR - Parallelized across available cpu cores

SEQ - Sequential, runs in a single thread, useful for debugging


PETRA has a Java library, just reference the .jar file and code straight out the box. Below is a taste of what its like to program in PETRA:

// Define a class X which is deconstructed into A and B
class X { 
	@Extract A a = new A();
	@Extract B b = new B();
        public boolean isOk(){ return a!=null && b!=null;}
// Define a stateful graph, mapping X to Y, each graph has its own isolated heap.  
class XtoY extends XGraph {
        consumes(extract(X.class,x->x.isOk())); // define a pre-condition, for the input
	// define any number of parallelizable steps
	step(some(B.class,b->b.isOk()), b->new D(),some(D.class,d->d.isOk()));
        step(new AtoC()); // steps can be nested
	// define any number of data joins, acting across objects in the graphs heap.
	join(some(C.class,c->c.isOk()), some(D.class,d->d.isOk()), (c,d)->new Y(),y->y.isOk()); 
        produces(some(Y.class,y->y.isOk())); // define a post-condition, for the return
// kick off root graph, this happens once per process.
Y y = new LogicComputer().computeWithInput(new XtoY(),new X());