A reversing starter, proved and broken¶
A reversing starter is one motor with two contactors. KM_CW closes to turn it
clockwise, KM_CCW counter-clockwise. Close both at once and you short two supply
phases straight through the reversing contacts, so the interlock here is wiring
protection rather than a process preference. Nobody gets a second chance to test it
on real switchgear.
The rung¶
KM_CW := fwd AND NOT rev, KM_CCW := rev. Rung 1 carries the interlock. Its normally-closed rev contact drops KM_CW the
moment reverse is asked for, and rung 2 needs no guard of its own because rung 1
already breaks the pair.
The extension is load-bearing
The file is called interlock.ld and its content is PLCopen XML. ESBMC's LD
front end keys off the extension, then XML-parses what it finds. Rename the file
to interlock.xml and the front end rejects it. Hand it a textual LD DSL and it
rejects that too.
| file | what it is | size | sha256 |
|---|---|---|---|
interlock.ld |
ladder program, PLCopen XML | 3.4 KB | 1bfbce455e3d |
interlock_bug.ld |
ladder program, PLCopen XML | 2.9 KB | 8be3a4bdabe0 |
props.yaml |
property file | 0.2 KB | 581b8bafc892 |
demo/interlock.ld (ladder program, PLCopen XML, 3.4 KB)
<?xml version="1.0" encoding="utf-8"?>
<!-- Reversing starter: ONE motor, TWO contactors.
KM_CW closes to run the motor clockwise
KM_CCW closes to run it counter-clockwise (anticlockwise)
Closing both at once shorts two supply phases through the reversing
contacts, so the interlock below is a wiring-protection requirement,
not a process preference.
Rung 1: KM_CW := fwd AND NOT rev (fwd contact, then a normally
closed rev contact, driving the KM_CW coil)
Rung 2: KM_CCW := rev
-->
<project xmlns="http://www.plcopen.org/xml/tc6_0200">
<fileHeader companyName="Demo" productName="Demo" productVersion="1" creationDateTime="2026-08-26T00:00:00" />
<contentHeader name="interlock">
<coordinateInfo><fbd><scaling x="1" y="1" /></fbd><ld><scaling x="1" y="1" /></ld><sfc><scaling x="1" y="1" /></sfc></coordinateInfo>
</contentHeader>
<types>
<dataTypes />
<pous>
<pou name="drive" pouType="program">
<interface>
<inputVars>
<variable name="fwd"><type><BOOL /></type></variable>
<variable name="rev"><type><BOOL /></type></variable>
</inputVars>
<outputVars>
<variable name="KM_CW"><type><BOOL /></type></variable>
<variable name="KM_CCW"><type><BOOL /></type></variable>
</outputVars>
</interface>
<body>
<LD>
<leftPowerRail localId="0">
<position x="0" y="0" /><connectionPointOut formalParameter="none" />
</leftPowerRail>
<!-- Rung 1 -->
<contact localId="10" negated="false" storage="none" edge="none">
<position x="20" y="10" />
<connectionPointIn><connection refLocalId="0" /></connectionPointIn>
<connectionPointOut /><variable>fwd</variable>
</contact>
<contact localId="11" negated="true" storage="none" edge="none">
<position x="40" y="10" />
<connectionPointIn><connection refLocalId="10" /></connectionPointIn>
<connectionPointOut /><variable>rev</variable>
</contact>
<coil localId="12" negated="false" storage="none">
<position x="60" y="10" />
<connectionPointIn><connection refLocalId="11" /></connectionPointIn>
<connectionPointOut /><variable>KM_CW</variable>
</coil>
<!-- Rung 2 -->
<contact localId="20" negated="false" storage="none" edge="none">
<position x="20" y="30" />
<connectionPointIn><connection refLocalId="0" /></connectionPointIn>
<connectionPointOut /><variable>rev</variable>
</contact>
<coil localId="21" negated="false" storage="none">
<position x="60" y="30" />
<connectionPointIn><connection refLocalId="20" /></connectionPointIn>
<connectionPointOut /><variable>KM_CCW</variable>
</coil>
<rightPowerRail localId="2147483646">
<position x="80" y="0" /><connectionPointIn />
</rightPowerRail>
</LD>
</body>
</pou>
</pous>
</types>
<instances><configurations><configuration name="Config0"><resource name="Res0">
<task name="tcyclic" interval="T#10ms" priority="0">
<pouInstance name="inst0" typeName="drive" />
</task>
</resource></configuration></configurations></instances>
</project>
The property¶
properties:
- id: P1
kind: mutual_exclusion
variables: [KM_CW, KM_CCW]
justification: "Both contactors must never close together: that shorts two supply phases across the reversing contacts."
mutual_exclusion takes a variable list and nothing else. The justification is not
decoration: it is the line a reviewer reads to decide whether this property is the
right one for that hazard.
Proving it¶
Recorded 2026-08-28T18:37:08Z. Every build ran the same command.
esbmc demo/interlock.ld --ld-props demo/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:08Z.
| 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.
1: IF !1 THEN GOTO 8
ASSIGN fwd=NONDET(_Bool);
ASSIGN rev=NONDET(_Bool);
IF !1 THEN GOTO 2
ASSIGN pf10=0;
2: IF !(1 && fwd) THEN GOTO 3
ASSIGN pf10=1;
3: IF !1 THEN GOTO 4
ASSIGN pf11=0;
4: IF !(1 && pf10 && !rev) THEN GOTO 5
ASSIGN pf11=1;
5: ASSIGN KM_CW=1 && pf11;
IF !1 THEN GOTO 6
ASSIGN pf20=0;
6: IF !(1 && rev) THEN GOTO 7
ASSIGN pf20=1;
7: ASSIGN KM_CCW=1 && pf20;
GOTO 1
8:
k-induction is the mode for a program you expect to be safe. It proves the property for every scan rather than for the first twenty, and the line naming the inductive step at k = 2 is what tells you the proof closed.
Breaking it¶
interlock_bug.ld is the same file with one element deleted. The |/| contact on
rev is gone from rung 1, so KM_CW := fwd, and nothing stops both contactors
closing.
Recorded 2026-08-28T18:37:08Z. Every build ran the same command.
esbmc demo/interlock_bug.ld --ld-props demo/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:08Z.
| 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.
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.
State 1 thread 0
----------------------------------------------------
fwd = 1
State 2 thread 0
----------------------------------------------------
rev = 1
State 3 thread 0
----------------------------------------------------
KM_CCW = 1
State 4 thread 0
----------------------------------------------------
KM_CW = 1
State 5 file demo/interlock_bug.ld thread 0
----------------------------------------------------
Violated property:
file demo/interlock_bug.ld
P1
!(KM_CW && KM_CCW)
** Results:
demo/interlock_bug.ld
FAILED [global.assertion.1] line 0 P1
** 1 of 1 properties failed
Read the trace in order. Both fwd and rev come up true in one scan, KM_CCW
follows rev, KM_CW follows fwd with nothing to block it, and the property fails
on the pair. Twelve milliseconds, one scan, one short circuit.
What the front end encoded¶
Read the tab above. The front end builds a guarded accumulator, pf10, sets it to 1 only
when the branch conducts, and then assigns KM_CW=1 && pf10. On this rung that is just a
longhand spelling of KM_CW = fwd, because only one path runs through it. Put two paths in
parallel and the accumulator stops being ceremony and starts deciding the verdict. Lesson
1.2 is where it does.
Watch the ingestion gate column as well. It reports whether the property's variables were assigned anywhere inside the scan loop. A front end that drops a body silently leaves an empty loop behind, and an empty loop satisfies every safety property you can write. The gate is what separates a proof from a shrug.
Try it yourself¶
Open interlock.ld, find the <contact negated="true"> element whose variable is
rev, and delete it. You have just written interlock_bug.ld. Or leave the program
alone and rewrite the property as kind: invariant with
expression: "!(KM_CW && KM_CCW)", which says the same thing in C operators and is
accepted, while the IEC spelling of that same formula, NOT (KM_CW AND KM_CCW), is
rejected by the property parser.
Reproducing has the commands.