Bombs that wait¶
The bombs in Part 2 waited for an input. These wait for nothing at all. They count.
The fuse¶
tank_overflow is a pump and a high-level switch. The safety requirement is the one you
would write yourself: the pump must never run while the tank reads full.
format_version: "0.1"
properties:
- id: P1
kind: invariant
expression: "!(pump && level_high)"
justification: "Fill pump must never run while the tank is full (overflow / actuator-manipulation LLB)."
- id: P2
kind: reachability
expression: "pump && level_high"
justification: "Witness (trigger synthesis) for the VIOLATION variant: a trace to this state recovers the bomb's arming sequence."
Here is the bombed program in full. Read the three blocks in order.
(* --- LLB fuse: increments silently every scan --- *)
scan_cnt := scan_cnt + 1;
IF scan_cnt >= 50 THEN
armed := TRUE;
END_IF;
IF start AND NOT level_high THEN
pump := TRUE;
END_IF;
(* --- LLB payload: interlock is gated by NOT armed --- *)
IF level_high AND NOT armed THEN
pump := FALSE;
END_IF;
The interlock is still there. It is the third block, and it does exactly what the correct
program does, right up until armed becomes true. Until scan fifty, NOT armed is true,
the guard fires, and the pump stops on a full tank. The bombed program and the clean
program are indistinguishable, not approximately but exactly.
| file | what it is | size | sha256 |
|---|---|---|---|
clean.st |
structured text | 1.0 KB | 1b5041ae61be |
bomb.st |
structured text | 1.6 KB | ef027bbe3208 |
props.yaml |
property file | 0.4 KB | 7c5b5fad344d |
What a bounded check makes of it¶
The same program, the same property, the same build, twice. The only difference is how many scans the harness runs.
Eight scans¶
Recorded 2026-08-27T19:24:17Z. Every build ran the same command.
runner/record_via_c.py benchmarks/water_treatment/tank_overflow/bomb.st benchmarks/water_treatment/tank_overflow/props.yaml false --tool master=<path-to-esbmc>
which generates the C below and hands it to ESBMC as:
Translated by Beremiz df4370c and MatIEC 7949c0b.
| build | ESBMC | verdict | expected | outcome | cpu |
|---|---|---|---|---|---|
| master | 8.4.0 d88a9fa4 |
SAFE |
VIOLATION |
wrong | 0.799 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"
#define __LOCATED_VAR(type, name, ...) \
type name##__image; type *name = &name##__image;
#include "LOCATED_VARIABLES.h"
#undef __LOCATED_VAR
int main(void) {
TANK_data__ d = {0};
TANK_init__(&d, 0);
for (int scan = 0; scan < 8; scan++) {
__SET_LOCATED(d., LEVEL_HIGH, , nondet_bool());
__SET_LOCATED(d., START, , nondet_bool());
TANK_body__(&d);
__ESBMC_assert(!(__GET_LOCATED(d.PUMP,) && __GET_LOCATED(d.LEVEL_HIGH,)), "P1");
__ESBMC_assert(!(__GET_LOCATED(d.PUMP,) && __GET_LOCATED(d.LEVEL_HIGH,)), "P2");
}
return 0;
}
Sixty-four scans¶
Recorded 2026-08-28T18:39:22Z. Every build ran the same command.
runner/record_via_c.py benchmarks/water_treatment/tank_overflow/bomb.st benchmarks/water_treatment/tank_overflow/props.yaml false --tool master=<path-to-esbmc>
which generates the C below and hands it to ESBMC as:
Translated by Beremiz df4370c and MatIEC 7949c0b.
| build | ESBMC | verdict | expected | outcome | cpu |
|---|---|---|---|---|---|
| master | 8.4.0 0064c4ac |
VIOLATION |
VIOLATION |
correct | 0.843 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"
#define __LOCATED_VAR(type, name, ...) \
type name##__image; type *name = &name##__image;
#include "LOCATED_VARIABLES.h"
#undef __LOCATED_VAR
int main(void) {
TANK_data__ d = {0};
TANK_init__(&d, 0);
for (int scan = 0; scan < 64; scan++) {
__SET_LOCATED(d., LEVEL_HIGH, , nondet_bool());
__SET_LOCATED(d., START, , nondet_bool());
TANK_body__(&d);
__ESBMC_assert(!(__GET_LOCATED(d.PUMP,) && __GET_LOCATED(d.LEVEL_HIGH,)), "P1");
__ESBMC_assert(!(__GET_LOCATED(d.PUMP,) && __GET_LOCATED(d.LEVEL_HIGH,)), "P2");
}
return 0;
}
State 1 file <generated>/harness.c line 14 column 5 function main thread 0
----------------------------------------------------
*d.LEVEL_HIGH.value = 0 (00000000)
State 2 file <generated>/harness.c line 15 column 5 function main thread 0
----------------------------------------------------
*d.START.value = 0 (00000000)
State 4 file <generated>/harness.c line 14 column 5 function main thread 0
----------------------------------------------------
*d.LEVEL_HIGH.value = 0 (00000000)
State 5 file <generated>/harness.c line 15 column 5 function main thread 0
----------------------------------------------------
*d.START.value = 0 (00000000)
State 7 file <generated>/harness.c line 14 column 5 function main thread 0
----------------------------------------------------
*d.LEVEL_HIGH.value = 0 (00000000)
State 8 file <generated>/harness.c line 15 column 5 function main thread 0
----------------------------------------------------
*d.START.value = 1 (00000001)
State 10 file <generated>/harness.c line 14 column 5 function main thread 0
----------------------------------------------------
*d.LEVEL_HIGH.value = 0 (00000000)
State 11 file <generated>/harness.c line 15 column 5 function main thread 0
----------------------------------------------------
*d.START.value = 0 (00000000)
State 13 file <generated>/harness.c line 14 column 5 function main thread 0
----------------------------------------------------
*d.LEVEL_HIGH.value = 0 (00000000)
State 14 file <generated>/harness.c line 15 column 5 function main thread 0
----------------------------------------------------
*d.START.value = 0 (00000000)
State 16 file <generated>/harness.c line 14 column 5 function main thread 0
----------------------------------------------------
*d.LEVEL_HIGH.value = 1 (00000001)
State 17 file <generated>/harness.c line 15 column 5 function main thread 0
----------------------------------------------------
*d.START.value = 0 (00000000)
State 19 file <generated>/harness.c line 14 column 5 function main thread 0
----------------------------------------------------
*d.LEVEL_HIGH.value = 0 (00000000)
State 20 file <generated>/harness.c line 15 column 5 function main thread 0
----------------------------------------------------
*d.START.value = 0 (00000000)
State 22 file <generated>/harness.c line 14 column 5 function main thread 0
----------------------------------------------------
*d.LEVEL_HIGH.value = 0 (00000000)
... 352 lines omitted from the middle of the trace (475 lines in total) ...
State 155 file <generated>/harness.c line 15 column 5 function main thread 0
----------------------------------------------------
*d.START.value = 0 (00000000)
State 156 file <generated>/harness.c line 17 column 5 function main thread 0
----------------------------------------------------
Violated property:
file <generated>/harness.c line 17 column 5 function main
P1
!((_Bool)((signed int)(*d.PUMP.value)) && (_Bool)((signed int)(*d.LEVEL_HIGH.value)))
** Results:
<generated>/POUS.c, function TANK_body__
PASSED [TANK_body__.object-out-of-bounds.1] line 19 dereference failure: Access to object out of bounds
PASSED [TANK_body__.assertion.1] line 19 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_body__.object-out-of-bounds.2] line 19 dereference failure: Access to object out of bounds
PASSED [TANK_body__.assertion.2] line 19 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_body__.object-out-of-bounds.3] line 20 dereference failure: Access to object out of bounds
PASSED [TANK_body__.assertion.3] line 20 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_body__.object-out-of-bounds.4] line 21 dereference failure: Access to object out of bounds
PASSED [TANK_body__.assertion.4] line 21 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_body__.object-out-of-bounds.5] line 21 dereference failure: Access to object out of bounds
PASSED [TANK_body__.assertion.5] line 21 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_body__.object-out-of-bounds.6] line 23 dereference failure: Access to object out of bounds
PASSED [TANK_body__.assertion.6] line 23 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_body__.object-out-of-bounds.7] line 24 dereference failure: Access to object out of bounds
PASSED [TANK_body__.assertion.7] line 24 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_body__.object-out-of-bounds.8] line 26 dereference failure: Access to object out of bounds
PASSED [TANK_body__.assertion.8] line 26 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_body__.object-out-of-bounds.9] line 27 dereference failure: Access to object out of bounds
PASSED [TANK_body__.assertion.9] line 27 dereference failure: Incorrect alignment when accessing data object
<generated>/POUS.c, function TANK_init__
PASSED [TANK_init__.object-out-of-bounds.1] line 5 dereference failure: Access to object out of bounds
PASSED [TANK_init__.assertion.1] line 5 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_init__.object-out-of-bounds.2] line 6 dereference failure: Access to object out of bounds
PASSED [TANK_init__.assertion.2] line 6 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_init__.object-out-of-bounds.3] line 7 dereference failure: Access to object out of bounds
PASSED [TANK_init__.assertion.3] line 7 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_init__.object-out-of-bounds.4] line 8 dereference failure: Access to object out of bounds
PASSED [TANK_init__.assertion.4] line 8 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_init__.object-out-of-bounds.5] line 9 dereference failure: Access to object out of bounds
PASSED [TANK_init__.assertion.5] line 9 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_init__.object-out-of-bounds.6] line 10 dereference failure: Access to object out of bounds
PASSED [TANK_init__.assertion.6] line 10 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_init__.object-out-of-bounds.7] line 11 dereference failure: Access to object out of bounds
PASSED [TANK_init__.assertion.7] line 11 dereference failure: Incorrect alignment when accessing data object
PASSED [TANK_init__.object-out-of-bounds.8] line 12 dereference failure: Access to object out of bounds
PASSED [TANK_init__.assertion.8] line 12 dereference failure: Incorrect alignment when accessing data object
<generated>/harness.c, function main
PASSED [main.object-out-of-bounds.1] line 14 dereference failure: Access to object out of bounds
PASSED [main.assertion.1] line 14 dereference failure: Incorrect alignment when accessing data object
PASSED [main.object-out-of-bounds.2] line 15 dereference failure: Access to object out of bounds
PASSED [main.assertion.2] line 15 dereference failure: Incorrect alignment when accessing data object
FAILED [main.assertion.3] line 17 P1
PASSED [main.object-out-of-bounds.3] line 17 dereference failure: Access to object out of bounds
PASSED [main.assertion.4] line 17 dereference failure: Incorrect alignment when accessing data object
NOT CHECKED [main.assertion.5] line 18 P2
PASSED [main.object-out-of-bounds.4] line 18 dereference failure: Access to object out of bounds
PASSED [main.assertion.6] line 18 dereference failure: Incorrect alignment when accessing data object
sensor_forge, whose payload forges what the HMI reports rather than moving an actuator,
behaves identically: SAFE at eight scans, VIOLATION at sixty-four.
Why the first answer is not a bug¶
It is tempting to call the eight-scan SAFE a false negative and move on. It is worth being more careful than that, because the reason matters for how you use the tool.
The harness this route generates is a bounded loop:
That is a complete program that runs eight scans and stops. It genuinely never violates the property, and ESBMC's proof of that is correct. The bound is part of the model, not part of the analysis. Nothing was approximated and no search was truncated; a different program was verified, and it was verified soundly.
The ladder route behaves differently, and the difference is worth seeing. There the scan
loop is while (true), so a bound is genuinely a truncation of the search, and ESBMC says
so in its own output:
NOT CHECKED [global.assertion.1] line 0 unwinding assertion loop 1
** 1 of 2 properties failed, 1 not checked
An unwinding assertion is the tool telling you it stopped early. A for loop written to
eight offers nothing to report, because there is nothing left unexplored.
So the two routes fail differently. One tells you the search was cut short. The other quietly answers a smaller question, correctly.
Choosing a depth¶
The practical rule is unglamorous: read the program before you choose a bound.
One grep found the threshold. A depth of fifty-one scans reaches it, and everything below fifty is a question about a program nobody is running.
The bulk recorder in this suite does something cruder and worth naming as a stopgap: when
a variant expected to fail comes back SAFE, record_all.py --route via-c retries once at
sixty-four scans before believing the answer. That catches a fifty-scan fuse. It would not
catch a five-thousand-scan fuse, and an attacker who reads this page will pick five
thousand.
Which is the next lesson's problem.
What to take from this¶
A bounded answer is only as good as the bound, and the bound is a modeling decision you
made, not a property of the program you made it about. Write it down next to the verdict.
Every panel on this site prints the command that produced it for exactly this reason: the
--unwind and the scan count are part of the claim, and a verdict quoted without them is
not a result.