Skip to content

Proving something

5. INVARIANT: a property that is proven, not tested

This is where zqel stops being “ST with nicer syntax” and becomes something new.

An INVARIANT is a statement that must be true in every reachable state of the block, forever. It is not a comment and not a runtime check — it is a proof obligation. The compiler proves it using one-step induction, which is easier than it sounds:

Just as important: an INVARIANT does not create behaviour. The rules still define what the block does; the invariant is only something that behaviour must satisfy. If the proof fails, zqel rejects the block — it does not “repair” your logic for you.

That is the key difference between verification and synthesis:

  • Verification asks: “Do these rules satisfy the property?”
  • Synthesis would ask: “Find me rules that satisfy the property.”

zqel in this guide is about the first question.

  • Base case: the invariant holds in the initial state (all outputs at their power-on defaults — 0 / FALSE).
  • Inductive step: assuming the invariant holds at the start of some scan, it still holds at the end of that scan (after one update).

If both hold, then by induction it holds forever — exactly like a row of dominoes: if the first one falls (base case) and each one knocks over the next (step), then all of them fall, no matter how many there are. You never have to check them one by one.

For the counter above, Value <= 10 is proven like this: it is 0 <= 10 at power-on (base), and if Value <= 10 now, the rules ensure it is still <= 10 after one scan (the saturate-hold rule at priority 20 catches the boundary). So it can never exceed 10 — for any sequence of button presses, of any length.

When a proof fails, you get a counterexample

Suppose we forget the saturating rule:

    Value:
        SET Value + 1 WHEN Count PRIO 10;   // just count up, no limit!
        HOLD OTHERWISE;
    INVARIANT
        Value <= 10;                        // ... but still claim this

The claim is now false, and zqel refuses to compile it:

verification failed:
  [invariant-step] invariant can be violated after one cycle: (Value <= 10)
      counterexample: Count=1, Value=10

Read that as a precise accusation: “Start a scan with Value = 10 and Count = 1. After one update Value becomes 11, so your invariant is false.” It is not a vague “test failed” — it is a specific reachable situation that breaks your claim. Fix the logic (add the saturating rule) or fix the claim; the compiler will not let you ship a false promise.

✅ Proven vs. ✅ tested. A test runs a handful of scenarios you thought of. An invariant proof covers all scenarios, including the ones you did not think of. The counterexample above is exactly one you might have missed.

Three non-obvious bugs the compiler catches for you

The nice examples are the ones where a human reviewer might plausibly nod the code through — and the compiler still says no.

(a) The hidden overflow bug. In PLC land an INT is not mathematical ℤ; it is 16-bit hardware arithmetic. So this innocent-looking block is wrong:

FUNCTION_BLOCK BadCounter
VAR_INPUT Count : BOOL; END_VAR
VAR_OUTPUT Value : INT; END_VAR
IMPLEMENTATION
    Value:
        SET Value + 1 WHEN Count PRIO 1;
        HOLD OTHERWISE;
    INVARIANT
        Value >= 0;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

A programmer may think “it only counts up, so it stays non-negative”. The machine knows better: at Value = 32767, adding one wraps to -32768, and the invariant fails. The point is not that wraparound exists — everyone knows that in the abstract — but that the compiler catches the exact moment where your intuitive, infinite-integer reasoning diverges from the plant.

(b) The missing bound on a dynamic read. An array access with a runtime index often “looks obviously safe” because a human silently carries some intended bound in their head. The compiler does not guess:

selected := Channel[sel];

If nothing proves sel in range, zqel reports a concrete violating state such as sel = -32768. That is a classic field bug: the logic is fine assuming the HMI or upstream block never sends nonsense, but the assumption was never written down.

(c) The specification hole disguised as a proof success. Formal tools do not only find buggy implementations; they also expose buggy specifications. “sorted” without “is a permutation” admits “write zeros everywhere”; “Pressure < 10 bar” admits “pump off forever, valve open forever”. The proof goes through, and that is precisely the warning sign: a proof can be perfectly correct and still certify the wrong thing. zqel forces that distinction into the open early, while the block is still small.

6. A safety property worth proving: mutual exclusion

Consider two motors that must never run at the same time (they might drive the same shaft from opposite directions — running both would wreck it). Motor A has priority; Motor B must yield (examples/motor.zqel):

    MotorA:
        OFF WHEN StopA  PRIO 10;   // stop always wins over start
        ON  WHEN StartA PRIO 5;
        HOLD OTHERWISE;

    MotorB:
        OFF WHEN StopB  PRIO 10;
        OFF WHEN MotorA PRIO 10;   // yield while A was already running at scan start
        OFF WHEN StartA PRIO 10;   // also yield while A is being STARTED this scan
        ON  WHEN StartB PRIO 5;
        HOLD OTHERWISE;

    INVARIANT
        NOT (MotorA AND MotorB);   // the safety property: never both on

✅ Proven: NOT (MotorA AND MotorB) — it is impossible, for any sequence of button presses, for both motors to be on in the same scan.

The generated ST shows the interlock baked right into Motor B's formula:

    (* proven invariant: NOT (MotorA AND MotorB) *)
    _MotorA_next := (NOT StopA AND (StartA OR MotorA));
    _MotorB_next := (NOT StopB AND NOT MotorA AND NOT StartA AND (StartB OR MotorB));
    MotorA := _MotorA_next;
    MotorB := _MotorB_next;

