LoLa — An Introduction by Example¶

A guided tour for students who already know a little about PLCs and Structured Text, but nothing about LoLa or formal verification. Read it top to bottom; every section builds on the previous one, and nothing is assumed that was not explained earlier.

0. Before we start: what problem does LoLa solve?¶

If you have programmed a PLC (programmable logic controller), you have probably written Structured Text (ST) — the IEC 61131-3 language that looks like Pascal. A PLC runs your program in a loop called the scan cycle: every few milliseconds it (1) reads all inputs, (2) runs your code once from top to bottom, (3) writes all outputs, and repeats forever. A function block (FB) is a reusable unit with inputs, outputs, and internal memory that survives from one scan to the next.

In ordinary ST you write the how — the exact sequence of assignments that computes the new outputs:

IF Stop THEN
    Motor := FALSE;
ELSIF Start THEN
    Motor := TRUE;
END_IF;

This works, but it has two well-known problems:

Order and precedence are implicit. Whether Stop or Start wins is decided by the order you happened to write the branches. Change the order and the behaviour changes — silently.
Correctness is only ever tested, never guaranteed. You can run a few cases and see that they work, but a PLC controls real machines; “it worked in the cases I tried” is not the same as “it can never do the wrong thing”.

LoLa takes an even harder line on one classic source of trouble: loops. From the point of view of language design, loops are the root of a remarkable amount of evil: hidden runtime cost, off-by-one errors, accidental non-termination, hard WCET questions, awkward aliasing through mutable indices, and proofs that suddenly have to discover the right loop invariant before they can say anything useful. You can easily argue that an absurd fraction of everyday programming pain starts exactly there.

So LoLa's plan is not to “support loops carefully”, but to avoid needing them in the first place. If repetition is allowed at all, it must be statically bounded and structurally visible to the compiler: as a fixed-size array, an aggregate over a known range, a sorting network, or another construct whose per-scan cost is known up front. This is not a missing feature. It is one of the language's main design decisions.

If you know declarative languages such as Prolog, this may sound familiar. In Prolog you also try to state the relation you want instead of spelling out a loop. For example, you do not write “iterate through the list and search”; you state rules such as “member(X, [X|_])” and “member(X, [_|T]) :- member(X, T)”. The engine then tries to satisfy the relation. That is powerful, but it comes with a notorious price: unbounded recursion and search. A relation may be perfectly elegant on paper and still diverge at runtime, revisit the same search space forever, or only terminate for some call patterns. In other words: declarative style alone does not buy you bounded execution.

That is why it helps to distinguish two separate axes:

Imperative vs. declarative. Imperative languages tell the machine which steps to execute in which order. Declarative languages state what relationship or result should hold, leaving more of the operational detail to the compiler, runtime or solver.
General vs. total. A general-purpose language admits computations that may fail to terminate. A total language admits only programs that are guaranteed to terminate (and usually to produce a result of the declared shape).

These axes are independent. A language can be:

imperative and general-purpose (ordinary C, Structured Text, Python),
declarative and general-purpose (Prolog is the standard example),
declarative and total (many proof-oriented languages and total functional cores),
or restricted/total in a domain-specific way.

LoLa deliberately sits in that last area. It is more declarative than ordinary PLC code, because you specify rules, priorities, invariants, assumptions and bounded aggregates rather than step-by-step control flow. But it is not “fully declarative” in the Modelica/Prolog sense where an open-ended solver or search engine may roam. LoLa is also not imperative in the usual “statement sequence with loops and mutable program counters” sense. The best description is:

LoLa is a declarative, synchronous, domain-specific, total control language.

“Total” here means: every accepted LoLa block has a statically proven finite per-scan execution. There is no unbounded loop, no open recursion, no search that may or may not bottom out. If the compiler cannot show the computation is bounded, it does not accept the program. That is the crucial difference from Prolog-style declarative languages: LoLa keeps the declarative flavour, but rejects the unbounded operational freedom that would destroy analyzability, WCET guarantees and complete verification.

This matters even more in the age of LLMs. A modern and surprisingly natural use of LoLa is exactly the neuro-symbolic pattern: let a probabilistic model propose a solution, and let the symbolic compiler and solver accept or reject it with no mercy. The LLM can be creative, fast, and occasionally wrong; LoLa is the mathematical doorman. If the verifier proves the stated invariants and contracts, the result is not “probably fine” but correct with respect to those statements. For industrial control, where a software error can damage equipment or endanger people, that is the only sane way to let an AI anywhere near executable logic.

Just as important, LoLa gives an LLM the kind of feedback it can actually use. A failed proof is not “your program seems bad”; it is a precise complaint with a counterexample, an unmet precondition, or a violated invariant. That is a far better repair signal than a vague test failure. In that sense LoLa is not merely a language, but a very sharp specification-and-correction loop.

But the risk does not disappear; it moves. There are really three different questions:

Did I implement it right?
Did I specify it right?
Did I specify everything that actually matters?

The first question is exactly where formal methods are strongest. The second is harder. The third is the real killer.

The standard toy example is sorting. “The output is sorted” still admits the absurd implementation “write zeros everywhere”. 0 0 0 0 0 is perfectly sorted. It is just not the result anyone wanted. That is why “sorted” without “is a permutation of the input” is an incomplete specification.

The same thing happens in automation. Suppose you write only:

INVARIANT
    Pressure < 10.0;

One perfectly valid “solution” is then:

Pump  := OFF;
Valve := OPEN;

forever. The pressure stays below 10 bar. The proof is correct. The plant is also useless. Safety alone did not capture the engineering intent.

That is why one sentence is worth stating explicitly:

Verification proves properties, never intentions.

Or more sharply:

Verification answers “Is the implementation consistent with the specification?” It deliberately does not answer “Is the specification what the engineer actually intended?”

This is the real requirements-engineering problem, and LLMs do not remove it. If anything, they make it more visible. An LLM may generate fifty candidate solutions. LoLa may reject forty-eight and accept two. That is already a huge win. But the two accepted solutions may still both be wrong — not because the code is broken, but because the specification left something important unsaid.

So LoLa does not eliminate engineering judgment; it changes where engineering judgment is required. The difficult question is no longer only “How do I implement this?” but “Have I specified everything that matters?” As synthesis becomes more automated, the engineer's centre of gravity shifts from writing algorithms to defining complete, correct and meaningful properties.

That shift is not merely a warning; it is also an opportunity. A good LLM should not only propose implementations. It should also criticise specifications:

“You required safety, but never stated that production should continue.”
“I see no liveness property.”
“The controller may legally keep the valve permanently closed.”
“You bounded the pressure, but never required eventual completion.”

That kind of criticism may turn out to be more valuable than code generation itself. In a mature LoLa workflow, the machine may increasingly propose the transitions while the engineer spends more effort on the invariants, contracts and missing properties. The hardest bugs in that world are no longer programming mistakes, but specification mistakes — and those cannot be proved away.

LoLa attacks both. In LoLa you do not write the sequence of assignments. You declare what each output is, you state explicitly which rule wins, and you write down the safety properties that must hold. Then a tool called an SMT solver (specifically Z3 — think of it as an automated mathematician) either proves your properties hold for every possible input and every possible timing, or it rejects your program and hands you a concrete counterexample.

Only after the proof succeeds does LoLa generate code — and it can generate the ST you already know, or Rust. Crucially, both are generated from the same verified model, so they cannot disagree with each other or with the proof.

Throughout this guide, whenever you see a note like this:

✅ Proven: “no two motors can run at once.”

…it means the compiler actually ran a mathematical proof over all inputs — not a test over a few samples. That is the whole point of LoLa. Let us see it.

1. Your first block: an RS latch¶

A latch (or bistable) remembers a bit. Press set, it turns on and stays on; press reset, it turns off and stays off. It is the “hello world” of PLC logic. Here it is in LoLa, fully commented (examples/rs_latch.lola):

FUNCTION_BLOCK RS              // declare a reusable function block named RS
VAR_INPUT                      // its inputs (read at the start of each scan)
    R : BOOL;                  //   R = reset button
    S : BOOL;                  //   S = set button
END_VAR
VAR_OUTPUT                     // its outputs (written at the end of each scan)
    Q : BOOL;                  //   Q = the stored bit
END_VAR
IMPLEMENTATION
    Q:                         // define the output Q with a list of prioritised rules
        OFF WHEN R PRIO 0;     //   if R is pressed, force Q off ... priority 0
        ON  WHEN S PRIO 1;     //   if S is pressed, force Q on  ... priority 1 (higher!)
        HOLD OTHERWISE;        //   otherwise keep Q's previous value
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Design choice, not a law of nature. If R and S are both 1 in the same scan, this block is set-dominant because we gave S the higher priority. A different priority assignment would give a different latch. LoLa does not guess which RS behaviour you “meant” — you state it explicitly.

Read the Q: block as a set of competing rules, not as a sequence of steps. Each rule says “under this condition, the output should become this value, and my importance is this number.” The vocabulary:

Keyword	Meaning
`ON` / `OFF`	make the output `TRUE` / `FALSE` (BOOL outputs only)
`SET expr`	assign the value of an expression (any type)
`HOLD`	keep the output's previous value (its memory)
`WHEN guard`	this rule is active only when `guard` is true
`PRIO n`	this rule's priority; bigger number = more important
`OTHERWISE`	the fallback rule; no condition, no priority

Here is the single most important idea in LoLa. Among all the rules whose guard is currently true, the one with the highest PRIO decides the output. The order in which you wrote the rules is irrelevant. Above, S has priority 1 and R has priority 0, so if you press both at once, set wins — this is a “set-dominant” latch. If you wanted reset to win, you would swap the priority numbers, not move the lines around. There is no single “canonical” answer here: IEC 61131-3 itself ships both an SR (set-dominant) and an RS (reset-dominant) standard block. Which one you want is a design decision, and in LoLa you make it by choosing the priorities — nothing else.

What the compiler makes of it¶

Let us compile it and ask for Structured Text:

$ python -m lola examples/rs_latch.lola --target st

FUNCTION_BLOCK RS
VAR_INPUT
    R : BOOL;
    S : BOOL;
END_VAR
VAR_OUTPUT
    Q : BOOL;
END_VAR
VAR
    _Q_next : BOOL;
END_VAR
    _Q_next := (S OR (NOT R AND Q));   (* <-- the three rules, collapsed into ONE formula *)
    Q := _Q_next;
END_FUNCTION_BLOCK

Look closely at that one line. Your three prioritised rules — set, reset, hold — were compiled into a single boolean formula:

Q_next  =  S  OR  (NOT R  AND  Q)

In words: Q becomes true if S is pressed (set wins), or else if R is not pressed and Q was already true (hold). This is exactly the classic set-dominant latch equation you would find in a textbook — but you did not write it. You wrote the intent (three rules and their priorities), and Z3 derived the equation, folding the priorities together in the correct order. That derived formula is the meaning of your block, and it is what every backend prints.

Why the extra variable _Q_next? The compiler computes the new value into a temporary first (_Q_next), and only then assigns it to Q. Section 2 explains why this staging matters.

2. How a block runs: one scan, all-at-once¶

A subtle but important point: in a real PLC scan, all of a block's outputs are conceptually updated simultaneously, using the values they had at the start of the scan. If one output's formula reads another output, it must read the old value, not a half-updated new one.

