A conveyor that ignores its emergency stop

Part 1 verified circuits small enough to hold in your head. This part starts on real machines, one industrial domain at a time, and the first question is never "what does the code do" but "what must never happen here".

The machine

A guarded belt conveyor. An operator presses run, the belt moves, and two things can stop it: the emergency stop mushroom, and the interlocked guard over the pinch point. A warning beacon lights whenever the emergency stop is latched.

The hazard has a name and it is not abstract. Somebody hits the E-stop because a hand, a sleeve or a person is in the machine. If the belt keeps moving after that, the protective device has been defeated and the thing it was protecting against happens.

benchmarks/manufacturing/g_conveyor_interlock/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!(conveyor && estop)"
    justification: "The conveyor must never run while emergency-stop is active."

That is the whole requirement: conveyor and estop never true together. It says nothing about the guard, nothing about the beacon, and nothing about how the logic gets there. A property is the claim you are prepared to defend, not a description.

The correct program

conveyor := NOT estop AND run_cmd AND NOT guard_open. Three contacts in series, and the two protective ones are normally closed, so either of them breaks the path. This is how an interlock is supposed to look.

file	what it is	size	sha256
clean.xml	ladder program, PLCopen XML	2.7 KB	62c65df380f8
bomb.xml	ladder program, PLCopen XML	3.1 KB	45d48ef1ac73
props.yaml	property file	0.2 KB	d7d55a88c756

Recorded 2026-09-04T23:40:48Z. Every build ran the same command.

cp benchmarks/manufacturing/g_conveyor_interlock/clean.xml benchmarks/manufacturing/g_conveyor_interlock/clean.ld
esbmc benchmarks/manufacturing/g_conveyor_interlock/clean.ld --ld-props benchmarks/manufacturing/g_conveyor_interlock/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:48Z.

v8.4

cp benchmarks/manufacturing/g_conveyor_interlock/clean.xml benchmarks/manufacturing/g_conveyor_interlock/clean.ld
esbmc benchmarks/manufacturing/g_conveyor_interlock/clean.ld --ld-props benchmarks/manufacturing/g_conveyor_interlock/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	SAFE	SAFE	correct	pass	0.017 s

v8.4 found its solution by the inductive step (k = 2).

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN run_cmd=NONDET(_Bool);
        ASSIGN estop=NONDET(_Bool);
        ASSIGN guard_open=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN warn=1 && estop;
        ASSIGN conveyor=1 && !estop && run_cmd && !guard_open;
        GOTO 1
     2:

Proved, with the ingestion gate passing. Nothing surprising, which is the point: you need to know what the correct program looks like before the other one means anything.

The same machine, with something added

One branch, four elements, and the interlock is gone:

conveyor := (NOT estop OR (estop AND maint)) AND run_cmd AND NOT guard_open

The added path conducts precisely when the emergency stop is pressed and a maintenance key is turned. Everywhere else in the input space the two programs behave identically. Run the machine normally, for years, and you will never see the difference.

Predict the verdict

You have the rung and the property. Before scrolling, decide what the checker reports and whether the gate passes.

Answer

build	verdict	expected	ingestion gate
v8.4	VIOLATION	VIOLATION	pass

Recorded 2026-09-04T23:40:48Z. Every build ran the same command.

cp benchmarks/manufacturing/g_conveyor_interlock/bomb.xml benchmarks/manufacturing/g_conveyor_interlock/bomb.ld
esbmc benchmarks/manufacturing/g_conveyor_interlock/bomb.ld --ld-props benchmarks/manufacturing/g_conveyor_interlock/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:48Z.

v8.4

cp benchmarks/manufacturing/g_conveyor_interlock/bomb.xml benchmarks/manufacturing/g_conveyor_interlock/bomb.ld
esbmc benchmarks/manufacturing/g_conveyor_interlock/bomb.ld --ld-props benchmarks/manufacturing/g_conveyor_interlock/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	VIOLATION	VIOLATION	correct	pass	0.013 s

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN run_cmd=NONDET(_Bool);
        ASSIGN estop=NONDET(_Bool);
        ASSIGN guard_open=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN warn=1 && estop;
        ASSIGN conveyor=1 && !estop && run_cmd && !guard_open;
        ASSIGN conveyor=1 && estop && maint && run_cmd && !guard_open;
        GOTO 1
     2:

Counterexample. ESBMC's own output. A trace long enough to need it is elided in the middle, and the omission is marked and counted where it happens.

v8.4

State 1  thread 0
----------------------------------------------------
  run_cmd = 1

State 2  thread 0
----------------------------------------------------
  estop = 1

State 3  thread 0
----------------------------------------------------
  guard_open = 0

State 4  thread 0
----------------------------------------------------
  maint = 1

State 5  thread 0
----------------------------------------------------
  conveyor = 1

