The guard that waits for the spindle¶

A milling spindle does not stop when its contactor drops. It coasts, for a second or two, and anybody who has opened a guard early has heard it. ISO 14119 handles that with guard locking: the door stays locked until the hazardous movement has actually stopped, which is a different moment from the one when the drive command goes away.

Update: released ESBMC 8.6.0

The runs on this page were recorded against the builds named beside them. For comparison, in the paper's evaluation (evidence/variants_302.csv in the release):

g_guard_lock: the released ESBMC 8.6.0 passes the ingestion gate and returns SAFE; 8.4.0 fails the gate.
The expected verdict is unchanged in every case.

Every machine in this part so far has been untimed. Lesson 7.2 said outright that the 0.5 s synchrony window it needed was not in the model, and lesson 7.3 pushed the dead time into an input. This one puts a real timer in the rung.

The rungs¶

The timer runs while the drive is off. Its output is the permission to release the lock, and OpenReq in series after it means the guard opens on a request, but only once the rundown has elapsed. The drive rung drops Motor the moment a request arrives, so the two are never on together whatever the timer does.

file	what it is	size	sha256
`program.xml`	ladder program, PLCopen XML	4.0 KB	`3ded357e988b`
`no_rundown.xml`	ladder program, PLCopen XML	2.7 KB	`0ee531ff14bd`
`props.yaml`	property file	0.2 KB	`1b331320d53f`
`rundown_check.props.yaml`	property file	0.5 KB	`f690a27115b8`

The property everyone writes¶

benchmarks/manufacturing/g_guard_lock/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!(Unlocked && Motor)"
    justification: "ISO 14119 guard locking: the guard is never released while the drive is energised."

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

cp benchmarks/manufacturing/g_guard_lock/program.xml benchmarks/manufacturing/g_guard_lock/program.ld
esbmc benchmarks/manufacturing/g_guard_lock/program.ld --ld-props benchmarks/manufacturing/g_guard_lock/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_guard_lock/program.xml benchmarks/manufacturing/g_guard_lock/program.ld
esbmc benchmarks/manufacturing/g_guard_lock/program.ld --ld-props benchmarks/manufacturing/g_guard_lock/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	fail	0.014 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 OpenReq=NONDET(_Bool);
        ASSIGN DoorClosed=NONDET(_Bool);
        ASSIGN RunCmd=NONDET(_Bool);
        ASSIGN Motor=1 && RunCmd && DoorClosed && !OpenReq;
        GOTO 1
     2:

Check the ingestion gate column before the verdict column. It passes, and the scan body carries Rundown__ET and Rundown__Q, so the timer reached the solver. That check is not ceremonial here: a front end that skipped the TON would leave Unlocked unassigned and prove this property about a program with the timer rung missing.

Now the variant with the timer deleted, where the guard releases on the request alone.

Predict the verdict

The rundown timer is gone and the door opens as soon as somebody asks. Does the guard still stay locked while the drive is energised?

Answer

build	verdict	expected	ingestion gate
v8.4	`SAFE`	`SAFE`	pass

It does, with the gate passing. OpenReq drops Motor in the same rung that raises Unlocked, so the two cannot coincide however impatient the release is. The property is about coincidence, and coasting is not coincidence.

The discriminator¶

benchmarks/manufacturing/g_guard_lock/rundown_check.props.yaml

# Discriminator, not a safety requirement. A spindle keeps turning after its contactor
# drops, so guard locking holds the door for the rundown time and a request does not
# open it at once. A program that proves this releases the guard on the request alone.
format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!OpenReq || Motor || Unlocked"
    justification: "A request with the drive already stopped always releases the guard. Guard locking must refute this."

Recorded 2026-08-28T18:37:08Z. Every build ran the same command.

cp benchmarks/manufacturing/g_guard_lock/program.xml benchmarks/manufacturing/g_guard_lock/program.ld
esbmc benchmarks/manufacturing/g_guard_lock/program.ld --ld-props benchmarks/manufacturing/g_guard_lock/rundown_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

Recorded 2026-08-28T18:37:08Z.

master

cp benchmarks/manufacturing/g_guard_lock/program.xml benchmarks/manufacturing/g_guard_lock/program.ld
esbmc benchmarks/manufacturing/g_guard_lock/program.ld --ld-props benchmarks/manufacturing/g_guard_lock/rundown_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
master	8.4.0 `0064c4ac`	`VIOLATION`	`VIOLATION`	correct	pass	0.012 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.