LoLa guarantees this, and you can see the mechanism in the generated ST: every new value is computed into a _..._next temporary first, and only after all of them are computed are they committed. The rising-edge detector in the next section shows this clearly. Keep the pattern in mind:

1. compute  _a_next, _b_next, ...   (all from start-of-scan values)
2. commit   a := _a_next;  b := _b_next;  ...

This is not something you write — it is how LoLa renders “update everything at once” into a language (ST) that only has step-by-step assignment.

3. Two kinds of memory: registers and derived values¶

Every output or internal variable is defined in one of two ways, and the difference is exactly when a reference reads its value. This trips up beginners, so read carefully.

A register is defined by rules (like Q: above). It is stored: it has memory that survives across scans. Inside a register's rules, a reference to another register means that register's value at the start of the scan — its “pre-value”, the old value. This is what you need for edge detection: to detect a change, you must compare against the previous value.
A derived value is defined with the := operator (name := expression;). It is combinational: it is recomputed every scan and not stored. Inside a derived definition, a reference to a register means its freshly computed new value — no one-scan delay.

Beginners usually need one compact picture:

Where you read a register	What you get
inside a rule block (`Q:` / `M:` / ...)	the old value from the start of the scan
inside a derived definition (`x := ...`)	the new value just computed for this scan

If you remember only one sentence from this section, remember this: rules read old state; := reads freshly computed state.

A rising-edge detector (R_TRIG, examples/iec/r_trig.lola) outputs a one-scan pulse each time its input goes from 0 to 1. It must remember the previous input:

FUNCTION_BLOCK R_TRIG
VAR_INPUT
    CLK : BOOL;                    // the signal we watch for a rising edge
END_VAR
VAR_OUTPUT
    Q : BOOL;                      // Q = 1 for exactly one scan on a 0->1 edge
END_VAR
VAR
    M : BOOL;                      // hidden internal memory: the PREVIOUS CLK
END_VAR
IMPLEMENTATION
    Q:                             // Q is a REGISTER, so M below is read as its PRE-value
        SET CLK AND NOT M OTHERWISE;   // edge = CLK is high now AND was low last scan
    M:
        SET CLK OTHERWISE;         // remember this scan's CLK for the next scan
END_IMPLEMENTATION
END_FUNCTION_BLOCK

VAR ... END_VAR declares hidden internal state — M here — that is not part of the public interface. The generated ST makes the pre-value and the all-at-once update visible:

    _Q_next := (CLK AND NOT M);    (* uses M = the OLD previous-CLK *)
    _M_next := CLK;                (* next scan's "previous CLK" *)
    Q := _Q_next;                  (* only now do we commit the new values ... *)
    M := _M_next;                  (* ... so _Q_next above saw the OLD M, not CLK *)

If both assignments happened immediately in order, M would be overwritten before Q read it and the edge detection would break. The _next staging is precisely what prevents that. This is the reading-time rule made concrete.

Rule of thumb. Need the previous value (edges, latches, counters comparing to a limit)? Use a register (rules). Need a value computed fresh this scan from other results (a plain combinational output)? Use :=.

4. Priorities in depth, and the errors that keep them honest¶

Because priority is written down explicitly, the compiler can check two things a human reviewer usually misses.

(a) No silent tie-breaks. If two rules with the same priority could be active at the same time but demand different results, that is not a coin toss — it is an ambiguous-priority error, reported with a counterexample. You must give them different priorities or make their conditions mutually exclusive. (Two rules with equal priority that agree — e.g. several OFF rules — are fine.)

(b) No dead code. A rule that is always beaten by a higher-priority rule can never affect the output. LoLa reports it as an unreachable-rule warning so you can delete it or fix its condition.

A bounded up-counter (examples/counter.lola) uses a realistic three-level priority stack:

FUNCTION_BLOCK Counter
VAR_INPUT
    Reset : BOOL;                  // reset to zero
    Count : BOOL;                  // count-up pulse
END_VAR
VAR_OUTPUT
    Value : INT;                   // the current count
END_VAR
IMPLEMENTATION
    Value:
        SET 0         WHEN Reset       PRIO 30;   // reset beats everything
        HOLD          WHEN Value >= 10 PRIO 20;   // at the limit: freeze (saturate)
        SET Value + 1 WHEN Count       PRIO 10;   // otherwise, if counting, add one
        HOLD OTHERWISE;                           // idle: keep the value

    INVARIANT                       // a property we DEMAND the compiler prove:
        Value >= 0;                 //   the count is never negative
    INVARIANT
        Value <= 10;                //   and never exceeds 10
END_IMPLEMENTATION
END_FUNCTION_BLOCK

INT is a 16-bit signed integer with the same wrap-around behaviour as real PLC hardware (add 1 to 32767 and you get −32768). LoLa models this faithfully, so its proofs are about what the hardware actually does, not an idealised infinite integer. We will come back to the two INVARIANT lines in the next section.

The generated ST folds the four-rule priority stack into nested SEL calls (SEL(cond, a, b) is the IEC selector: it returns b if cond is true, else a — a two-way multiplexer):

    (* proven invariant: (Value >= 0) *)
    (* proven invariant: (Value <= 10) *)
    _Value_next := SEL(Reset, SEL(((10 <= Value) OR NOT Count), (1 + Value), Value), 0);
    Value := _Value_next;

Unfold it from the outside in and you recover your priorities exactly: if Reset, result is 0; else if (Value >= 10 or not counting) keep Value; else Value + 1. The two comment lines are the compiler telling you which properties it proved before emitting this code.

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

This is where LoLa 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, LoLa 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.”

LoLa 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 LoLa 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, LoLa 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. LoLa 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.lola):

    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.

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.

7. Time, made symbolic¶

Real machines need delays: “shut down only if the fault persists for 2 seconds.” LoLa has two declarative time primitives:

HELD(cond, PT) — a BOOL that is true once cond has been continuously true for at least the duration PT.
ELAPSED(cond, PT) — the matching TIME value: how long cond has been continuously true, capped at PT (this is the IEC TON.ET output).

Together they are an on-delay timer. Here is a full IEC TON (examples/iec/ton.lola):

FUNCTION_BLOCK TON
VAR_INPUT
    IN : BOOL;                     // start condition
    PT : TIME;                     // preset time (a runtime value, not a constant!)
END_VAR
VAR_OUTPUT
    Q  : BOOL;                     // true PT after IN went true and stayed true
    ET : TIME;                     // elapsed time so far, capped at PT
END_VAR
IMPLEMENTATION
    Q  := HELD(IN, PT);            // "IN has held for >= PT"
    ET := ELAPSED(IN, PT);         // "how long IN has held, up to PT"
END_IMPLEMENTATION
END_FUNCTION_BLOCK

The generated ST does not re-implement timing arithmetic — it maps straight onto a native IEC TON instance, the same standard block you already use:

VAR
    _held_in_0 : TON;              (* a real IEC TON, instantiated for us *)
END_VAR
    _held_in_0(IN := IN, PT := PT);
    Q := _held_in_0.Q;
    ET := _held_in_0.ET;

So on the PLC there is no elapsed-time arithmetic leaking into your logic; time stays inside a proper timer block.

Why this lets us prove timing-independent properties¶

Here is the beautiful part. Inside the verifier, time is symbolic — the proof does not pick a specific delay, it reasons about all delays at once. Consider a pressure guard that warns immediately but shuts down only after a sustained fault (examples/pressure.lola):

    Warn:
        ON WHEN Overpressure PRIO 1;       // warn the instant pressure is high
        OFF OTHERWISE;

    Shutdown:
        ON WHEN HELD(Overpressure, 2s) PRIO 1;   // shut down only after 2 s of it
        OFF OTHERWISE;

    INVARIANT
        NOT Shutdown OR Warn;              // "Shutdown implies Warn"

NOT Shutdown OR Warn is the logician's way of writing “if Shutdown then Warn”.

✅ Proven for every possible timing: whenever the block shuts down, it is also warning. It does not matter whether the 2-second timer has elapsed or not, whether the scan is fast or slow — a shutdown can only happen while overpressure is present, and overpressure always raises the warning in the same scan.

