A lockout that lets go¶
A gas burner lights in a fixed order, and EN 298 fixes it: run the fan long enough to sweep the chamber, open the pilot, prove the flame, and only then admit main gas. Get the order wrong and you are igniting a chamber that has been filling with fuel.
The second requirement is about what happens after a failure. A burner that fails to light must go to lockout, and lockout is non-volatile: it needs somebody to walk up and press reset. A controller that retries on its own is doing unsupervised ignition attempts on a chamber that has already proved it will not light.
The rungs¶
Lockout := (Lockout OR FlameFail) AND NOT ResetBtn, Pilot := CallForHeat AND PurgeDone
AND NOT Lockout, MainValve := CallForHeat AND PurgeDone AND FlameProven AND NOT Lockout.
| file | what it is | size | sha256 |
|---|---|---|---|
program.xml |
ladder program, PLCopen XML | 4.8 KB | 8d5a0314b1d6 |
self_clearing.xml |
ladder program, PLCopen XML | 4.6 KB | e9618b8c237c |
props.yaml |
property file | 0.2 KB | 0d8c0bb4baa6 |
lockout_check.props.yaml |
property file | 0.4 KB | d95e72df20cc |
The property everyone writes¶
format_version: "0.1"
properties:
- id: P1
kind: invariant
expression: "!MainValve || (PurgeDone && FlameProven)"
justification: "EN 298 light-off order: the main gas valve opens only after the purge has completed and the flame is proven."
Recorded 2026-09-04T23:40:46Z. Every build ran the same command.
cp benchmarks/hvac/g_burner_purge/program.xml benchmarks/hvac/g_burner_purge/program.ld
esbmc benchmarks/hvac/g_burner_purge/program.ld --ld-props benchmarks/hvac/g_burner_purge/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s
Recorded 2026-09-04T23:40:46Z.
| build | ESBMC | verdict | expected | outcome | ingestion gate | cpu |
|---|---|---|---|---|---|---|
| v8.4 | 8.4.0 | SAFE |
SAFE |
correct | pass | 0.018 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.
1: IF !1 THEN GOTO 2
ASSIGN CallForHeat=NONDET(_Bool);
ASSIGN PurgeDone=NONDET(_Bool);
ASSIGN FlameProven=NONDET(_Bool);
ASSIGN FlameFail=NONDET(_Bool);
ASSIGN ResetBtn=NONDET(_Bool);
ASSIGN MainValve=1 && CallForHeat && PurgeDone && FlameProven && !Lockout;
ASSIGN Pilot=1 && CallForHeat && PurgeDone && !Lockout;
ASSIGN Lockout=1 && Lockout && !ResetBtn;
ASSIGN Lockout=1 && FlameFail && !ResetBtn;
ASSIGN Fan=1 && CallForHeat;
GOTO 1
2:
That is the light-off order, and it is the property a commissioning engineer would ask for. It says nothing whatever about lockout, so a controller with no lockout at all satisfies it.
Predict the verdict
In this variant the lockout follows the flame-fault contact and clears itself. Does the light-off order still hold?
Answer
| build | verdict | expected | ingestion gate |
|---|---|---|---|
| v8.4 | SAFE |
SAFE |
pass |
The discriminator¶
# Discriminator, not a safety requirement. A burner lockout is non-volatile and needs a
# manual reset, so it outlives the flame fault that caused it. A lockout that clears
# itself proves this property and lets the burner retry unattended.
format_version: "0.1"
properties:
- id: P1
kind: invariant
expression: "!Lockout || FlameFail"
justification: "Lockout holds only while the flame fault is present. A latching lockout must refute this."
Recorded 2026-08-28T18:37:07Z. Every build ran the same command.
cp benchmarks/hvac/g_burner_purge/program.xml benchmarks/hvac/g_burner_purge/program.ld
esbmc benchmarks/hvac/g_burner_purge/program.ld --ld-props benchmarks/hvac/g_burner_purge/lockout_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:07Z.
| build | ESBMC | verdict | expected | outcome | ingestion gate | cpu |
|---|---|---|---|---|---|---|
| master | 8.4.0 0064c4ac |
VIOLATION |
VIOLATION |
correct | pass | 0.015 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 25
ASSIGN CallForHeat=NONDET(_Bool);
ASSIGN PurgeDone=NONDET(_Bool);
ASSIGN FlameProven=NONDET(_Bool);
ASSIGN FlameFail=NONDET(_Bool);
ASSIGN ResetBtn=NONDET(_Bool);
ASSIGN Lockout__prev=1 && Lockout;
IF !1 THEN GOTO 2
ASSIGN pf13=0;
2: IF !(1 && CallForHeat) THEN GOTO 3
ASSIGN pf13=1;
3: IF !1 THEN GOTO 4
ASSIGN pf14=0;
4: IF !(1 && pf13 && PurgeDone) THEN GOTO 5
ASSIGN pf14=1;
5: IF !1 THEN GOTO 6
ASSIGN pf15=0;
6: IF !(1 && pf14 && FlameProven) THEN GOTO 7
ASSIGN pf15=1;
7: IF !1 THEN GOTO 8
ASSIGN pf16=0;
8: IF !(1 && pf15 && !Lockout__prev) THEN GOTO 9
ASSIGN pf16=1;
9: ASSIGN MainValve=1 && pf16;
IF !1 THEN GOTO 10
ASSIGN pf9=0;
10: IF !(1 && CallForHeat) THEN GOTO 11
ASSIGN pf9=1;
11: IF !1 THEN GOTO 12
ASSIGN pf10=0;
12: IF !(1 && pf9 && PurgeDone) THEN GOTO 13
ASSIGN pf10=1;
13: IF !1 THEN GOTO 14
ASSIGN pf11=0;
14: IF !(1 && pf10 && !Lockout__prev) THEN GOTO 15
ASSIGN pf11=1;
15: ASSIGN Pilot=1 && pf11;
IF !1 THEN GOTO 16
ASSIGN pf6=0;
16: IF !(1 && FlameFail) THEN GOTO 17
ASSIGN pf6=1;
17: IF !1 THEN GOTO 18
ASSIGN pf5=0;
18: IF !(1 && Lockout__prev) THEN GOTO 19
ASSIGN pf5=1;
19: IF !1 THEN GOTO 20
ASSIGN pf7=0;
20: IF !(1 && pf6 && !ResetBtn) THEN GOTO 21
ASSIGN pf7=1;
21: IF !(1 && pf5 && !ResetBtn) THEN GOTO 22
ASSIGN pf7=1;
22: ASSIGN Lockout=1 && pf7;
IF !1 THEN GOTO 23
ASSIGN pf3=0;
23: IF !(1 && CallForHeat) THEN GOTO 24
ASSIGN pf3=1;
24: ASSIGN Fan=1 && pf3;
GOTO 1
25:
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
----------------------------------------------------
FlameFail = 1
State 2 thread 0
----------------------------------------------------
ResetBtn = 0
State 3 thread 0
----------------------------------------------------
Lockout = 1
State 5 thread 0
----------------------------------------------------
FlameFail = 0
State 6 thread 0
----------------------------------------------------
ResetBtn = 0
State 7 thread 0
----------------------------------------------------
Lockout__prev = 1
State 8 thread 0
----------------------------------------------------
Lockout = 1
State 9 file benchmarks/hvac/g_burner_purge/program.ld thread 0
----------------------------------------------------
Violated property:
file benchmarks/hvac/g_burner_purge/program.ld
P1
!Lockout || FlameFail
** Results:
NOT CHECKED [global.assertion.1] line 0 unwinding assertion loop 1
benchmarks/hvac/g_burner_purge/program.ld
FAILED [global.assertion.2] line 0 P1
** 1 of 2 properties failed, 1 not checked
(this mode stops at the first violation; use --multi-property for a verdict on every property)
Refuted, which is the right answer: a latching lockout outlives the fault that set it. A
front end that flattened the two branches into Lockout would prove this instead, soundly,
about a lockout that is a plain copy of FlameFail AND NOT ResetBtn.
Recorded 2026-08-28T18:37:07Z. Every build ran the same command.
cp benchmarks/hvac/g_burner_purge/self_clearing.xml benchmarks/hvac/g_burner_purge/self_clearing.ld
esbmc benchmarks/hvac/g_burner_purge/self_clearing.ld --ld-props benchmarks/hvac/g_burner_purge/lockout_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:07Z.
| build | ESBMC | verdict | expected | outcome | ingestion gate | cpu |
|---|---|---|---|---|---|---|
| master | 8.4.0 0064c4ac |
SAFE |
SAFE |
correct | pass | 0.017 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 22
ASSIGN CallForHeat=NONDET(_Bool);
ASSIGN PurgeDone=NONDET(_Bool);
ASSIGN FlameProven=NONDET(_Bool);
ASSIGN FlameFail=NONDET(_Bool);
ASSIGN ResetBtn=NONDET(_Bool);
ASSIGN Lockout__prev=1 && Lockout;
IF !1 THEN GOTO 2
ASSIGN pf12=0;
2: IF !(1 && CallForHeat) THEN GOTO 3
ASSIGN pf12=1;
3: IF !1 THEN GOTO 4
ASSIGN pf13=0;
4: IF !(1 && pf12 && PurgeDone) THEN GOTO 5
ASSIGN pf13=1;
5: IF !1 THEN GOTO 6
ASSIGN pf14=0;
6: IF !(1 && pf13 && FlameProven) THEN GOTO 7
ASSIGN pf14=1;
7: IF !1 THEN GOTO 8
ASSIGN pf15=0;
8: IF !(1 && pf14 && !Lockout__prev) THEN GOTO 9
ASSIGN pf15=1;
9: ASSIGN MainValve=1 && pf15;
IF !1 THEN GOTO 10
ASSIGN pf5=0;
10: IF !(1 && FlameFail) THEN GOTO 11
ASSIGN pf5=1;
11: IF !1 THEN GOTO 12
ASSIGN pf6=0;
12: IF !(1 && pf5 && !ResetBtn) THEN GOTO 13
ASSIGN pf6=1;
13: ASSIGN Lockout=1 && pf6;
IF !1 THEN GOTO 14
ASSIGN pf3=0;
14: IF !(1 && CallForHeat) THEN GOTO 15
ASSIGN pf3=1;
15: ASSIGN Fan=1 && pf3;
IF !1 THEN GOTO 16
ASSIGN pf8=0;
16: IF !(1 && CallForHeat) THEN GOTO 17
ASSIGN pf8=1;
17: IF !1 THEN GOTO 18
ASSIGN pf9=0;
18: IF !(1 && pf8 && PurgeDone) THEN GOTO 19
ASSIGN pf9=1;
19: IF !1 THEN GOTO 20
ASSIGN pf10=0;
20: IF !(1 && pf9 && !Lockout__prev) THEN GOTO 21
ASSIGN pf10=1;
21: ASSIGN Pilot=1 && pf10;
GOTO 1
22:
Two lockouts, one verdict¶
Put the four runs together. The property that was actually shipped, the light-off order,
says SAFE for the burner that latches and SAFE for the burner that does not. A results
table built from it would report a working lockout in both rows.
The pattern is worth naming because it generalizes past this benchmark. Wherever a requirement reduces to "this memory outlives its cause", the check for it is a refutation, and both a program without the memory and a front end that quietly drops it will pass anything weaker.