Petra FAQ

FAQ

1. What is Petra Programming, and how does it differ from Java or other paradigms?

Petra is a subset of Java 8 designed for formal modelling and software development, integrating code, proof, and natural language for high-trust systems. Unlike full Java, Petra emphasizes formal verification of state transitions using annotations and assertions, ensuring robust, safe code for complex systems. It prioritises abstraction-oriented design over Java’s general-purpose flexibility. Learn more.

2. What are the system requirements and how do I install the Petra tools?

Petra requires a Java 8+ JVM and runs on Windows, macOS, or Linux. A compatible IDE like IntelliJ IDEA is recommended and the language level of Java should be set to 8.

3. How do I write and run my first “Hello Petra” program?

Petra requires at least a Java main entry point class, a Petra root object and a Petra base object.
Petra requires all classes to be created in separate files.
Petra program classes can be developed in a bottom-up or top-down style (with respect to the program tree), or a mix of both.
For simple demonstration we will start from bottom-up in this simple example.

First we create a Logger base object (remember Petra is a just a subset of Java 8 so classes can be given any name as usual in Java).

@Base public final class Logger {
    private boolean enabled = false;

    @Initial
    public boolean disabled() { return !enabled; }
    public boolean enabled() { return enabled; }

    public void sayHello() {
        if (enabled()){
            System.out.println("Hello Petra");
            assert(enabled());
        }
    }

    public void enable() {
        if (disabled()){
            enabled=true;
            assert(enabled());
        }
    }
}

Then we create the HelloPetra Petra root object. For our example this is the one and only Petra non-base object however large Petra objects will contain many non-base objects and always a single root object.

public final class HelloPetra {
    private final Logger logger = new Logger();

    @Initial
    public boolean disabled() { return logger.disabled(); }
    public boolean enabled() { return logger.enabled(); }

    public void run() {
        if (disabled()){
            logger.enable();
            assert(enabled());
        } else if (enabled()){
            logger.sayHello();
            assert(enabled());
        }
    }
}

Finally we create the Java program entry point class Main.java which invokes the Petra root.

public class Main {
    public static void main(String[] args){
        HelloPetra helloPetra = new HelloPetra();
        helloPetra.run(); // first call enables the logger
        helloPetra.run(); // second call prints Hello Petra!
    }
}

Core Usage

4. What are the key language features and syntax basics?

Petra extends Java 8 with a small set of formal annotations, strict structural rules, and built-in verification support. It allows developers to write code that can be automatically checked for correctness with respect to state transitions and invariants.

Key language features include:

Annotations for formal specification:
- @Base — Marks a class as a base object. These encapsulate “assumed” or external behaviour (e.g., I/O, library calls) that is not formally verified but treated as trusted. Base objects are restricted to primitive fields only.
- @Initial — Identifies the method that defines the initial state of an object. This is used by the verifier as the starting point for exploring reachable states.
- @External — Used for helper classes that provide access to external Java functionality (e.g., sockets, files) while keeping the core Petra logic clean.
- @NonDet — Marks a state method as non-deterministic. This indicates that the method may return different values across different runs or invocations, even under the same apparent conditions (for example, due to external inputs such as an LLM response, sensor data, or random choice). The verifier treats calls to @NonDet methods as capable of producing any valid return value consistent with the object’s state model, rather than assuming a single deterministic outcome. This is essential for modelling real-world systems with uncertainty or external services/agents.
State transition discipline:
- Objects maintain a clear separation between base objects (unverified wrappers) and non-base objects (formally verified). Every non-base object has exactly one root object at the top of the hierarchy.
- Methods typically follow a guarded style: if (currentState()) { ... newState(); assert(newState()); }. This makes state changes explicit and verifiable.
How the initial state is traced through the hierarchy:

The @Initial method defined in a base object (or a lower-level non-base object) is automatically propagated upwards through the object hierarchy. If a non-base object depends on the initial state of a child object (by calling its @Initial method directly or indirectly), the verifier treats the calling method as part of the initial-state calculation. This propagation continues all the way up to the root Petra object. As a result, the root object’s own @Initial method must correctly compose the initial states of all its child objects, ensuring a single, well-defined starting point for the entire verified system.
How non-determinism is traced through the hierarchy:

