Industrial / PLC-class Controllers

This vertical targets controls engineers, plant automation leads, and systems integrators who have a working PLC stack and are evaluating whether an LLM-generated rule layer can be trusted on safety-adjacent logic. Familiarity with IEC 61131-3, ladder logic, or structured text is assumed; familiarity with Synoema is not.

1. Why contracts matter for industrial

Industrial control carries sixty years of safety-first culture that general-purpose software does not. When a fuel-pump shutdown or a feed-valve interlock is written in ladder logic on a Siemens S7 or an Allen-Bradley CompactLogix, the engineer inherits conventions codified in IEC 61131-3 (structured text, ladder, function block diagrams) and extended in IEC 61508 (functional safety) and its vertical derivatives (IEC 61511 for process, ISO 26262 for automotive, EN 50128 for rail). These standards share a shape: safety-relevant logic is not "code that happens to be correct" — it is a specification with pre- and post-conditions, cross-checked by review, by tools, and where the SIL level demands it, by formal analysis.

The LLM-code-generation wave has not seriously engaged with this culture. When an engineer asks Claude or GPT to "write me a Lua script that shuts down the pump when pressure exceeds 500 kPa," they get a one-liner — in ASCII, not in a specification language. If the model emits >= instead of >, or reads pressure from a nullable source without guarding negative sensor noise, the bug is silent. The script runs. The first time the bug is discovered is the first overpressure event.

This is the gap Synoema closes. Synoema's requires / ensure contracts are not comments — they are compiled into the generated WASM binary and checked at runtime. A rule whose ensure does not hold raises a postcondition violated error before the actuator is driven. The engineer's intent is captured in a form the compiler can check, and the LLM that wrote the rule cannot silently drift away from that intent on the next regeneration because the contract is the intent, re-presented to the model every time.

2. Side-by-side — Synoema vs Lua

Lua is the most widely-deployed scripting language in industrial edge devices today, shipping inside NodeMCU, OpenPLC, RevPi, and many vendor firmwares. The same rule — emergency pump shutdown at 500 kPa — in both languages:

Synoema (this change)

rule_pump_overpressure : Int -> Bool
  requires pressure >= 0
  ensure result == (pressure > 500)
rule_pump_overpressure pressure = pressure > 500

Lua (typical industrial edge script)

function rule_pump_overpressure(pressure)
    if pressure > 500 then
        return true
    else
        return false
    end
end

The silent bugs the contract catches

1. Off-by-one on the threshold. An engineer (or an LLM) edits the Lua version and types >= instead of >. The function now returns true at exactly 500 kPa — on an analog loop with ±1 kPa sensor quantisation, the pump trips fifty times a day. No test fails; the plant logs fill with nuisance trips. In Synoema, the ensure result == (pressure > 500) clause is checked on every call. If the body returns pressure >= 500, the post-condition fails at the first 500-kPa sample and the runtime raises postcondition violated, instead of silently hammering the pump relay.
2. Negative sensor noise. The pressure transducer occasionally emits -1 or -2 when the ADC is transitioning. The Lua version happily evaluates pressure > 500 on -1 (→ false) and moves on — but on a gauge-pressure reading, -1 is a sensor fault, not a valid zero-pressure reading. The Synoema requires pressure >= 0 clause turns that transducer glitch into an early precondition violated error, which the supervisory layer logs as a sensor-fault event — the actual distinction the operator cares about.
3. Wrong return type. The Lua function silently returns nil if the caller passes a string (pressure = "N/A"), because Lua's comparison operators are loose. Downstream, an if trip then … treats nil as falsy — the pump stays on during a sensor blackout. The Synoema rule is typed Int -> Bool. A sensor-layer attempt to pass a string is a compile-time type error. There is no fallthrough to the pump-stays-on branch.

None of these bugs are exotic. All three are in the first fifty Lua NodeMCU safety-script mistakes you find in any vendor's support backlog. The point is not that Lua is a bad language — it is not — but that none of the three bugs can be expressed as a contract the compiler will check, because Lua does not have contracts. Synoema does.

3. Formal verification chain