State 6 file benchmarks/manufacturing/g_conveyor_interlock/bomb.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/manufacturing/g_conveyor_interlock/bomb.ld
  P1
  !(conveyor && estop)

Read the counterexample

Both builds refute it, and the trace is the recipe:

run_cmd    = 1
estop      = 1
guard_open = 0
maint      = 1
conveyor   = 1

The emergency stop is pressed and the belt is running. Notice what the verifier handed you: not a warning that something looks odd, but the exact input combination that opens the hole. That combination is the trigger, and recovering it is what trigger synthesis means in the suite's vocabulary.

Why this is a bomb and not a bug

A bug is a mistake. Look at the added branch and ask what mistake produces it. Nobody types a series pair of estop and maint by accident, and nobody wires it in parallel with the normally closed contact that it exactly cancels. The branch is deliberate, targeted at the one contact that matters, and dormant until a specific input pattern appears.

That shape has a name in the literature, a logic-level bomb, and three parts you can point at in the drawing:

part	here
trigger	estop AND maint, an input pattern no operator asserts by accident
payload	bypass the interlock, energize the conveyor
dormancy	identical to the correct program until the pattern occurs

Eleven more benchmarks in this suite carry the same attack fitted to a different plant: a busbar, a batch reactor, a traffic junction, an elevator door. The plant changes and the shape does not.

Both routes reach this, eventually

Both programs now carry a verdict from the ladder front end and from the C route, which is what an independent check is supposed to look like: the same conclusion arrived at through Beremiz and MatIEC rather than through the front end under test.

Recorded 2026-08-27T19:19:07Z. Every build ran the same command.

runner/record_via_c.py benchmarks/manufacturing/g_conveyor_interlock/bomb.xml benchmarks/manufacturing/g_conveyor_interlock/props.yaml false --tool master=<path-to-esbmc>

which generates the C below and hands it to ESBMC as:

esbmc <generated>/harness.c -I $PLC_TOOLS/matiec/lib/C -I <generated> --unwind 10 --timeout 30s

Translated by Beremiz df4370c and MatIEC 7949c0b.

build	ESBMC	verdict	expected	outcome	cpu
master	8.4.0 d88a9fa4	VIOLATION	VIOLATION	correct	0.812 s

What ESBMC was given. The harness the adapter generated, with the property written over the variables MatIEC emitted.

#include "iec_std_lib.h"
#include "POUS.h"
#include "POUS.c"

int main(void) {
  G_CONVEYOR_INTERLOCK_BOMB_data__ d = {0};
  G_CONVEYOR_INTERLOCK_BOMB_init__(&d, 0);
  for (int scan = 0; scan < 8; scan++) {
    __SET_VAR(d., RUN_CMD, , nondet_bool());
    __SET_VAR(d., ESTOP, , nondet_bool());
    __SET_VAR(d., GUARD_OPEN, , nondet_bool());
    __SET_VAR(d., MAINT, , nondet_bool());
    G_CONVEYOR_INTERLOCK_BOMB_body__(&d);
    __ESBMC_assert(!(__GET_VAR(d.CONVEYOR,) && __GET_VAR(d.ESTOP,)), "P1");
  }
  return 0;
}

Counterexample. ESBMC's own output. A trace long enough to need it is elided in the middle, and the omission is marked and counted where it happens.

master

