LoLa

LoLa is a declarative language for PLC logic whose semantics are defined by SMT. Every program you write is a set of equations, rules and invariants; the compiler proves them with Z3 before any code is emitted — the solver is the single source of truth, not a linter bolted on after the fact.

FUNCTION_BLOCK StartStop
VAR_INPUT  Start : BOOL; Stop : BOOL; END_VAR
VAR_OUTPUT Running : BOOL; END_VAR
VAR        latch : RS; END_VAR
IMPLEMENTATION
    latch(S := Start, R1 := Stop);
    Running := latch.Q1;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Where to go

• Tutorial — introduction by example: the language from first contact to proven blocks.
• How-to guides: task-oriented recipes — run a program, compose components, diagnose a proof failure.
• Reference: the normative language definition, CLI, assurance claims and configuration.
• Explanation: why the language is built this way — scan semantics, ownership, the assurance model.

Backends and toolchain

LoLa compiles to Structured Text (IEC 61131-3) and Rust from one proven model, with a reproducible Nix toolchain and a native no_std runtime architecture. See Architecture for the full picture.