Non-determinism introduced by @NonDet methods (often in base objects that interact with the external world) is automatically propagated upwards through the object hierarchy. If a non-base object calls a @NonDet method (directly or indirectly via other objects), the calling methods in the non-base layers are also treated as potentially non-deterministic by the verifier. This propagation continues all the way up to the root Petra object. As a result, any method in the root object that depends on non-deterministic behaviour must either be marked @NonDet itself or have its possible outcomes explicitly handled and verified across all branches.
Assertions and verification:
- Standard Java assert statements are used to declare post-conditions and invariants. The Petra verifier statically checks that these assertions always hold after state transitions.
Structural rules (syntax basics):
- All Petra classes must be in separate files (one public class per file, as in Java).
- Non-base objects require up-front initialisation of all fields in their constructors or field declarations.
- State query methods (e.g., enabled(), disabled()) are pure and used to guard transitions.
- Complex logic or external side effects are pushed into base objects; non-base objects focus on high-level, verifiable control flow.
Abstraction and hierarchy:
- Petra encourages building large systems through a tree of objects. Formal verification is performed compositionally across the hierarchy rather than on a single monolithic model.

Simple Petra-Java syntax example (building on the Hello Petra program):

// In a non-base object
private final SomeBase base = new SomeBase();

@Initial
public boolean initialState() {
    return base.isInitial();
}

public boolean readyState() {
    return base.isReady();
}

public void performAction() {
    if (initialState()) {
        base.transitionToReady();
        assert(readyState());   // verified post-condition
    }
}

Petra’s syntax remains very close to Java 8, so existing Java developers can adopt it quickly. The main differences lie in the disciplined use of annotations, state-guard and transition patterns, and the separation of verified versus assumed code.

5. How do I handle calls to external libraries or I/O?

These must be handled through calls within the Petra base objects. The base objects can only contain primitive fields and so static utility classes should be used for arbitrary Java operations which are outside of Petra’s syntax.

@External
public final class IOHelper {
    private final ServerSocket serverSocket = new ServerSocket();
    public static boolean isDataReady() { /* use socket server to make decision */ }
}

6. Are there any performance considerations or best practices?

Petra’s verification adds minimal overhead but scales efficiently.
Avoid complex state models (i.e. less than 2^16 states per object) to prevent verification delays. This is more than enough for most applications as the true scale of Petra comes from the object hierarchy and abstraction mechanism. For more niche highly mathematical applications such we have an arbitrarily large symbolic sets solver in development.
In terms of execution, Petra’s Java subset requires up-front initialisation of all fields in non-base objects, which keeps garbage collection low.
Care should be taken when programming the arbitrary “assumed” code in Petra base objects in order to avoid performance issues, see below for examples.

@Base public final class Logger {
    private boolean enabled = false;

    @Initial
    public boolean disabled() { return !enabled; }
    public boolean enabled() { return enabled; }

    public void sayHello() {
        if (enabled()){
            System.out.println("Hello Petra!");
            assert(enabled());
        }
    }

    public void enable() {
        if (disabled()){
            enabled=true;
            try {Thread.sleep(10000);} catch (Exception e){} // obviously unnecessary and would cause a performance issue.
            for (int i=0;i<Integer.MAX;i++){new String();} // obviously unnecessary and would create huge amounts of garbage to collect.
            assert(enabled());
        }
    }
}

Troubleshooting and Support

7. What are the most common errors and how do I debug them?

Initially when learning Petra the most common errors in programming will be to do with getting used to the Petra syntax which is a subset of Java 8. Once developers are more comfortable with this, verification issues will take over. More on these will be discussed in the Petra Rules section.

8. How can I integrate Petra with existing codebases or languages?

Petra integrates with Java 8 codebases via direct inclusion. For calls to non-Java languages within the base objects, use process builders or JNI. Other versions of Petra are in development for example there will be a direct translation of the system to support a Petra compliant C++ subset.

Community and Advanced Topics

9. Where can I find tutorials, examples, case studies or more resources?

10. How can I contribute to the Petra project or report bugs?

Petra is maintained by PetraCode Ltd. Submit feedback, bug reports, or contribution inquiries via aran@petracode.co.uk.

This FAQ is updated based on user feedback. Contact aran@petracode.co.uk with suggestions. Last updated: 19 April 2026.