I'm Petra

It’s time to switch on: model complex domains, prevent critical errors, and eliminate risk.
Build bulletproof Java with our scalable OOP formal verification methods and integrated linter.

public final class Light {
     private final Power power = new Power();
     private final Control control = new Control();     @Initial
     public boolean off() { return power.off() || control.off(); }
     public boolean on() { return power.on() && control.off(); } // validation error: inconsistant with domain model.     public void toggle() {
         if (off()){
             sep(()->{power.turnOn();},
                 ()->{control.turnOn();});
             assert(on()); // verification error: unreachable state.
         } else if (on()){
             sep(()->{power.turnOff();},
                 ()->{control.turnOff();});
             assert(off());
         }
    }
}

• Case Study
• Services
• [email protected]