The contract is checked at every layer between the engineer's prompt and the bytes that land on the MCU:

[natural-language prompt]
      │
      ▼
[GBNF constrained decoding] ──→ lang/tools/constrained/synoema-iot-rules.gbnf
      │                         (LLM cannot emit a non-rule form
      │                          at token-sampling time)
      ▼
[parser + type checker] ─────→ lang/crates/synoema-parser/
      │                        lang/crates/synoema-types/
      │                        (`sno check` fails on ill-typed or
      │                         pattern-incomplete rules)
      ▼
[contract IR lowering] ──────→ lang/crates/synoema-codegen/
      │                        (Cranelift IR; requires / ensure
      │                         become trap-on-false branches)
      ▼
[WASM v2 heap emit] ─────────→ lang/crates/synoema-codegen-wasm/
      │                        (integer-only rule subset fits the
      │                         bare-MCU target — no allocator)
      ▼
[wasm3 runtime on MCU] ──────→ docs/iot/wasm3-embed.md
                               (contract traps surface as wasm3 trap
                                codes, caught by the host loop)

The first arrow — constrained decoding — is the one incumbent LLM workflows do not have. The LLM cannot accidentally emit os.execute("rm -rf /") inside an industrial rule because the GBNF grammar refuses to sample those tokens. The contract lowering into IR (fourth arrow) is the distinctive Synoema claim. The fifth arrow makes those guarantees portable to sub-megabyte MCUs — the same contract-carrying bytecode runs on a £4 STM32F4 and on a server.

4. Hardware BOM reference

The vertical is hardware-agnostic — the WASM target means the same rule runs on ARM Cortex-M4, ESP32 (Xtensa LX6/LX7), or a RISC-V eval board. Two reference BOMs:

BOM A: STM32F4 Discovery + industrial I/O hat

BOM B: ESP32 + relay bank

Neither BOM is certified. Both are prototyping platforms for bench demonstrations and pre-production trials. Certification path (ISO 26262, IEC 61508) is called out in Out of scope below.

5. Comparison — Synoema vs Lua vs MicroPython vs TinyGo

The take-away is not "Synoema wins every column." It is that on the first column — contracts — Synoema is the only row with Yes, and that column is the one that matters most for the industrial vertical. Every other column is roughly comparable or marked honestly as not-yet-measured.

6. The five rules shipped

Source: lang/examples/iot/verticals/industrial/*.sno. Four of the five carry an ensure; four carry a requires. rule_flow_min_alarm has only a requires because its post-condition is the rule body itself ("alarm iff every sample is below threshold"), and duplicating that predicate in the ensure would be a verification cycle, not a verification signal. Not every rule benefits equally from contracts — the whitepaper is honest about this.

7. Out of scope — explicitly deferred

• Real PLC hardware validation. This change ships source and WASM-compiled artifacts; lab runs the actual STM32F4 / ESP32 validation manually. The demo script is a software-only proof-of-life.
• ISO 26262 / IEC 61508 certification path. Neither the Synoema compiler nor the wasm3 runtime is qualified for safety-integrity-level use today. The certification story is a multi-year effort and a separate whitepaper.
• SIL (Safety Integrity Level) analysis. Beyond the conceptual framing in §1, no SIL level is claimed for the rules shipped here. SIL rating requires FMEA, fault-tree analysis, and test-coverage data that are out of scope for an MVP.
• Modbus RTU / Modbus TCP / OPC-UA protocol integration. The rules consume integer sensor readings and emit integer actuator commands; the bus-adapter layer is a separate integration change.
• Multi-rule orchestration. The rules here are independent predicates. A realistic plant has a scan cycle that composes them under a fixed priority; the orchestration layer is a separate concern.

Cross-references

• IoT Platform overview — 3-tier model, all six verticals
• All Verticals — landing across home, industrial, wearable, automotive, agriculture, healthcare
• IoT Rules DSL — the strict subset enforced by GBNF
• lang/examples/iot/verticals/industrial/ — the five rule files and prompts.json
• scripts/demo_industrial.sh — reproducible demo driver
• Canonical whitepaper on GitHub