master

     1: IF !1 THEN GOTO 15
        ASSIGN OpenReq=NONDET(_Bool);
        ASSIGN DoorClosed=NONDET(_Bool);
        ASSIGN RunCmd=NONDET(_Bool);
        ASSIGN Motor__prev=1 && Motor;
        IF !1 THEN GOTO 2
        ASSIGN pf3=0;
     2: IF !(1 && !Motor__prev) THEN GOTO 3
        ASSIGN pf3=1;
     3: ASSIGN Rundown__IN=1 && pf3;
        IF !Rundown__IN THEN GOTO 5
        IF !(Rundown__ET < Rundown__PT) THEN GOTO 4
        ASSIGN Rundown__ET=Rundown__ET + 1;
     4: GOTO 6
     5: ASSIGN Rundown__ET=0;
     6: ASSIGN Rundown__Q=Rundown__IN && Rundown__ET >= Rundown__PT;
        IF !1 THEN GOTO 7
        ASSIGN pf6=0;
     7: IF !(1 && Rundown__Q && OpenReq) THEN GOTO 8
        ASSIGN pf6=1;
     8: ASSIGN Unlocked=1 && pf6;
        IF !1 THEN GOTO 9
        ASSIGN pf8=0;
     9: IF !(1 && RunCmd) THEN GOTO 10
        ASSIGN pf8=1;
    10: IF !1 THEN GOTO 11
        ASSIGN pf9=0;
    11: IF !(1 && pf8 && DoorClosed) THEN GOTO 12
        ASSIGN pf9=1;
    12: IF !1 THEN GOTO 13
        ASSIGN pf10=0;
    13: IF !(1 && pf9 && !OpenReq) THEN GOTO 14
        ASSIGN pf10=1;
    14: ASSIGN Motor=1 && pf10;
        GOTO 1
    15:

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  thread 0
----------------------------------------------------
  OpenReq = 1

State 2  thread 0
----------------------------------------------------
  DoorClosed = 0

State 3  thread 0
----------------------------------------------------
  RunCmd = 0

State 4  thread 0
----------------------------------------------------
  Motor = 0

State 5 file benchmarks/manufacturing/g_guard_lock/program.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/manufacturing/g_guard_lock/program.ld
  P1
  !OpenReq || Motor || Unlocked


** Results:
benchmarks/manufacturing/g_guard_lock/program.ld
  FAILED       [global.assertion.1]  line 0  P1

** 1 of 1 properties failed

Recorded 2026-08-28T18:37:08Z. Every build ran the same command.

cp benchmarks/manufacturing/g_guard_lock/no_rundown.xml benchmarks/manufacturing/g_guard_lock/no_rundown.ld
esbmc benchmarks/manufacturing/g_guard_lock/no_rundown.ld --ld-props benchmarks/manufacturing/g_guard_lock/rundown_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

Recorded 2026-08-28T18:37:08Z.

master

cp benchmarks/manufacturing/g_guard_lock/no_rundown.xml benchmarks/manufacturing/g_guard_lock/no_rundown.ld
esbmc benchmarks/manufacturing/g_guard_lock/no_rundown.ld --ld-props benchmarks/manufacturing/g_guard_lock/rundown_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
master	8.4.0 `0064c4ac`	`SAFE`	`SAFE`	correct	pass	0.016 s

master 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.

master

     1: IF !1 THEN GOTO 10
        ASSIGN OpenReq=NONDET(_Bool);
        ASSIGN DoorClosed=NONDET(_Bool);
        ASSIGN RunCmd=NONDET(_Bool);
        IF !1 THEN GOTO 2
        ASSIGN pf3=0;
     2: IF !(1 && OpenReq) THEN GOTO 3
        ASSIGN pf3=1;
     3: ASSIGN Unlocked=1 && pf3;
        IF !1 THEN GOTO 4
        ASSIGN pf8=0;
     4: IF !(1 && RunCmd) THEN GOTO 5
        ASSIGN pf8=1;
     5: IF !1 THEN GOTO 6
        ASSIGN pf9=0;
     6: IF !(1 && pf8 && DoorClosed) THEN GOTO 7
        ASSIGN pf9=1;
     7: IF !1 THEN GOTO 8
        ASSIGN pf10=0;
     8: IF !(1 && pf9 && !OpenReq) THEN GOTO 9
        ASSIGN pf10=1;
     9: ASSIGN Motor=1 && pf10;
        GOTO 1
    10:

Master refutes it on the timed guard and proves it on the untimed one, which is the pattern this part has been running since 7.1. What is new is the shape of the question. The other six discriminators asked whether a program remembers something. This one asks whether it waits.

What the timer costs¶

A timer is the most expensive thing in this part to verify, and the reason is visible in the scan body. Rundown__ET is an integer the solver has to reason about across scans, so the state space stops being a handful of booleans. The Structured Text twin makes the point plainly: through the C route it takes 41 seconds, against hundredths for every untimed machine in this part.

That cost is why a rundown interlock is a good thing to have a benchmark for. It is not exotic, it is on most guarded machines in the building, and it is exactly the shape of logic that a verifier is tempted to skip.