State 1 file <generated>/harness.c line 9 column 15 function main thread 0
----------------------------------------------------
  d.RUN_CMD.value = { .RUN_CMD={ .value=(unsigned char)main::$tmp::return_value$_nondet_bool$1?1!0&0#1, .flags=0 }, .ESTOP={ .value = 0 },
    .GUARD_OPEN={ .value = 0 }, .MAINT={ .value = 0 },
    .CONVEYOR={ .value = 0 }, .WARN={ .value = 0 } }

State 2 file <generated>/harness.c line 10 column 15 function main thread 0
----------------------------------------------------
  d.ESTOP.value = { .RUN_CMD=d.RUN_CMD, .ESTOP=1, .GUARD_OPEN=d.GUARD_OPEN, .MAINT=d.MAINT,
    .CONVEYOR=d.CONVEYOR, .WARN=d.WARN }

State 3 file <generated>/harness.c line 11 column 15 function main thread 0
----------------------------------------------------
  d.GUARD_OPEN.value = { .RUN_CMD=d.RUN_CMD, .ESTOP=d.ESTOP, .GUARD_OPEN=0, .MAINT=d.MAINT,
    .CONVEYOR=d.CONVEYOR, .WARN=d.WARN }

State 4 file <generated>/harness.c line 12 column 15 function main thread 0
----------------------------------------------------
  d.MAINT.value = { .RUN_CMD=d.RUN_CMD, .ESTOP=d.ESTOP, .GUARD_OPEN=d.GUARD_OPEN, .MAINT=1,
    .CONVEYOR=d.CONVEYOR, .WARN=d.WARN }

State 5 file <generated>/POUS.c line 17 column 13 function G_CONVEYOR_INTERLOCK_BOMB_body__ thread 0
----------------------------------------------------
  data__->CONVEYOR.value = { .RUN_CMD=d.RUN_CMD, .ESTOP=d.ESTOP, .GUARD_OPEN=d.GUARD_OPEN, .MAINT=d.MAINT,
    .CONVEYOR=(unsigned char)(d.GUARD_OPEN.value == 0 && (signed int)d.RUN_CMD.value != 0 && ((signed int)d.MAINT.value != 0 && (signed int)d.ESTOP.value != 0 || d.ESTOP.value == 0)), .WARN=d.WARN }

State 6 file <generated>/POUS.c line 18 column 13 function G_CONVEYOR_INTERLOCK_BOMB_body__ thread 0
----------------------------------------------------
  data__->WARN.value = { .RUN_CMD=d.RUN_CMD, .ESTOP=d.ESTOP, .GUARD_OPEN=d.GUARD_OPEN, .MAINT=d.MAINT,
    .CONVEYOR=d.CONVEYOR, .WARN=d.ESTOP.value }

State 7 file <generated>/harness.c line 14 column 5 function main thread 0
----------------------------------------------------
Violated property:
  file <generated>/harness.c line 14 column 5 function main
  P1
  !((_Bool)((signed int)d.CONVEYOR.value) && (_Bool)((signed int)d.ESTOP.value))


** Results:
<generated>/POUS.c, function G_CONVEYOR_INTERLOCK_BOMB_body__
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_body__.object-out-of-bounds.1]  line 17  dereference failure: Access to object out of bounds
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_body__.assertion.1]             line 17  dereference failure: Incorrect alignment when accessing data object
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_body__.object-out-of-bounds.2]  line 17  dereference failure: Access to object out of bounds
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_body__.assertion.2]             line 17  dereference failure: Incorrect alignment when accessing data object
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_body__.object-out-of-bounds.3]  line 18  dereference failure: Access to object out of bounds
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_body__.assertion.3]             line 18  dereference failure: Incorrect alignment when accessing data object
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_body__.object-out-of-bounds.4]  line 18  dereference failure: Access to object out of bounds
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_body__.assertion.4]             line 18  dereference failure: Incorrect alignment when accessing data object
<generated>/POUS.c, function G_CONVEYOR_INTERLOCK_BOMB_init__
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.object-out-of-bounds.1]  line  5  dereference failure: Access to object out of bounds
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.assertion.1]             line  5  dereference failure: Incorrect alignment when accessing data object
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.object-out-of-bounds.2]  line  6  dereference failure: Access to object out of bounds
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.assertion.2]             line  6  dereference failure: Incorrect alignment when accessing data object
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.object-out-of-bounds.3]  line  7  dereference failure: Access to object out of bounds
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.assertion.3]             line  7  dereference failure: Incorrect alignment when accessing data object
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.object-out-of-bounds.4]  line  8  dereference failure: Access to object out of bounds
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.assertion.4]             line  8  dereference failure: Incorrect alignment when accessing data object
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.object-out-of-bounds.5]  line  9  dereference failure: Access to object out of bounds
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.assertion.5]             line  9  dereference failure: Incorrect alignment when accessing data object
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.object-out-of-bounds.6]  line 10  dereference failure: Access to object out of bounds
  PASSED       [G_CONVEYOR_INTERLOCK_BOMB_init__.assertion.6]             line 10  dereference failure: Incorrect alignment when accessing data object
<generated>/harness.c, function main
  FAILED       [main.assertion.1]                                         line 14  P1

** 1 of 21 properties failed, 20 passed

Getting the second column took a detour worth recording. For a long time this page showed one column here, because Beremiz crashed while rendering this ladder:

File "PLCGenerator.py", line 1079, in FactorizePaths
    factorized_paths.sort()
TypeError: '<' not supported between instances of 'list' and 'str'

factorized_paths holds strings and lists at once and Python 3 declines to order the two, so the clean rung came through only because its branches are the same length, while this one sets a one-element branch beside a two-element branch and mixes the types in precisely the way that sort cannot handle.

The defect is a Python 3 porting bug in Beremiz rather than anything about the conveyor. It is filed as beremiz#83 with a fix in PR #84, and the record above names its Beremiz as commit df4370c, which is that branch. Until the PR lands, reproducing this column means building from it.

A benchmark suite that records what happened rather than what should have happened collects these, and occasionally gets to fix one.

What to take from this

The property did the work. It named a physical hazard, it was short enough to argue about, and it was strong enough that a deliberately hidden branch could not satisfy it. Nothing about the code review found this bomb; the requirement did.