Skip to content

Introduction by example

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

The chapters

Each chapter stands on its own, but they build in order: a block, then a proof about it, then the values it works on, then how blocks compose.

  1. One block — An RS latch, one scan, the two kinds of memory, priorities, and saying when instead of what.
  2. Proving something — INVARIANT, a safety property worth proving, the same block said as a contract, and PARAMETER.
  3. Values and time — Symbolic time, MATHREAL/DT/CLAMP, partial operations, and ASSUME.
  4. Putting blocks together — Composition, template blocks, and physical units.
  5. Many values at once — Arrays, indexing as a partial operation, MAP, and three ways to say “sorted”.
  6. Code from elsewhere — FUNCTION contracts, EXTERN … BY, where the representation comes from, guided synthesis, and the compiler.
  7. Sequential control — SSFC: steps, transitions, parallel regions.
  8. Looking back — What zqel is and is not, the whole language on one page, and four mental checkpoints.

0. Before we start: what problem does zqel 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:

  1. 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.
  2. 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”.

zqel 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 zqel'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.

zqel 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. zqel is also not imperative in the usual “statement sequence with loops and mutable program counters” sense. The best description is:

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

“Total” here means: every accepted zqel 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: zqel 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 zqel 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; zqel 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, zqel 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 zqel 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:

  1. Did I implement it right?
  2. Did I specify it right?
  3. 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. zqel 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 zqel 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 zqel 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.

zqel attacks both. In zqel 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 zqel 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 zqel. Let us see it.