Notice NOT MotorA AND NOT StartA inside Motor B: B can only turn on when A is neither running nor being started. That is why the invariant holds — and the compiler checked that the formula it generated really does guarantee it, rather than trusting you to have gotten the interlock right by hand.

6a. The same block, said as a contract

Everything above sits inside IMPLEMENTATION, and there the register rules are the block: they say what it does, and that is the end of it. There is a second place to put them, and the difference is worth a page because it is the one the rest of the toolchain is built on.

FUNCTION_BLOCK MotorControl
VAR_INPUT
    StopA  : BOOL;
    StartA : BOOL;
    StopB  : BOOL;
    StartB : BOOL;
END_VAR
VAR_OUTPUT
    MotorA : BOOL;
    MotorB : BOOL;
END_VAR

CONTRACT
    MotorA:
        OFF WHEN StopA  PRIO 10;
        ON  WHEN StartA PRIO 5;
        HOLD OTHERWISE;

    MotorB:
        OFF WHEN StopB  PRIO 10;
        OFF WHEN MotorA PRIO 10;
        OFF WHEN StartA PRIO 10;
        ON  WHEN StartB PRIO 5;
        HOLD OTHERWISE;

    INVARIANT
        NOT (MotorA AND MotorB);
END_CONTRACT
END_FUNCTION_BLOCK

Same rules, same proof, same generated code — and examples/motor_contract.zqel is this file, compiled by the same gate that compiles every other example. What changed is the standing of those rules. In CONTRACT they no longer say what the block does; they say what any implementation of it must do.

That only starts to pay when an IMPLEMENTATION is added underneath:

  • A register there for an output the CONTRACT does not name behaves exactly as in section 6 — the ordinary case, unaffected.
  • A register for MotorA or MotorB becomes a candidate. The compiler admits it only after proving that its step function and the contract's agree on every state and every input. A countermodel rejects it, and so does an unknown or a timeout: not proved is not accepted.
  • BY <artifact>; in place of a register binds an external artifact — Rust, ST, something a vendor shipped — to the same obligation (§12.3 of the Language Reference).

So the rules you would have written by hand in section 6 become the thing that judges whatever gets written instead — hand-written, generated, or synthesised. The workflow around that is the realization ladder; its rungs are workflow states, not new syntax, and every one of them is judged against the block above.

One restriction to know before you move clauses across: the typed relational clauses (ONLY_WHEN, IMPLIES, IFF, EXCLUDES) are not admitted in CONTRACT. That surface is deliberately still open, and a RULE carrying one is refused there rather than quietly accepted.

6b. PARAMETER: one block, many machines

The counter in section 4 saturates at ten. Every real installation wants its own limit, and copying the block to change one number is how a codebase acquires six slightly different counters.

A PARAMETER is a value fixed once when the instance is configured and immutable for its lifetime — not an input, because it never changes during operation, and not a constant, because each instance may have a different one:

FUNCTION_BLOCK BoundedCounter
PARAMETER
    Limit : INT;
    REQUIRE Limit > 0;
END_PARAMETER
VAR_INPUT
    Reset : BOOL;
    Count : BOOL;
END_VAR
VAR_OUTPUT
    Value : INT;
END_VAR
IMPLEMENTATION
    Value:
        SET 0         WHEN Reset          PRIO 30;
        HOLD          WHEN Value >= Limit PRIO 20;
        SET Value + 1 WHEN Count          PRIO 10;
        HOLD OTHERWISE;

    INVARIANT Value >= 0;
    INVARIANT Value <= Limit;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Compilation succeeded: BoundedCounter
  2 output properties verified

Read that verdict carefully, because it is stronger than it looks. The proof is not about a counter that stops at ten, nor about one particular Limit. It holds for every Limit the REQUIRE admits — one proof, every machine in the fleet.

The REQUIRE is not decoration

Delete it and the same block no longer verifies:

verification failed:
  [invariant-init] invariant does not hold in the power-up state,
  before the first scan has run (every output and local at its default):
  (Value <= Limit)
      counterexample: Count=0, Limit=-1, Reset=0, Value=0

Without a constraint, Limit could be −1. Value starts at 0, and 0 is not ≤ −1, so the invariant fails before the machine has run a single scan. The solver did not guess this case; it searched every configuration you allowed and reported the one that breaks.

That is the working relationship: REQUIRE narrows the configurations you promise to build, and the proof covers all of them.

What a configuration constraint may mention

Only other parameters and literals. A REQUIRE naming an input is rejected:

verification failed:
  [parameter-require-nonconfig-ref] PARAMETER REQUIRE references 'Count'
  which is not a PARAMETER — only PARAMETER names and literals are allowed

The reason is timing. Configuration constraints are checked when the instance is set up, before any scan; an input has no value then. A property about inputs belongs in REQUIRE at the block level or in an INVARIANT, both of which live in scan time.

Three rules follow from what a parameter is, and each has a diagnostic behind it: a parameter never appears on the left of an assignment or SET (it is immutable), it has no previous value for PRE to read (it does not evolve), and its configuration constraint sees only configuration data.