The generated ST again uses a native TON and shows the 2s preset as the IEC literal T#2000ms:

    (* proven invariant: (NOT Shutdown OR Warn) *)
    _held_overpressure_0(IN := Overpressure, PT := T#2000ms);
    _Warn_next := Overpressure;
    _Shutdown_next := _held_overpressure_0.Q;
    Warn := _Warn_next;
    Shutdown := _Shutdown_next;

8. Continuous values: `REAL`, `DT`, `CLAMP`¶

For control (levels, flows, temperatures) you need continuous quantities. REAL is LoLa's continuous number. Two primitives make control code expressible:

DT — the elapsed time of the current scan, in seconds, taken from the runtime clock. You never wire it; it is always available. In proofs it is symbolic and non-negative, so results hold for any scan rate.
CLAMP(x, lo, hi) — saturation: return x, but never below lo or above hi.

A clamped integrator accumulates its input over time and is limited to a band (examples/analog/integrator.lola):

FUNCTION_BLOCK Integrator
VAR_INPUT
    x     : MATHREAL;                  // the signal to integrate (e.g. a rate)
    Limit : MATHREAL;                  // the saturation band, supplied by the caller
END_VAR
VAR_OUTPUT
    y : MATHREAL;                      // the accumulated integral
END_VAR
IMPLEMENTATION
    y:
        // new y = old y + x*dt, but never outside [-Limit, +Limit]
        SET CLAMP(y + x * DT, -Limit, Limit) OTHERWISE;

    ASSUME
        Limit >= 0.0;              // a precondition the caller must satisfy (see below)

    INVARIANT
        y <= Limit;                // the integral never winds up past the band ...
    INVARIANT
        y >= -Limit;               // ... in either direction
END_IMPLEMENTATION
END_FUNCTION_BLOCK

y + x * DT is the discrete integration step: add “rate × elapsed time” to the running total. Wrapping it in CLAMP(..., -Limit, Limit) implements anti-windup — a standard control technique that stops an integrator from accumulating without bound when it saturates.

✅ Proven: −Limit <= y <= Limit for any input signal and any scan timing. The anti-windup is not hoped-for behaviour; it is a theorem about the block.

A REAL in LoLa is mathematical ℝ — not a machine float or a fixed-point integer. Proofs hold over the real numbers exactly. This is also why DT is symbolic in the proof: the solver reasons over all possible ℝ-valued scan times at once, so the anti-windup bound holds regardless of how fast or slow the scan runs.

To emit runnable code for a block with REAL variables you must first declare a Representation Boundary — the choice of machine arithmetic. The simplest way is the --profile float64 flag, which lowers REAL to IEEE 754 binary64 (LREAL in ST, f64 in Rust). Without a Representation Boundary the compiler verifies the programme mathematically but refuses to generate code, because the gap between ℝ and a finite machine type is a separate correctness obligation (see how-to/real-numerical-assurance.md). ST and Rust are then generated from the same proven ℝ model, so they cannot diverge from each other or from the proof. For the complete REAL semantics and the numerical assurance chain, see Language Reference §13.

9. Partial operations: division and `IF/THEN/ELSE`¶

Division has a trap: a / b is undefined when b = 0. In most languages that is a runtime crash waiting to happen. LoLa treats “the divisor is non-zero” as a proof obligation, just like an invariant. Writing a bare division that might divide by zero is a compile error:

[division-by-zero] cannot prove the divisor is non-zero: b may be 0 where
a / b is evaluated. Guard it, e.g. IF b <> 0.0 THEN ... ELSE ...

The language gives you the tool to discharge the obligation: IF cond THEN a ELSE b is a conditional expression (it produces a value), and the proof is path-sensitive — inside the THEN branch the compiler knows cond is true. So a discrete-time differentiator guards its division and compiles (examples/analog/differentiator.lola):

    // rate of change = (x - x_prev) / dt, but only when dt is non-zero
    d: SET IF DT <> 0.0 THEN (x - x_prev) / DT ELSE 0.0 OTHERWISE;

Because you handled the DT = 0 case explicitly (returning 0.0), the compiler is satisfied that the division is only ever reached when DT <> 0. And the generated code contains exactly that guard — nothing is swept under the rug, and there is no possibility of a divide-by-zero fault on the machine.

The pattern: LoLa never silently accepts an operation that can fail. It makes you prove it is safe, and gives you the language (IF, guards, priorities) to do so.

10. Environment premises: `ASSUME`¶

Look back at the integrator's line ASSUME Limit >= 0.0;. What is it?

An INVARIANT is something the block must prove. An ASSUME is the opposite: something the block's caller must guarantee. This is called an assume-guarantee contract, and it is what lets a block be reusable with parameters instead of magic numbers.

For students, the shortest way to keep the two apart is:

INVARIANT = my block guarantees this
ASSUME = my block only promises that if the caller gives me this

Why does the integrator need it? Its anti-windup proof only works if the band is sensible. If Limit could be negative, then at power-on y = 0 would already be outside [-Limit, Limit] (an empty interval), and CLAMP's bounds would be crossed. Rather than hard-code Limit = 10, the block states its honest precondition — “I work for any non-negative Limit” — and the compiler then proves the anti-windup for every valid Limit at once.

Rules that keep ASSUME sound:

It may mention inputs only. Assuming something about the block's internal state would be cheating (the environment does not control internal state).
It may not mention DT either — the compiler rejects it. You must not “assume away” properties of the runtime clock.
The assumptions must be satisfiable together. Contradictory assumptions (from which anything follows) are a contradictory-assume error, so you cannot accidentally prove everything by assuming a falsehood.

So if you are unsure which one to write, ask:

“Can the block itself enforce this?”

If yes, it belongs in the rules and may then be stated again as an INVARIANT. If no — if it is really a requirement on the outside world — it is an ASSUME.

11. Building bigger blocks: composition¶

You build large systems by wiring small blocks together. VAR inst : OtherBlock; creates an instance; inst(In := expr, ...) wires its inputs; inst.Out reads its outputs. A start/stop station built from the reset-dominant RS latch (examples/composition/StartStop.lola, reusing RS.lola):

FUNCTION_BLOCK StartStop
VAR_INPUT
    Start : BOOL;
    Stop  : BOOL;
END_VAR
VAR_OUTPUT
    Running : BOOL;
END_VAR
VAR
    latch : RS;                    // an instance of the RS block from RS.lola
END_VAR
IMPLEMENTATION
    latch(S := Start, R1 := Stop); // wire Start -> latch.S, Stop -> latch.R1
    Running := latch.Q1;           // expose the latch's output
END_IMPLEMENTATION
END_FUNCTION_BLOCK

At compile time LoLa flattens the instance in: the sub-block's internals become hidden locals of the parent, its inputs are replaced by the wired expressions, and latch.Q1 reads its freshly computed output. The generated ST shows the flattened result — the RS latch's equation, now with its state renamed latch__Q1:

VAR
    latch__Q1 : BOOL;              (* the sub-latch's memory, now a hidden local *)
    _latch__Q1_next : BOOL;
END_VAR
    _latch__Q1_next := (NOT Stop AND (Start OR latch__Q1));
    Running := (NOT Stop AND (Start OR latch__Q1));
    latch__Q1 := _latch__Q1_next;

Because composition is just flattening, everything else — proofs, backends — works unchanged. And the contracts compose:

A sub-block keeps its own INVARIANTs: instantiating a child never drops its safety proofs.
A parent may write invariants about a sub-instance's outputs (inst.Out).
A child's ASSUME is honoured based on how it is wired, and the compiler splits it accordingly. If it resolves to the parent's own inputs, it bubbles up as a premise on the parent (the parent's caller must honour it). If the parent instead supplies it with internal logic (a local, register or constant), the parent must discharge it — the premise becomes a proof obligation the parent proves on the spot (wiring it to D := TRUE compiles; wiring it to FALSE fails, as it must). Both directions work today. The split is syntactic (by which names the wired premise references), so a premise that mixes free inputs with internal state is not yet handled in full generality — the roadmap tracks the general “prove what you can, assume the residual” form.

11b. Template blocks — reusing logic at different sizes¶

Composition lets you wire a fixed-size RS latch into anything that needs one. But what if you want a dot-product block that works for vectors of different lengths? Without something more, you would write Vec3, Vec4, Vec5 as separate files — identical logic, different size. That is the monomorphism trap.

Type template parameters solve this. Put the size in angle brackets after the block name, then use it like an ordinary integer everywhere inside:

FUNCTION_BLOCK Vec<N: UINT>
VAR_INPUT
    a : ARRAY[0..N-1] OF LREAL;
    b : ARRAY[0..N-1] OF LREAL;
END_VAR
VAR_OUTPUT
    dot : LREAL;
END_VAR
IMPLEMENTATION
    dot := SUM(k IN 0..N-1 : a[k] * b[k]);
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Save this as Vec.lola. Now a parent block can wire in Vec<3> and Vec<4> as if they were ordinary sub-blocks:

FUNCTION_BLOCK TwoVecs
VAR_INPUT
    p3 : ARRAY[0..2] OF LREAL;  q3 : ARRAY[0..2] OF LREAL;
    p4 : ARRAY[0..3] OF LREAL;  q4 : ARRAY[0..3] OF LREAL;
END_VAR
VAR_OUTPUT
    d3 : LREAL;
    d4 : LREAL;
END_VAR
VAR
    v3 : Vec<3>;
    v4 : Vec<4>;
END_VAR
WIRING
    v3(a := p3, b := q3);
    v4(a := p4, b := q4);
    d3 := v3.dot;
    d4 := v4.dot;
END_WIRING
END_FUNCTION_BLOCK

The compiler monomorphizes each instantiation: it substitutes N = 3 into the full AST of Vec, resolves ARRAY[0..N-1] to ARRAY[0..2] and SUM(k IN 0..N-1 : …) to SUM(k IN 0..2 : …), names the result Vec<3>, and then compiles it as an ordinary concrete FB. Vec<3> and Vec<4> are independent concrete types: separate proofs, separate generated arrays, separate hidden locals after flattening.

Nothing about this sidesteps the rules you already know. The Bounded-Cycle Theorem still holds: every bound is a compile-time integer literal after substitution, so the compiler knows the size of every array and the range of every aggregate before it starts verifying anything.

Two type parameters work the same way. A 2×3 matrix-vector multiply:

FUNCTION_BLOCK MatVec<M: UINT, K: UINT>
VAR_INPUT
    a : ARRAY[0..M*K-1] OF LREAL;   (* row-major; a[i*K+k] is row i, col k *)
    x : ARRAY[0..K-1]   OF LREAL;
END_VAR
VAR_OUTPUT
    y : ARRAY[0..M-1] OF LREAL;
END_VAR
IMPLEMENTATION
    y := ARRAY(i IN 0..M-1 : SUM(k IN 0..K-1 : a[i*K+k] * x[k]));
END_IMPLEMENTATION
END_FUNCTION_BLOCK

VAR
    mv : MatVec<2, 3>;   (* M=2 rows, K=3 columns *)
END_VAR
WIRING
    mv(a := A, x := x);
    y := mv.y;
END_WIRING

For more detail — multiple parameters, wiring patterns, pitfalls — see the How-To: Use Template Blocks and the Concept: Template Blocks.

12. Physical units — catching “apples plus oranges” at compile time¶

A famous class of bugs is mixing incompatible physical quantities (adding a pressure to a temperature, or forgetting to multiply a flow by a time). LoLa can catch these at compile time if you annotate your REALs with units:

VAR_INPUT
    flow : REAL<m3/h>;             // volumetric flow, cubic metres per hour
    cap  : REAL<m3>;               // tank capacity, cubic metres
END_VAR
VAR_OUTPUT
    volume : REAL<m3>;             // accumulated volume, cubic metres
END_VAR
IMPLEMENTATION
    volume:
        SET CLAMP(volume + flow * DT, 0.0, cap) OTHERWISE;
    ...

(Full example: examples/analog/flow_totalizer.lola.) The compiler works out the dimension of every expression and checks consistency:

+, − and comparisons require compatible dimensions (a bare number adapts to either side).
* and / combine dimensions (multiply/divide the exponents).
DT has the dimension of time.

The key insight it proves here: flow (m³/h) times DT (s) has dimension m³ — a volume — because the two time dimensions cancel. So it may be added to volume. Try to add a raw flow to a volume and you get:

[dimension-mismatch] cannot apply '+' to incompatible dimensions m^3 and m^3/s

Units are a compile-time contract only: they are checked and then erased, so the generated ST/Rust is byte-for-byte identical whether or not you annotated them. They cost nothing at runtime and catch a whole category of engineering mistakes before the code ever runs.

13. Arrays and bounded repetition¶

Every signal so far has been a single value. Real controllers watch banks of them: eight temperature sensors, sixty-four samples, four PID channels. You could of course write out T1, T2, … T8 and eight near-identical rules — and that is exactly what the early hand-written examples looked like. It was miserable, and it hid the intent. LoLa gives you arrays and aggregates so you state the result over the whole array at once:

Before the first example, here is the minimal vocabulary:

Syntax	Meaning
`ARRAY[lo..hi] OF T`	an array type with fixed compile-time bounds
`a[i]`	read element `i` of array `a`
`ARRAY(i IN lo..hi : e)`	build a new array by computing each element
`OP(i IN lo..hi : e)`	aggregate over a fixed index range (`ALL`, `ANY`, `COUNT`, `SUM`, `MIN`, `MAX`)

The important point is that lo..hi is not runtime data. It is part of the source and therefore known at compile time. That is why LoLa can admit arrays while still forbidding open-ended loops.

VAR_INPUT
    T   : ARRAY[1..8] OF REAL<degC>;   // the 8 sensor readings
    Lim : REAL<degC>;                  // the alarm threshold
END_VAR
VAR_OUTPUT
    all_ok  : BOOL;   any_hot : BOOL;   n_alarm : INT;
    hottest : REAL<degC>;              average : REAL<degC>;
END_VAR
IMPLEMENTATION
    all_ok  := ALL  (i IN 1..8 : T[i] <= Lim);
    any_hot := ANY  (i IN 1..8 : T[i] >  Lim);
    n_alarm := COUNT(i IN 1..8 : T[i] >  Lim);
    hottest := MAX  (i IN 1..8 : T[i]);
    average := SUM  (i IN 1..8 : T[i]) / 8.0;
    ...

(Full example: examples/arrays/sensor_monitor.lola.)

An aggregate has the shape OP(i IN lo..hi : body): it folds body, evaluated for each index in the range, with OP. The vocabulary:

Aggregate	Result	Reads like
`ALL(i IN … : p)`	`BOOL`	every element satisfies `p`
`ANY` / `EXISTS`	`BOOL`	at least one satisfies `p`
`COUNT(i IN … : p)`	`INT`	how many satisfy `p`
`SUM(i IN … : e)`	number	the total
`MIN` / `MAX`	number	the extreme value

The crucial constraint — and it is the whole reason arrays are allowed at all — is that the index range is a compile-time constant set. ARRAY[1..8] has exactly eight elements, known now. That is the Bounded-Cycle principle: every valid program has a statically proven finite per-scan execution. An aggregate over a static range keeps that promise — the work per scan is known up front, never a loop the PLC has to run an unknown number of times.

What the compiler makes of it¶

_r0 := TRUE;
FOR i := 1 TO 8 DO
    _r0 := _r0 AND (T[i] <= Lim);
END_FOR;
all_ok := _r0;

_r2 := 0;
FOR i := 1 TO 8 DO
    _r2 := _r2 + SEL((T[i] > Lim), 0, 1);      (* COUNT: a sum of 0/1 *)
END_FOR;
n_alarm := _r2;

A plain accumulator loop with a statically known trip count — the shape a PLC programmer would have written by hand, except you did not have to.

Two views of the same aggregate. Here is a distinction worth holding on to. What you just saw is the emitted code, and it is a loop. What the prover sees is something else: ALL/ANY become a quantifier (∀i/∃i), SUM/COUNT a recurrence, MIN/MAX a value pinned by two axioms (it bounds every element, and one element attains it). The proof therefore does not grow with the range: ALL over 256 elements is under 20 formula nodes rather than 256 terms.

Why care? Because if the proof secretly expanded the aggregate while the emitted code showed a tidy loop, then the day a large array made verification slow, nothing in the visible artifact would point at the cause. Keeping both views structured keeps the cost attributable.

Because the prover reasons about the aggregate as a whole rather than element by element, the operating envelope — itself an aggregate — proves the block's guarantees directly:

    ASSUME ALL(i IN 1..8 : T[i] <= 200.0);
    ASSUME ALL(i IN 1..8 : T[i] >= -50.0);
    INVARIANT hottest <= 200.0;   INVARIANT average <= 200.0;

✅ Proven: hottest and average stay within [-50, 200] — a MAX and a mean never escape the readings. The same magnitude bounds certify that the SUM behind average cannot overflow the fixed-point type on either target.

14. Indexing as a partial operation¶

In §9 you met the idea that some operations are partial: division is only defined when the divisor is non-zero, so it carries a proof obligation. A dynamic array index — a[k] where k is a runtime value, not a constant — is the very same idea. Channel[sel] is only defined when sel is in bounds, so it carries the obligation array-index-out-of-bounds, discharged exactly like division-by-zero:

FUNCTION_BLOCK Selector
VAR_INPUT
    Channel : ARRAY[0..7] OF REAL;
    sel     : INT;
END_VAR
VAR_OUTPUT selected : MATHREAL; END_VAR
IMPLEMENTATION
    selected := Channel[sel];
    ASSUME sel >= 0;
    ASSUME sel <= 7;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

(Full example: examples/arrays/selector.lola.)

Drop either ASSUME and compilation fails — not with a warning, with a concrete counterexample:

[array-index-out-of-bounds] Channel[sel] can be reached with sel = -32768

Just like division, the bound may instead be proven path-sensitively from an enclosing IF 0 <= sel AND sel <= 7 THEN …. A constant index (Channel[3]) is free: the compiler checks it against the declared range at compile time, no proof needed.

What the compiler makes of it¶

Once the index is proven in range, the backends index their native arrays directly — which is sound precisely because of the proof:

selected := Channel[sel];      (* native ST array access, proven in-range *)

In the Z3 model the same read is a loop-free nested ITE over the eight element constants, so the model stays quantifier-free and decidable.

Rule of thumb. A constant index is free. A computed index costs you a bound — the exact same bargain as /. If you cannot prove the index is in range, LoLa will not let the block compile, because on the plant it would read past the array.

15. Building arrays: the `MAP`¶

Arrays have been inputs so far. You can also produce one as an output, element by element, with an ARRAY(…) constructor — a MAP over a range:

VAR_OUTPUT
    Bar    : ARRAY[0..7] OF REAL<bar>;  // conditioned pressures (a MAP result)
    worst  : REAL<bar>;   n_high : INT;
END_VAR
IMPLEMENTATION
    Bar    := ARRAY(i IN 0..7 : Raw[i] * gain);   // MAP: scale every channel
    worst  := MAX  (i IN 0..7 : Bar[i]);          // REDUCE over the built array
    n_high := COUNT(i IN 0..7 : Bar[i] > 10.0);
    ...

(Full example: examples/arrays/conditioning.lola.)

Bar is a first-class array on the block's interface, not a bag of scalars: the ST backend emits ARRAY[0..7] OF LINT, the Rust backend [i64; 8]. Each element is a derived value, and you can immediately aggregate over the array you just built — worst and n_high fold Bar, so a MAP feeds a REDUCE.

The constructor itself is worth reading slowly:

ARRAY(i IN 0..7 : Raw[i] * gain)

i is a local index variable that exists only inside this expression.
0..7 is the fixed compile-time range over which the array is built.
Raw[i] * gain is the value of the resulting element at position i.

So ARRAY(...) is not a mutable fill loop. It is an array-valued expression: “build me the whole array whose i-th element is ...”.

What the compiler makes of it¶

Bar[0] := ((Raw[0] * gain) / 1000);
Bar[1] := ((Raw[1] * gain) / 1000);
…                                       (* one derived assignment per element *)
worst  := SEL(…);                        (* the compare-swap MAX chain over Bar *)

Units flow elementwise: Raw is dimensionless counts, gain is bar-per-count, so each Bar[i] is checked to be bar. The magnitude ASSUMEs keep every fixed-point product in range, so the whole block is provably overflow-safe on both targets.

16. Three ways to say “sorted”¶

Sorting is the textbook “I obviously need a loop” task — so it is the sharpest test of a language that has none. LoLa gives you three ways to obtain a sorted array, all loop-free, all statically finite, and each more declarative than a hand-written bubble sort. (Forcing bubble was the wrong instinct in the first place: in Prolog you would never encode a particular sorting algorithm to say what “sorted” means.)

16.1 State the result — `SORT`¶

The least you can say is: s is a, sorted.

VAR_OUTPUT s : ARRAY[0..4] OF REAL; END_VAR   // a, sorted non-decreasing
IMPLEMENTATION
    s := SORT(a);
END_IMPLEMENTATION

(Full example: examples/arrays/sort5.lola.)

As a language element, SORT means exactly this:

its argument must be a fixed-size array;
its result has the same element type and shape;
it specifies the sorted version of that array, not a particular algorithm;
the current implementation is intentionally bounded in size, because the proof cost grows with the network.

The compiler realises SORT as a compare-swap sorting network — which network, and how it is later optimised, is the compiler's concern, not the source's. Two guarantees come for free:

permutation, by construction — every network step is a compare-swap (the min/max of a pair), which can only rearrange values;
sortedness, proven — Z3 auto-adds and discharges s[0] <= s[1] <= …. If the network were wrong, compilation would fail with a counterexample.

✅ Proven: s[0] <= s[1], s[1] <= s[2], s[2] <= s[3], s[3] <= s[4] — the sortedness invariants, auto-generated and discharged over the realised network.

Because the sortedness proof is the expensive part (not the code — the shared network is emitted compactly via memoised DAG walks and backend CSE), SORT is capped at 8 elements (~3 s to prove).

16.2 Constrain the result — `RULE`¶

Stronger still: give sorted no := definition at all, and pin it down purely by stating what it must be.

VAR_OUTPUT sorted : ARRAY[0..3] OF INT; END_VAR   // defined only by the RULEs
IMPLEMENTATION
    RULE permutation(xs, sorted);
    RULE ALL(i IN 0..2 : sorted[i] <= sorted[i + 1]);
END_IMPLEMENTATION

(Full example: examples/arrays/decl_sort.lola.)

This is where students most often need a hard conceptual separation:

:= says how a value is computed.
INVARIANT says what must always be true of code you already wrote.
RULE says what value is allowed, even if you did not write the computation.

So RULE is not a “stronger invariant”. It plays a different role in the language: it participates in defining the solution.

This is the contract/implementation split made into language. permutation(xs, sorted) says sorted is a rearrangement of xs; the compiler realises it as a compare-swap network, so the permutation holds by construction. The ALL(…) RULE says sorted is ordered; that is proven on the realised network — and it is what actually pins sorted to the one sorted order. The RULEs are the what, the network is a how the compiler chose, and Z3 proves the how meets the what. An unsatisfiable RULE (say, the opposite order) is a compile error.

✅ Proven: sorted[0] <= sorted[1] <= sorted[2] <= sorted[3] — discharged against the network the compiler synthesised for the permutation RULE. No runtime solver runs; everything is compiled and proven ahead of time.

Recall §5: an INVARIANT is a property proven about code you wrote. A RULE turns that around — you write only the property, and the compiler finds code that satisfies it and proves it does. That is the shift from verification to synthesis.

16.3 Define the computation — a bounded recursive `FUNCTION`¶

Sometimes you do want to spell out the algorithm. LoLa lets you — with a FUNCTION and bounded recursion — and still forbids the unbounded loop:

Start with the simplest mental model. A function has the shape

FUNCTION name(arg1 : T1, arg2 : T2, ...) -> R
    expression
END_FUNCTION

and means:

it is stateless: a function has no VAR, no hidden memory, no scan-to-scan state;
its body is an expression, not a statement list;
calling it just means substitute, inline, simplify at compile time;
recursion is allowed only when the compiler can prove it terminates on a static decreasing measure.

Before the sorting example, a tiny non-recursive one:

FUNCTION clamp01(x : REAL) -> REAL
    IF x < 0.0 THEN 0.0 ELSE IF x > 1.0 THEN 1.0 ELSE x
END_FUNCTION

This already shows the intended reading: a FUNCTION is a pure expression-level abbreviation. It does not “run later at runtime with its own stack frame” in the usual programming-language sense.

FUNCTION swap(a : ARRAY[0..5] OF INT, i : INT, j : INT) -> ARRAY[0..5] OF INT
    ARRAY(p IN 0..5 : IF p = i THEN a[j] ELSE IF p = j THEN a[i] ELSE a[p])
END_FUNCTION

FUNCTION bubble(a : ARRAY[0..5] OF INT, k : INT) -> ARRAY[0..5] OF INT
    IF k <= 0 THEN a
    ELSE IF a[k - 1] <= a[k] THEN a
    ELSE bubble(swap(a, k - 1, k), k - 1)
END_FUNCTION

FUNCTION isort(a : ARRAY[0..5] OF INT, k : INT) -> ARRAY[0..5] OF INT
    IF k <= 0 THEN a
    ELSE bubble(isort(a, k - 1), k)
END_FUNCTION
...
    sorted := isort(xs, 5);

(Full example: examples/algorithms/insertion_sort.lola.)

A FUNCTION is a compile-time macro: the compiler inlines it and unrolls the recursion completely, leaving a loop-free expression. The one hard rule makes that always possible: recursion must reduce a static measure — here the index k, known at each call site by constant folding — so it bottoms out at compile time. A PLC scan has bounded WCET; a recursion on a runtime measure would not, and is a compile error.

✅ Verified four ways: reference simulator = Z3 model = executed ST = compiled Rust, over the whole unrolled chain (tests/test_functions.py). Unlike SORT, nothing is auto-proven sorted here — you defined the computation, so it scales further than the proof-bounded SORT.

Design choice — synthesis vs. definition, one model. SORT and RULE state a property and let the machine find and prove a realisation (synthesis); the recursive FUNCTION gives the computation and lets the machine prove the unrolled chain. All three end at the same proven Z3 model, and the same backends print it. The unrolled network is a shared-object DAG — memoised, then CSE'd into temporaries computed once — so the emitted code stays compact even though each recursive step conceptually rebuilds the array.

17. Reusable operations: `FUNCTION` contracts¶

A FUNCTION is a compile-time-inlined, side-effect-free operation — no memory, no scan-to-scan state. You have already seen functions used as helpers inside sorting (§16). Give a function a contract and the compiler proves it before anything calls it.

Contract vocabulary:

REQUIRE <bool>; — a precondition the caller must earn; the compiler checks it at every call site.
ENSURE <bool>; — a postcondition the function guarantees; inside ENSURE, the function's own name stands for its return value.
VARIANT <int>; — a termination measure for a recursive function; the compiler verifies it strictly decreases.

A precondition and a postcondition¶

A saturating clamp is only meaningful when the bounds are correctly ordered:

FUNCTION clamp3(x : INT, lo : INT, hi : INT) -> INT
  REQUIRE lo <= hi;
  ENSURE  clamp3 >= lo;
  ENSURE  clamp3 <= hi;
  IF x < lo THEN lo ELSE IF x > hi THEN hi ELSE x
END_FUNCTION

The compiler proves the body establishes both ENSUREs given the REQUIRE. The call site must earn that precondition:

FUNCTION_BLOCK Limiter
VAR_INPUT v : INT; a : INT; b : INT; END_VAR
VAR_OUTPUT y : INT; END_VAR
IMPLEMENTATION
    y := clamp3(v, a, b);
    ASSUME a <= b;                    -- earns clamp3's REQUIRE at this call site
    INVARIANT y >= a AND y <= b;      -- PROVEN from clamp3's ENSURE
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Drop the ASSUME and the block no longer compiles — the precondition is not earned. The error is blamed at the call site (contract-require), not inside clamp3 — so you know immediately whether the function or its caller is at fault.

Watch for INT overflow. INT is 16-bit and wraps. A contract like ENSURE f >= a over a + n is only provable when a + n cannot overflow. Bound inputs with REQUIRE, or state an overflow-safe contract.

Recursion: `VARIANT` makes termination explicit and checked¶

Recursion is allowed only when a strictly decreasing measure makes it terminate. VARIANT names that measure; the compiler verifies it:

FUNCTION countdown(n : INT) -> INT
  REQUIRE n >= 0;
  ENSURE  countdown = 0;
  VARIANT n;
  IF n <= 0 THEN 0 ELSE countdown(n - 1)
END_FUNCTION

VARIANT n declares that every recursive call decreases n; a measure that does not strictly decrease is a hard error. The real worked example is examples/algorithms/insertion_sort.lola: bubble and isort both carry VARIANT k, prove sortedness, and promise ENSURE PERMUTATION_OF(a).

Named predicates¶

A FUNCTION -> BOOL is a named predicate, usable in any INVARIANT, ASSUME, REQUIRE, or ENSURE:

FUNCTION nonneg(a : ARRAY[0..3] OF INT) -> BOOL
  ALL(i IN 0..3 : a[i] >= 0)
END_FUNCTION

FUNCTION_BLOCK Gate
VAR_INPUT xs : ARRAY[0..3] OF INT; END_VAR
VAR_OUTPUT ok : BOOL; END_VAR
IMPLEMENTATION
    ok := nonneg(xs);
    ASSUME ALL(i IN 0..3 : xs[i] >= 0);
    INVARIANT ok = TRUE;              -- PROVEN via the inlined predicate
END_IMPLEMENTATION
END_FUNCTION_BLOCK

ENSURE PERMUTATION_OF(a) is the one intrinsic postcondition: it says the result is a rearrangement of array parameter a. It is proved structurally (the index-witness approach from §16), not as an SMT formula — because a symbolic permutation predicate sends the solver into an explosion; see insertion_sort.lola.

18. Calling externally verified code: `EXTERN … BY`¶

Some operations cannot be proved inside LoLa, but can be verified by an external tool. EXTERN FUNCTION … BY <artifact> lets that external proof enter the model.

The motivating example: saturating absolute value¶

Consider absolute value for INT. The obvious attempt fails:

FUNCTION abs_attempt(x : INT) -> INT
  ENSURE abs_attempt >= 0;          -- REJECTED by the compiler
  IF x < 0 THEN -x ELSE x
END_FUNCTION

The compiler is right. INT is 16-bit; -(-32768) overflows and wraps to -32768, a negative number. The body does not establish >= 0 for every input. No pure LoLa proof exists.

The registry ships a Rust implementation (abs_sat_i16) that saturates the one overflow case: abs_sat(-32768) = 32767. It is proved exhaustively over all 65536 i16 inputs by an external harness. EXTERN lets that warrant flow in:

EXTERN FUNCTION abs_sat(x : INT) -> INT
  ENSURE abs_sat >= 0;
  BY abs_sat_i16;

FUNCTION_BLOCK SaturatingAbs
VAR_INPUT  v : INT; END_VAR
VAR_OUTPUT y : INT; END_VAR
IMPLEMENTATION
    y := abs_sat(v);
    INVARIANT y >= 0;                -- PROVEN by assuming abs_sat_i16's warrant
END_IMPLEMENTATION
END_FUNCTION_BLOCK

The BY abs_sat_i16 clause names a specific artifact. It is optional: without it, the compiler selects an implementation automatically from all registered artifacts whose contract matches the ENSURE clause. BY is a selection hint — the contract always holds regardless of which artifact is chosen.

How it works:

The model ASSUMEs abs_sat >= 0 at every call site — justified by the artifact's warrant, not re-derived by Z3. An INVARIANT y >= 5 would be rejected because the warrant is >= 0 and no wider.
The Rust backend ships the abs_sat_i16 artifact verbatim and emits the call. The ST backend reads its own ST artifact from the same registry entry.

The trust boundary — explicit and traced¶

EXTERN is honest by construction. The compiler labels every INVARIANT that rests on an EXTERN contract with the artifact and warrant it inherits:

INVARIANT y >= 0 : assumed via EXTERN abs_sat_i16 {rust: proved, st: audited}

An invariant that reads no EXTERN output is a pure LoLa proof and carries no such label. audited and proved are distinct; a [!] flag appears on any invariant that rests on a less-than-proved warrant. The PILOT profile (minimum_extern_warrant = "proved") enforces this at compile time and refuses to build if the weakest attained warrant falls below proved across the required targets.

A second operation: `sat_add`¶

A second artifact — sat_add_i16, a saturating signed addition — was added to the registry by writing only a manifest entry and a reference implementation; the parser, model, and backends were not touched. Its contract is multi-argument and references the inputs:

EXTERN FUNCTION sat_add(a : INT, b : INT) -> INT
  ENSURE NOT (a >= 0 AND b >= 0) OR sat_add >= 0;
  ENSURE NOT (a <= 0 AND b <= 0) OR sat_add <= 0;
  BY sat_add_i16;

With ASSUME x >= 0; ASSUME y >= 0;, the invariant s >= 0 on s := sat_add(x, y) is discharged by threading the ASSUMEs into the assumed postcondition. This is a guarantee LoLa's own wrapping + cannot make: 20000 + 20000 overflows and becomes a negative number; the saturating version clamps it to 32767.

The pattern generalises: a new externally-verified operation needs a reference implementation, a VerificationRecipe, and an EXTERN declaration — no compiler code, no parser change. The lola extern toolchain (init / verify / register / check) manages the registry side; see how-to/verified-functions.md if you want to add one. For the worked examples as LoLa programs, see examples/extern/.

19. Where the representation comes from (advanced)¶

One more payoff of stating bounds. If you ask, LoLa will use Z3 to certify the value range of each REAL signal from your invariants, ASSUMEs and CLAMPs, and pick the smallest fixed-point integer type that holds it safely:

$ python -m lola level.lola --profile float64
OK: Level verified (1 outputs, 2 invariant(s) proven).
REAL representations (Z3-certified range -> fixed-point width):
  h: [0, 20] -> i16

A signal proven to stay in [0, 20] fits a 16-bit integer; one that can reach ±100 needs 32 bits; an unbounded one falls back to the widest type. When enabled, the Rust backend then stores each signal in its chosen width. This matters on memory-constrained targets and FPGAs, and — as with everything in LoLa — it is proven safe, never guessed.

When the search space explodes — and what to do about it¶

Formal methods are not magic. Some formulations are easy to prove; others are logically equivalent but make the search blow up. In practice, three patterns are the usual culprits:

Huge symmetric choice spaces. “Find me some arrangement” is much harder than “here is the construction; prove it works”. That is why SORT and permutation(...) are compiler-guided realisations rather than open-ended synthesis problems.
Symbolic indexing and nested case splits. Expressions like a[f(i)] or deeply nested conditionals generate large proof terms quickly; they ask the solver to reason about many possible data routes at once.
Unbounded or weakly bounded arithmetic. A proof gets much easier once the block states its operating envelope (ASSUME, CLAMP, units, invariants) instead of leaving every signal mathematically unconstrained.

What helps in practice:

Write the operating envelope down. Bounds on inputs, gains, limits, pressures, temperatures, selector ranges. They are not “extra decoration”; they are what turns an open world into an engineering problem.
Prefer structured declarative operators over hand-coded search. ALL, ANY, COUNT, SUM, MIN, MAX, ARRAY(...), SORT, and RULE give the compiler a known semantic shape. An ad-hoc imperative encoding of the same idea is often much harder to analyse.
Separate safety from optimisation. First prove the block cannot do the wrong thing; only then worry about whether it does the most useful thing. If you mix both at once, the proof problem becomes larger and the diagnosis worse.
Strengthen the spec when the counterexample is “technically legal but absurd”. That is not the solver being annoying; it is the tool telling you what your current words still permit.

The practical rule is simple:

Do not ask the solver to guess structure you could have stated directly.

The better you expose bounds, intent and structure in the source, the smaller the search space and the better the diagnostics.

19b. Guided synthesis: when the solver needs a hand¶

Some blocks — schedulers, arbiters, ranking algorithms — have the right kind of specification (RULE constraints) but a search space too large for the bounded synthesiser to explore directly. The answer is guided synthesis: you supply a candidate implementation and a bounded model checker proves it correct.

Here is a 2-pump scheduler whose RULE ties the running pump to accumulated hours:

FUNCTION_BLOCK Relay
VAR_INPUT
    demand : INT;
    ok     : ARRAY[0..1] OF BOOL;
    hours  : ARRAY[0..1] OF DINT;
END_VAR
VAR_OUTPUT
    run : ARRAY[0..1] OF BOOL;
END_VAR
IMPLEMENTATION
    ASSUME demand >= 0;
    ASSUME demand <= 1;
    ASSUME COUNT(i IN 0..1 : ok[i]) >= demand;
    RULE COUNT(i IN 0..1 : run[i]) = demand;
    RULE ALL(i IN 0..1 : (NOT run[i]) OR ok[i]);
    RULE ALL(i IN 0..1 : ALL(j IN 0..1 :
        (NOT (run[i] AND ok[j] AND (NOT run[j]))) OR (hours[i] <= hours[j])
    ));
END_IMPLEMENTATION
END_FUNCTION_BLOCK

This block has synthesis targets (run[0], run[1]) but no := definitions. The bounded synthesiser might not find candidates within its node budget when the third rule (the hours-ranking condition) couples both outputs.

Step 1 — Build the proof request:

lola guided relay.lola --out build/proof/

This writes proof_request.json and the Kani harness skeleton candidate.creusot.rs.

Step 2 — Propose a candidate (LLM-assisted or hand-written):

lola guided --agent claude relay.lola --out build/proof/

The LLM receives the proof request (inputs, outputs, ASSUME and RULE texts) and writes a Rust candidate body. An example correct body for the 2-pump relay:

let run0 = input.demand >= 1 && input.ok[0]
    && (!input.ok[1] || input.hours[0] <= input.hours[1]);
let run1 = input.demand >= 1 && input.ok[1]
    && (!input.ok[0] || input.hours[1] < input.hours[0]);
Relay { run: [run0, run1] }

Note the asymmetry: <= for index 0 (wins ties), < for index 1 (loses ties). This is not decoration — it is what makes the scheduling deterministic.

Step 3 — Accept (prove) the candidate:

lola guided accept relay.lola \
    --candidate build/proof/candidate_response.json \
    --backend kani --out build/proof/

Kani runs symbolic exhaustion over all input combinations. If it reports VERIFICATION SUCCESSFUL, it writes acceptance.json — a GuidedSynthesisWarrant. If it finds a counterexample, you fix the candidate and retry.

Step 4 — Compile with the warrant:

import json
from lola import compiler
from lola.guided_synthesis import make_guided_synthesis_warrant

warrant = make_guided_synthesis_warrant(json.loads(open("build/proof/acceptance.json").read()))
comp = compiler.compile_source(source, guided_synthesis_warrants={"Relay": warrant})
assert comp.report.ok

The compiler checks that the warrant's declaration_sha256 matches the current source contract, skips CEGIS synthesis, and records the warrant in program.assurance.guided_synthesis_warrants.

The connection to EXTERN

This is the same trust structure as EXTERN, applied to a full block rather than a single function:

EXTERN	Guided synthesis
`ENSURE` + artifact	`RULE` + `acceptance.json`
Compiler ASSUMEs the ENSURE	Warrant discharges the RULE proof goal
`ExternalImplementationWarrant`	`GuidedSynthesisWarrant`

The difference is that EXTERN applies to individual function calls (one result value), while guided synthesis covers an entire block's output set with a joint proof.

→ Full workflow details: How-to: Guided synthesis\ → Trust model: Concept: Guided synthesis and EXTERN

19c. Real arithmetic: where synthesis meets numerics¶

Everything above stayed in BOOL/INT territory, where a RULE is a finite-domain statement and any of the provers decides it exactly. RULEs over LREAL are different: they are statements about exact real numbers, proved by Z3 over ℝ — while the running code computes in binary64. Those are two different claims, and LoLa keeps them separate on purpose: the ℝ proof says the algorithm is right, and a separately proved error envelope (|machine − exact| ≤ ε, via the Gappa prover) says how far the binary64 execution can drift from it. This is why the original free-form Rust/Kani and ST/CBMC guided paths refuse LREAL outputs: a model checker running the candidate in f64 would prove a subtly different theorem than the RULE states. GS-v2-N instead accepts a narrow LoLa candidate, proves its RULE over exact reals, emits both machine backends from that same compilation, and accepts only if the Static Numerical Core publishes a proved binary64 error envelope for every numeric output. Its first slice is intentionally combinational: state, PRE, DT, timers, calls, arrays, wiring, templates, and continuous references remain excluded.

The showcase for all of this at once is the Levenberg–Marquardt example: twelve RULE-only LREAL blocks synthesized from one-line contracts (Gram matrix, gradient, damping, updates), one verify-only solver whose Cramer RULEs Z3 proves under det > 0, a composed LM_Step block whose positive-definiteness precondition the compiler discharges symbolically from λ ≥ 1, a runnable PROGRAM fitting a calibration curve live on the Rust runtime — and an end-to-end proved bound |x̂_new − x_new| ≤ 1.02e-12 across all four block boundaries.

→ Worked vertical: examples/algorithms/lm_step/\ → Concept: Synthesis — from RULE contract to proven implementation

20. Using the compiler¶

From a source checkout, invoke as python -m lola. The four modes you have seen in this guide:

python -m lola FILE.lola                     # verify only (default): prove all properties
python -m lola FILE.lola --target st         # emit IEC 61131-3 Structured Text
python -m lola FILE.lola --target rust       # emit Rust
python -m lola FILE.lola --profile float64   # enable REAL → Float64 (required for REAL code)
python -m lola FILE.lola --strict            # treat warnings as errors (CI mode)

The golden rule: verification always runs first, and the backends only ever see a program that passed. ST and Rust are generated from the same proven model, so they agree by construction.

For the full option table — --project, --profile pilot, lola extern, exit codes, and output formats — see the CLI Reference.

21. Sequential Control with SSFC¶

All of the LoLa constructs you have seen so far are about values: rules that define what an output should be, invariants that constrain what values are possible, composition that wires values together. This is the right tool when the question is "what should the motor speed be?" or "is the alarm active?"

Many controllers also have a sequential dimension: the process fills first, then heats, then holds at temperature, then drains — and can be pre-empted into a safe-stopped state at any point. This is mode logic. Encoding it as a set of output rules works, but you end up managing boolean phase-registers manually, writing edge detectors with PRE() to move between phases, and asserting the "only one phase active" invariant by hand.

LoLa provides a second declaration form — the SSFC (Super Sequential Function Chart) — for exactly this. An SSFC is a hierarchy of named states with declared transitions between them. Semantically, an SSFC declaration defines a FUNCTION_BLOCK type: it is a stateful, instantiable component whose behavior is expressed as a state machine rather than as a set of rules. It is not a separate runtime; it lowers to the same LoLa IR and is proved, compiled, and emitted by the same pipeline.

The framing that matters:

Use LoLa rules to describe what values should hold.
Use an SSFC to describe which phase the controller is in, how it moves between phases, and what happens on entry, while active, and on exit.

21.1 A minimal state machine¶

SSFC TankFill
  VAR_INPUT
    go          : BOOL;
    level_high  : BOOL;
    level_empty : BOOL;
  END_VAR
  VAR_OUTPUT
    valve_fill  : BOOL;
    valve_drain : BOOL;
    done        : BOOL;
  END_VAR

  INITIAL STATE Idle
    TRANSITION TO Fill WHEN go;
  END_STATE

  STATE Fill
    EN:  valve_fill  := TRUE;
    EX:  valve_fill  := FALSE;
    TRANSITION TO Drain WHEN level_high;
  END_STATE

  STATE Drain
    EN:  valve_drain := TRUE;
    EX:  valve_drain := FALSE;
    TRANSITION TO Done WHEN level_empty;
  END_STATE

  STATE Done
    EN:  done := TRUE;
    EX:  done := FALSE;
    TRANSITION TO Idle WHEN TRUE;
  END_STATE
END_SSFC

Reading the syntax:

SSFC / END_SSFC wrap the block, like FUNCTION_BLOCK / END_FUNCTION_BLOCK.
VAR_INPUT / VAR_OUTPUT / VAR work identically to FUNCTION_BLOCK.
One state carries the INITIAL keyword — it is active at startup.
Each state declares outgoing transitions: TRANSITION TO <target> WHEN <guard-expression>;
Guards are pure Boolean expressions evaluated against the pre-state (the value of all variables at the start of the current scan, before any lifecycle block has run — exactly like PRE(x) in a FUNCTION_BLOCK).

The scan model for SSFC extends the three-phase model (§2) to nine steps:

1  Snapshot pre-state          — PRE(x) reads from here for the whole scan
2  Evaluate all guards         — of active states and their superstates
3  Select transition           — at most one may fire per scan
4  Execute EX blocks           — of states being left, deepest-first
5  Update marking              — which state is now active
6  Reset T_elapsed             — newly entered states get T_elapsed = 0
7  Execute EN blocks           — of newly entered states, outermost-first
8  Execute DU blocks           — of ALL currently active states, outermost-first
9  Commit                      — outputs observable; becomes pre-state of next scan

If no guard is true in step 3, steps 4–7 are skipped; only DU runs (step 8).

21.2 Lifecycle blocks: EN, DU, EX¶

Every state may declare up to three lifecycle blocks. All are optional; a missing block is equivalent to an empty one.

Block	Runs when	Typical use
EN	Exactly once: the scan the state is entered (after the marking update, before DU)	Set an output TRUE on entry; arm a timer; increment a counter
DU	Every scan the state is active (including the entry scan, after EN)	Continuous feedback; outputs that depend on sensor readings; `T_elapsed`-based values
EX	Exactly once: the scan the state is left (before the marking update)	Reset outputs that EN set; latch a result before leaving

STATE Heat
  EN:
    heater       := TRUE;
    alarm_active := FALSE;
  DU:
    heat_warn    := Heat.T_elapsed >= HEAT_WARN_D;
    alarm_active := alarm_active OR temp_exceeded;
  EX:
    heater       := FALSE;
    heat_warn    := FALSE;
  TRANSITION TO Hold WHEN temp_reached;
END_STATE

EN turns on the heater. Because heater is register-backed, it holds TRUE across scans until something writes FALSE. No DU rule is needed to sustain it.
DU recomputes heat_warn every scan: it becomes TRUE once the state has been active for at least HEAT_WARN_D. It also accumulates alarm_active.
EX clears both outputs in the same scan the state is left, so the next state inherits a clean slate.

PRE(x) vs. direct read inside lifecycle blocks: EX blocks run before EN blocks in the same scan. A direct read of x inside EN sees any value that EX already wrote. PRE(x) always reads the step-1 snapshot, regardless of what earlier lifecycle blocks wrote. The rule: use PRE(x) for "the value this scan began with"; use direct x for "what the current scan's earlier lifecycle blocks produced."

21.3 Implicit fields: State.X and State.T_elapsed¶

Every state S exposes two read-only fields available in any lifecycle block or transition guard in the same SSFC:

S.X : BOOL — TRUE iff S is currently active. Useful in DU blocks of a parent superstate, in guards of sibling states, or in the rules of a composed FUNCTION_BLOCK.

S.T_elapsed : TIME — The elapsed time since S was most recently entered. Zero in the entry scan; increments by DT (the scan cycle time) each subsequent scan. Reading T_elapsed of an inactive state is a static error.

STATE Hold
  DU:
    heater        := Hold.T_elapsed < HOLD_TIME;
    hold_ok_light := Hold.T_elapsed >= HOLD_CONFIRM;
  TRANSITION TO Drain WHEN Hold.T_elapsed >= HOLD_TIME;
END_STATE

The compiler treats T_elapsed as a symbolic TIME accumulator. Timing properties derived from it are verified for all consistent scan rates, not for a fixed rate — the same approach as the HELD/ELAPSED predicates in §7.

21.4 Superstates and preemption¶

A superstate groups child states under a shared parent. Its lifecycle blocks run whenever any child is active. More importantly, a transition declared directly on the superstate is a preemption transition: it fires from any active child, without knowing which one.

SUPERSTATE Production
  INITIAL STATE Fill
    EN:  valve_fill := TRUE;
    EX:  valve_fill := FALSE;
    TRANSITION TO Heat WHEN level_high;
  END_STATE
  STATE Heat
    EN:  heater := TRUE;
    EX:  heater := FALSE;
    TRANSITION TO Hold WHEN temp_reached;
  END_STATE
  STATE Hold
    DU:  heater := Hold.T_elapsed < HOLD_TIME;
    TRANSITION TO Drain WHEN Hold.T_elapsed >= HOLD_TIME;
  END_STATE
  STATE Drain
    EN:  valve_drain := TRUE;
    EX:  valve_drain := FALSE;
    TRANSITION TO Completed WHEN level_empty;
  END_STATE
  TRANSITION TO SafeStopped WHEN abort;    -- preempts ANY of the four children
END_SUPERSTATE

TRANSITION TO SafeStopped WHEN abort is checked every scan regardless of which child is active. When abort is TRUE, the entire Production superstate is left: the active child's EX fires, then Production's EX fires (if declared), then SafeStopped's EN fires — all in the same scan.

Priority rule: a superstate's own transitions always have higher implicit priority than any child transition in the same scan. If Fill's level_high guard and Production's abort guard are both TRUE simultaneously, the abort transition is selected.

LCA-based EX/EN ordering: When a transition fires, the compiler computes the Lowest Common Ancestor (LCA) of the source and target states. EX blocks fire from the source up to (but not including) the LCA, deepest-first. EN blocks fire from the LCA down to the target, outermost-first. This mirrors a stack-unwind/push pattern: nested context is removed before new context is added.

21.5 Parallel regions and synchronisation¶

A superstate may contain parallel regions — two or more independent sub-machines that run concurrently while the superstate is active.

SUPERSTATE Calibrate
  PARALLEL
    REGION arm_a
      INITIAL STATE A_Move
        EN:  joint_a := TRUE;
        EX:  joint_a := FALSE;
        TRANSITION TO A_Done WHEN a_at_position;
      END_STATE
      STATE A_Done END_STATE
    END_REGION
    REGION arm_b
      INITIAL STATE B_Move
        EN:  joint_b := TRUE;
        EX:  joint_b := FALSE;
        TRANSITION TO B_Done WHEN b_at_position;
      END_STATE
      STATE B_Done END_STATE
    END_REGION
    JOIN FROM A_Done, B_Done TO Ready;
  END_PARALLEL
  TRANSITION TO Aborted WHEN emergency;
END_SUPERSTATE
STATE Ready
  EN: ready_light := TRUE;
  TRANSITION TO Idle WHEN NOT start;
END_STATE

Entering Calibrate is a fork: both A_Move and B_Move activate in the same scan.
Each region advances independently. A_Move may reach A_Done while B_Move is still moving.
The JOIN fires in the first scan where both A_Done and B_Done are simultaneously active. It exits both regions atomically and enters Ready.
TRANSITION TO Aborted WHEN emergency preempts both regions at once, just as a superstate preemption exits all child states in an exclusive SSFC.

Write-conflict rule: Two simultaneously-active regions must not write the same output variable in lifecycle blocks. The compiler rejects it: ssfc-cross-region-conflict.

21.6 What the compiler checks¶

python -m lola batch_controller.lola

The assurance report names eight claims:

Claim	What it verifies
C-SAF	1-Safeness: for every (region, transition) pair, token balance adds up. Exact.
C-INT	Region integrity: transitions stay within structural scope; parallel coverage is consistent. Exact.
C-DEAD	No leaf state is structurally stuck (zero outgoing transitions, no TERMINAL). Exact.
C-GUARD-SAT	Every WHEN guard is satisfiable over the type domain. SMT.
C-DET	No two guards of the same state can be simultaneously TRUE without PRIO. SMT.
C-DATA-DEAD	No guard is permanently FALSE. Environmental Waiting (EW) distinguished from deadlock. SMT.
C-REACH	Every state reachable via individually-SAT-satisfiable guard sequence. SMT.
C-HOME	Per-place witness path to a nominated home state found. Over-approximation: PASS ≠ guaranteed return-to-home. SMT.

For an EW verdict on a transition: the machine is correctly waiting for a VAR_INPUT to change — that is not a bug. A WARN on C-HOME for a state in a parallel region means the per-place BFS found no witness path; this is a sound indicator but does not constitute a formal deadlock proof.

Add TERMINAL to a state that is intended to be a valid resting point with no outgoing transitions:

STATE Completed TERMINAL
END_STATE

21.7 Composing components with WIRING¶

An SSFC state can run a child component — a FUNCTION_BLOCK or another SSFC — as a wired sub-controller. The WIRING block inside a state declares which child instances are active there, and how their ports connect to the parent's signals.

SSFC PasteurizerSequence
  VAR_INPUT
    temp_actual : MATHREAL;
    abort       : BOOL;
    level_empty : BOOL;
  END_VAR
  VAR_OUTPUT
    heater_cmd  : MATHREAL;
  END_VAR
  VAR
    pid         : PID_Temperature;
  END_VAR

  SUPERSTATE Production
    STATE Heat
      WIRING pid
        __ssfc_dt := __ssfc_dt;          (* forward scan-cycle time *)
        pid.setpoint := HEAT_SETPOINT;
        pid.actual   := temp_actual;
        heater_cmd   := pid.output;
      END_WIRING
      TRANSITION TO Hold WHEN temp_reached;
    END_STATE
    STATE Hold
      DU: heater_cmd := Hold.T_elapsed < HOLD_TIME ? HOLD_POWER : 0.0;
      TRANSITION TO Drain WHEN Hold.T_elapsed >= HOLD_TIME;
    END_STATE
    TRANSITION TO SafeStopped WHEN abort;
  END_SUPERSTATE

  STATE SafeStopped
    EN: heater_cmd := 0.0;
  END_STATE
END_SSFC

What WIRING does:

The child instance pid runs every scan that the enclosing state (Heat) is active. It is not re-initialised on re-entry unless its EN block says so.
Port bindings are written as assignments: child.port := expr for inputs, parent_output := child.port for outputs. You can mix reads and writes freely within one WIRING block.
__ssfc_dt is the parent's scan-cycle time parameter. It must be forwarded explicitly when the child is itself an SSFC.
inst* (star-wiring): if the child has ports with the same name and a compatible type as signals already in scope, WIRING pid inst*; END_WIRING auto-wires them. Explicit bindings take priority over star-wiring.

What WIRING does not do: it does not alter state machine execution or create a separate control thread. The child's scan is synchronous with the parent's — one child update per parent scan, inside the parent's DU phase. The child's outputs become visible in the same scan they are computed, and its internal registers persist across scans just like any FUNCTION_BLOCK.

21.8 Signal ownership analysis¶

When multiple states write the same output, the compiler cannot statically guarantee that exactly one writer is active at any moment. LoLa's Write Ownership analysis resolves this at analysis time.

In the Pasteurizer above, heater_cmd is written in Heat (via PID output), in Hold (via DU), and in SafeStopped (via EN). Run the analysis:

from lola.ssfc_ownership import analyze_ownership

report = analyze_ownership(ssfc, net, mg)
for sig in report.all_signals():
    print(sig.name, sig.ownership_class)

Typical output:

heater_cmd   EXCLUSIVE_MULTI_WRITER

The result means: multiple states write heater_cmd, but the compiler has proved they cannot all be active in the same scan. Heat, Hold, and SafeStopped are in an exclusive hierarchy — at most one is active per scan — so no write conflict is possible.

OwnershipClass summary:

Class	Safe?	Meaning
`SINGLE_WRITER`	Yes	Only one write site exists.
`EXCLUSIVE_MULTI_WRITER`	Yes	Multiple sites; mutual exclusion formally proved.
`COMPATIBLE_MULTI_WRITER`	Yes	Co-activatable sites, but they write the same value.
`CONFLICTING`	No	Co-activatable sites write different values. Design error.
`UNKNOWN`	Review	Mutual exclusion could not be determined.

CONFLICTING is the only outcome that blocks CI (under the default policy). UNKNOWN is worth reviewing but is not a failure by default.

A transitive component effect is automatically traced when a WIRING block references State.X (the activity marker):

state activation → WIRING → child.input → (child FB) → child.output → parent output

These chains appear in report.component_effects and are analysed alongside direct variable writes. See concepts/ownership-and-effects.md for the full classification rules and how-to/audit-signal-ownership.md for the step-by-step workflow.

21.9 Recovery and progress analysis¶

Write Ownership proves which state writes an output. Recovery and Progress analysis proves whether the SSFC is guaranteed to reach a designated safe state from any reachable configuration.

The Pasteurizer has a natural recovery pair: from Production (any child active) to SafeStopped. Declare the environment's commitment as an ASSUME clause, then run the analysis:

ASSUME abort;   (* safety interlock: abort stays asserted once raised *)

from lola.ssfc_recovery import analyze_recovery, render_claim_md
from lola.ssfc_marking import build_marking_graph

mg    = build_marking_graph(net)
claim = analyze_recovery("Production", "SafeStopped", ssfc, net, mg)
print(render_claim_md(claim))

The report has four independent claim levels:

STRUCTURAL   ✓ PROVED
             path: Production → SafeStopped (1 transition)

POSSIBLE     ✓ PROVED
             per-edge SAT path: abort is satisfiable

GUARANTEED   ≈ PROVED-CONDITIONAL
             all admissible executions reach SafeStopped
             requires: ASSUME abort

BOUNDED      ≈ PROVED-CONDITIONAL
             within 1 scan (worst-case attractor rank)
             requires: ASSUME abort

Reading the levels:

STRUCTURAL checks the marking-graph topology, ignoring all guards. It confirms a path exists at all.
POSSIBLE checks that a guard-satisfiable path exists (per-edge SAT). It does not prove all executions take that path.
GUARANTEED proves that every admissible execution from Production eventually reaches SafeStopped. PROVED-CONDITIONAL means this holds given the declared ASSUMEs; without them the guard abort might never be TRUE and the system could remain in Production indefinitely.
BOUNDED gives the worst-case number of scans. If the scan cycle is 10 ms and BOUNDED = 1, the guaranteed recovery time is at most 10 ms.

The assumptions_used field (on the GUARANTEED evidence) lists only the ASSUME clauses that are load-bearing — those whose removal causes GUARANTEED to fail. Non-contributing ASSUMEs are excluded.

A second pair, SafeStopped → Idle, depends on an operator action (reset_request). With no ASSUME for it, GUARANTEED is NOT PROVED — which is the correct result: the system can reach Idle (POSSIBLE = PROVED), but no external contract guarantees it ever will. This is not a bug; it is an accurate characterisation of an operator-triggered transition.

For the full step-by-step workflow — choosing states, when to add ASSUMEs, and how to interpret NOT PROVED — see how-to/prove-safe-recovery.md.

22. What LoLa is — and is not¶

It helps to know the shape of the box you are working in. LoLa is a synchronous, reactive state-transition language for control logic — not a general-purpose, Turing-complete programming language. A block reads inputs, computes its next state from the current state, and writes outputs, once per scan. Computation unfolds over time (across scans), never as an unbounded loop within a scan.

The single boundary that draws the box is the Bounded-Cycle-Theorem: every valid LoLa program has a statically proven, finite per-scan execution. This — not a list of banned features — is the real admission test. It is exactly why CBMC is complete on the generated code and why Z3 decides the model. Everything you have met either is, or is not, admissible by that one criterion:

Arrays and repetition are allowed — but only at statically fixed size. An aggregate or a MAP over 1..8 is bounded repetition with a statically known trip count (§13–15). A SORT, a RULE-defined array, a recursive FUNCTION are all admitted because they unroll to a finite expression whose size is known now (§16–17). What is not admissible is a loop or an array whose length is a runtime value.
Unsafe operations are allowed — but only with a discharged proof. Division and a dynamic array index are partial; they compile only when the divisor / index is proven safe (§9, §14).
INT has + - * but no division or modulo (only REAL divides, as a guarded partial operation).

These are not oversights — they are the price and the enabler of the “prove all states” guarantee. The boundary is easiest to feel with three examples in examples/algorithms/:

Fibonacci (fibonacci.lola) fits naturally — it is a state machine: two registers, (a, b) → (b, a + b), one number per scan. (Registers have no custom init, so a seeded flag sets a = 0, b = 1 on the first scan; INT is 16-bit, so it wraps after F(24).)
Sorting fits at a fixed size — and §16 shows the declarative way to say it: SORT, a RULE spec, or a bounded recursive isort. The early bubble_sort5.lola hand-unrolled a compare-swap network; its successors state the result instead. What all of them share is the fixed size — arbitrary-length sorting needs a runtime-bounded loop, which is not expressible.
is_prime(n) (is_prime.lola) fits only bounded: with no modulo or loops, compositeness is an aggregate — n is composite iff ANY(a, b : a·b = n) over a bounded product range. Unbounded primality needs unbounded computation LoLa deliberately cannot express.

The rule of thumb: if a construct has a statically finite execution, it fits — whether that is a bounded state machine, a statically bounded aggregate, a synthesised network, or a bounded recursion. If it needs runtime-unbounded data or iteration, it does not. If you find yourself wanting a for loop whose trip count only the plant knows, you have stepped outside what a verifiable PLC block is — and that is by design.

23. The whole language, on one page¶

You declare the what, not the how. Outputs are defined by prioritised rules (registers, which have memory) or by := (derived, combinational). The compiler synthesises the formula and prints it as ST or Rust.
Priority is explicit. The highest-priority active rule wins; the order you wrote the rules is irrelevant; equal-priority conflicts are compile-time errors, and dead rules are reported as warnings (or as errors in --strict mode).
Reading time is defined. Inside a register's rules, other registers read their old (start-of-scan) value; through a := definition they read their new value. All outputs update simultaneously (the _next staging).
Properties are proven, not tested. INVARIANT is proven by induction over all states; timers are symbolic, so timing properties hold for all timings; a failed proof comes with a concrete counterexample.
Unsafe operations carry obligations. Division and a dynamic array index require a proof (or a path-sensitive IF guard) that the divisor is non-zero / the index is in range.
Repetition is bounded and static. Arrays have a compile-time size; aggregates (ALL ANY COUNT SUM MIN MAX) and the ARRAY(…) MAP emit as loops with statically known bounds, and are proven structurally (quantifier, recurrence, or witness axioms) rather than by expanding them. A SORT or a permutation RULE is synthesised into a compare-swap network and its sortedness proven; a FUNCTION may recurse only on a static measure, so it unrolls fully. Everything obeys the Bounded-Cycle-Theorem: a statically proven, finite per-scan execution.
Template blocks scale structure without runtime generics. FUNCTION_BLOCK Vec<N: UINT> is a compile-time recipe: each instantiation (Vec<3>, Vec<4>) is monomorphized into a separate concrete type with concrete array bounds, its own proof, and its own generated code — the static-size invariant never bends.
Contracts scale. ASSUME states caller obligations; under composition a child premise either bubbles up to the caller (wired to parent inputs) or is discharged by the parent as a proof obligation (wired to internal logic); child invariants are preserved.
Functions carry their own contracts. A FUNCTION with REQUIRE/ENSURE is proved by the compiler before any call site sees it; the ENSUREs become available facts at every call, and the compiler blames the call site if the REQUIRE is not earned (§17).
External proofs join by contract. An EXTERN FUNCTION … BY <artifact> lets a warrant from an external tool (exhaustive enumeration, Creusot, CBMC) flow into the model as an assumed postcondition. Every invariant that rests on it is labelled with the artifact and its warrant — audited or proved — so nothing is silently promoted (§18).
Units and ranges are static. Dimensional analysis is checked then erased; certified ranges choose the numeric representation — all without changing behaviour.
One source of truth. Every rule above is defined once, in the Z3 model. The ST and Rust backends are pretty-printers over it and cannot diverge from the proof or from each other.

For the normative specification of every construct above — syntax, semantics, proof obligations, and diagnostics — see the Language Reference.

24. Four mental checkpoints¶

Before you write a LoLa block, ask yourself these four questions:

What is state, and what is just a fresh calculation? If it must remember across scans, it is a register (rules). If it is just computed from this scan's results, it is :=.
What happens if two conditions are true at once? Write the priorities so the conflict is explicit. Do not rely on text order.
What must never happen? Those are candidates for INVARIANT.
What must the environment promise me? Those are candidates for ASSUME.
What can the compiler prove itself, and what needs an external warrant? If a pure LoLa FUNCTION can establish the property (§17), use that. If the operation has a soundness gap LoLa cannot close — overflow, a domain-specific algorithm, a Creusot/CBMC proof — declare it EXTERN … BY <artifact> (§18) and the compiler will label every invariant that rests on it with the warrant it inherits.

That is LoLa: you write intent and safety requirements; a machine proves them and writes the code. Your job shifts from ”did I code it right?” to ”did I specify the right thing?” — and the compiler guarantees the rest.

Where to go next

You want to…	Go to
Look up a keyword, type, or operator	Language Reference
Look up SSFC syntax and semantics	Language Reference §21 — SSFC
Look up ownership and recovery claim definitions and EvidenceStrength	Assurance Reference
See all CLI options and output formats	CLI Reference
Configure REAL representation or sampling	Project Configuration Reference
Model a sequential process with SSFC	How-to: Model a Sequential Machine
Model concurrent sequences with JOIN	How-to: Model Parallel Regions
Compose an SSFC with FB or SSFC child components	How-to: Compose Components
Check which state owns each output	How-to: Audit Signal Ownership
Prove safe recovery within N scans	How-to: Prove Safe Recovery
Add an externally-verified function	How-to: Verified Functions
Configure REAL / Float64 representation	How-to: Configure REAL Representation
Diagnose a proof failure	How-to: Diagnose Proof Failures
Understand pre-state semantics and priorities	Concepts: Synchronous semantics
Understand SSFC scan model and assurance scope	Concepts: SSFC Semantics
Understand FB/SSFC composition and WIRING	Concepts: Component Model
Understand signal ownership analysis	Concepts: Ownership and Effects
Understand recovery and progress analysis	Concepts: Recovery and Progress
Understand REAL = ℝ and the numerical assurance chain	Concepts: Numerical semantics
Understand what "proved" guarantees	Concepts: Assurance model
Understand EXTERN warrant inheritance	Concepts: EXTERN trust model
Understand guided synthesis and its relationship to EXTERN	Concepts: EXTERN trust model §guided-synthesis
Accept and use a guided synthesis candidate	How-to: Guided synthesis
Look up GuidedSynthesisWarrant fields	Reference: GuidedSynthesisWarrant
Read the compiler internals	Architecture

LoLa — An Introduction by Example¶

0. Before we start: what problem does LoLa solve?¶

1. Your first block: an RS latch¶

What the compiler makes of it¶

2. How a block runs: one scan, all-at-once¶

3. Two kinds of memory: registers and derived values¶

4. Priorities in depth, and the errors that keep them honest¶

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

When a proof fails, you get a counterexample¶

Three non-obvious bugs the compiler catches for you¶

6. A safety property worth proving: mutual exclusion¶

6b. PARAMETER: one block, many machines¶

The REQUIRE is not decoration¶

What a configuration constraint may mention¶

7. Time, made symbolic¶

Why this lets us prove timing-independent properties¶

8. Continuous values: REAL, DT, CLAMP¶

9. Partial operations: division and IF/THEN/ELSE¶

10. Environment premises: ASSUME¶

11. Building bigger blocks: composition¶

11b. Template blocks — reusing logic at different sizes¶

12. Physical units — catching “apples plus oranges” at compile time¶

13. Arrays and bounded repetition¶

What the compiler makes of it¶

14. Indexing as a partial operation¶

What the compiler makes of it¶

15. Building arrays: the MAP¶

What the compiler makes of it¶

16. Three ways to say “sorted”¶

16.1 State the result — SORT¶

16.2 Constrain the result — RULE¶

16.3 Define the computation — a bounded recursive FUNCTION¶

17. Reusable operations: FUNCTION contracts¶

A precondition and a postcondition¶

Recursion: VARIANT makes termination explicit and checked¶

Named predicates¶

18. Calling externally verified code: EXTERN … BY¶

The motivating example: saturating absolute value¶

The trust boundary — explicit and traced¶

A second operation: sat_add¶

19. Where the representation comes from (advanced)¶

When the search space explodes — and what to do about it¶

19b. Guided synthesis: when the solver needs a hand¶

19c. Real arithmetic: where synthesis meets numerics¶

20. Using the compiler¶

21. Sequential Control with SSFC¶

21.1 A minimal state machine¶

21.2 Lifecycle blocks: EN, DU, EX¶

21.3 Implicit fields: State.X and State.T_elapsed¶

21.4 Superstates and preemption¶

21.5 Parallel regions and synchronisation¶

21.6 What the compiler checks¶

21.7 Composing components with WIRING¶

21.8 Signal ownership analysis¶

21.9 Recovery and progress analysis¶

22. What LoLa is — and is not¶

23. The whole language, on one page¶

24. Four mental checkpoints¶

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

6b. `PARAMETER`: one block, many machines¶

The `REQUIRE` is not decoration¶

8. Continuous values: `REAL`, `DT`, `CLAMP`¶

9. Partial operations: division and `IF/THEN/ELSE`¶

10. Environment premises: `ASSUME`¶

15. Building arrays: the `MAP`¶

16.1 State the result — `SORT`¶

16.2 Constrain the result — `RULE`¶

16.3 Define the computation — a bounded recursive `FUNCTION`¶

17. Reusable operations: `FUNCTION` contracts¶

Recursion: `VARIANT` makes termination explicit and checked¶

18. Calling externally verified code: `EXTERN … BY`¶

A second operation: `sat_add`¶