Both buttons held, and the press stays up¶
A power press with two palm buttons a shoulder's width apart. Hold both and the ram comes down. Let either one go and it stops. The reasoning is old and simple: while both hands are on the buttons, neither is in the die.
ISO 13851 grades these devices. A Type I control is the plain conjunction of the two signals. Types II and III add anti-tie-down, which is the requirement that both actuators be released together before a new cycle can start, so that taping one down buys the operator nothing.
The rungs¶
BothOff := NOT LH AND NOT RH, Armed := (Armed OR BothOff) AND NOT Stroke,
Stroke := (Stroke OR Armed) AND LH AND RH. Armed is the memory of a release. It
comes up when both buttons are off, and the
stroke rung consumes it. Once a cycle has started, nothing rearms the press until the
operator takes both hands off, which is the behavior the standard is asking for.
| file | what it is | size | sha256 |
|---|---|---|---|
program.xml |
ladder program, PLCopen XML | 3.9 KB | 01ffc81a68d2 |
type_i.xml |
ladder program, PLCopen XML | 3.0 KB | 40e1b1f2e89c |
props.yaml |
property file | 0.2 KB | 01c905820f28 |
tiedown_check.props.yaml |
property file | 0.5 KB | d1118ab8f733 |
The property everyone writes¶
format_version: "0.1"
properties:
- id: P1
kind: invariant
expression: "!Stroke || (LH && RH)"
justification: "ISO 13851 requires the ram to descend only while both actuators are held. Releasing either one stops the stroke."
The ram descends only while both actuators are held. That is the sentence in the risk assessment, and the checker proves it.
Recorded 2026-09-04T23:40:48Z. Every build ran the same command.
cp benchmarks/manufacturing/g_two_hand/program.xml benchmarks/manufacturing/g_two_hand/program.ld
esbmc benchmarks/manufacturing/g_two_hand/program.ld --ld-props benchmarks/manufacturing/g_two_hand/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s
Recorded 2026-09-04T23:40:48Z.
| build | ESBMC | verdict | expected | outcome | ingestion gate | cpu |
|---|---|---|---|---|---|---|
| v8.4 | 8.4.0 | SAFE |
SAFE |
correct | pass | 0.016 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.
In the Type I variant the stroke rung reads Stroke := LH AND RH and no longer looks at
Armed at all, so nothing in the program remembers a release.
Predict the verdict
This is the device you can defeat with a strip of tape. Does the property above still hold?
Answer
| build | verdict | expected | ingestion gate |
|---|---|---|---|
| v8.4 | SAFE |
SAFE |
pass |
Of course it does. Stroke is literally the conjunction, so the implication is trivial.
The property is true of the device the standard classifies as defeatable, and it is true
for a stronger reason than it is true of the good one.
The discriminator¶
Tape changes nothing about the signals. It only changes how they got there. So ask the question tape cannot survive: does holding both buttons always produce a stroke?
# Discriminator, not a safety requirement. Taping one actuator down leaves both signals
# high, which is exactly the state this property says must produce a stroke. A Type II
# device refutes it: after a tie-down there was no both-released, so it stays armed off.
format_version: "0.1"
properties:
- id: P1
kind: invariant
expression: "!(LH && RH) || Stroke"
justification: "Both actuators held always produces a stroke. A Type II device with anti-tie-down must refute this."
Recorded 2026-08-28T18:37:10Z. Every build ran the same command.
cp benchmarks/manufacturing/g_two_hand/program.xml benchmarks/manufacturing/g_two_hand/program.ld
esbmc benchmarks/manufacturing/g_two_hand/program.ld --ld-props benchmarks/manufacturing/g_two_hand/tiedown_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:10Z.
| 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.
1: IF !1 THEN GOTO 22
ASSIGN LH=NONDET(_Bool);
ASSIGN RH=NONDET(_Bool);
ASSIGN Armed__prev=1 && Armed;
ASSIGN BothOff__prev=1 && BothOff;
ASSIGN Stroke__prev=1 && Stroke;
IF !1 THEN GOTO 2
ASSIGN pf10=0;
2: IF !(1 && Stroke__prev) THEN GOTO 3
ASSIGN pf10=1;
3: IF !1 THEN GOTO 4
ASSIGN pf11=0;
4: IF !(1 && Armed__prev) THEN GOTO 5
ASSIGN pf11=1;
5: IF !1 THEN GOTO 6
ASSIGN pf12=0;
6: IF !(1 && pf10 && LH) THEN GOTO 7
ASSIGN pf12=1;
7: IF !(1 && pf11 && LH) THEN GOTO 8
ASSIGN pf12=1;
8: IF !1 THEN GOTO 9
ASSIGN pf13=0;
9: IF !(1 && pf12 && RH) THEN GOTO 10
ASSIGN pf13=1;
10: ASSIGN Stroke=1 && pf13;
IF !1 THEN GOTO 11
ASSIGN pf7=0;
11: IF !(1 && BothOff__prev) THEN GOTO 12
ASSIGN pf7=1;
12: IF !1 THEN GOTO 13
ASSIGN pf6=0;
13: IF !(1 && Armed__prev) THEN GOTO 14
ASSIGN pf6=1;
14: IF !1 THEN GOTO 15
ASSIGN pf8=0;
15: IF !(1 && pf7 && !Stroke__prev) THEN GOTO 16
ASSIGN pf8=1;
16: IF !(1 && pf6 && !Stroke__prev) THEN GOTO 17
ASSIGN pf8=1;
17: ASSIGN Armed=1 && pf8;
IF !1 THEN GOTO 18
ASSIGN pf3=0;
18: IF !(1 && !LH) THEN GOTO 19
ASSIGN pf3=1;
19: IF !1 THEN GOTO 20
ASSIGN pf4=0;
20: IF !(1 && pf3 && !RH) THEN GOTO 21
ASSIGN pf4=1;
21: ASSIGN BothOff=1 && pf4;
GOTO 1
22:
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
----------------------------------------------------
LH = 1
State 2 thread 0
----------------------------------------------------
RH = 1
State 3 file benchmarks/manufacturing/g_two_hand/program.ld thread 0
----------------------------------------------------
Violated property:
file benchmarks/manufacturing/g_two_hand/program.ld
P1
!(LH && RH) || Stroke
** Results:
benchmarks/manufacturing/g_two_hand/program.ld
FAILED [global.assertion.1] line 0 P1
** 1 of 1 properties failed
LH = 1, RH = 1, and the press stays up. That trace is the tie-down attempt: both
signals present, no release behind them, and a Type II device declining to run.
Recorded 2026-08-28T18:37:10Z. Every build ran the same command.
cp benchmarks/manufacturing/g_two_hand/type_i.xml benchmarks/manufacturing/g_two_hand/type_i.ld
esbmc benchmarks/manufacturing/g_two_hand/type_i.ld --ld-props benchmarks/manufacturing/g_two_hand/tiedown_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:10Z.
| 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 12
ASSIGN LH=NONDET(_Bool);
ASSIGN RH=NONDET(_Bool);
ASSIGN BothOff__prev=1 && BothOff;
IF !1 THEN GOTO 2
ASSIGN pf8=0;
2: IF !(1 && LH) THEN GOTO 3
ASSIGN pf8=1;
3: IF !1 THEN GOTO 4
ASSIGN pf9=0;
4: IF !(1 && pf8 && RH) THEN GOTO 5
ASSIGN pf9=1;
5: ASSIGN Stroke=1 && pf9;
IF !1 THEN GOTO 6
ASSIGN pf6=0;
6: IF !(1 && BothOff__prev) THEN GOTO 7
ASSIGN pf6=1;
7: ASSIGN Armed=1 && pf6;
IF !1 THEN GOTO 8
ASSIGN pf3=0;
8: IF !(1 && !LH) THEN GOTO 9
ASSIGN pf3=1;
9: IF !1 THEN GOTO 10
ASSIGN pf4=0;
10: IF !(1 && pf3 && !RH) THEN GOTO 11
ASSIGN pf4=1;
11: ASSIGN BothOff=1 && pf4;
GOTO 1
12:
The Type I device proves the property at k = 2, which is the formal statement of "both signals high is sufficient", and therefore of "tape is sufficient".
What the model does not carry¶
ISO 13851 also requires the two actuations to fall within 0.5 s of each other. Nothing above expresses that, because the scan model here has no clock in it and the property language speaks only about the current scan. The synchrony requirement is real and this benchmark does not check it.
Worth being blunt about a second gap. A two-hand control that a risk assessment counts on is wired to a safety relay, not to standard PLC inputs, because the relay is what gives the redundancy and diagnostic coverage the performance level needs. What is verified here is the program's logic, which is one layer of the argument and not the argument.