A seal-in latch, where the verdict hides the encoding

The seal-in latch is the second circuit every PLC course teaches. It is also where a verdict starts lying to you.

The rung

Run := (Start OR Run) AND NOT EStop. The coil's own output feeds back through the lower branch. Press Start, release it, and the motor keeps running until EStop opens the path. In PLCopen XML that junction is two <connection> elements inside one <connectionPointIn>, which is a wired OR.

file	what it is	size	sha256
sealin.ld	ladder program, PLCopen XML	3.1 KB	8cda4284cf9e
props.yaml	property file	0.2 KB	5d67454ec625
latch_check.props.yaml	property file	0.3 KB	98128be44265

demo2/sealin.ld (ladder program, PLCopen XML, 3.1 KB)

<?xml version="1.0" encoding="utf-8"?>
<!-- Motor start/stop with seal-in (latching) and an emergency stop.
     Run := (Start OR Run) AND NOT EStop

     Two parallel branches feed one junction: a Start contact and a Run
     contact. The Run contact carries the coil's own output back in, which
     is the seal-in. A normally closed EStop contact sits after the junction,
     so it breaks both branches at once.
-->
<project xmlns="http://www.plcopen.org/xml/tc6_0200">
  <fileHeader companyName="Demo" productName="Demo" productVersion="1" creationDateTime="2026-08-26T00:00:00" />
  <contentHeader name="sealin"><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="Start"><type><BOOL /></type></variable>
            <variable name="EStop"><type><BOOL /></type></variable>
          </inputVars>
          <outputVars>
            <variable name="Run"><type><BOOL /></type></variable>
          </outputVars>
        </interface>
        <body>
          <LD>
            <leftPowerRail localId="0">
              <position x="0" y="0" /><connectionPointOut formalParameter="none" />
            </leftPowerRail>
            <!-- branch 1: Start -->
            <contact localId="10" negated="false" storage="none" edge="none">
              <position x="20" y="10" />
              <connectionPointIn><connection refLocalId="0" /></connectionPointIn>
              <connectionPointOut /><variable>Start</variable>
            </contact>
            <!-- branch 2: the seal-in, Run feeding back -->
            <contact localId="11" negated="false" storage="none" edge="none">
              <position x="20" y="30" />
              <connectionPointIn><connection refLocalId="0" /></connectionPointIn>
              <connectionPointOut /><variable>Run</variable>
            </contact>
            <!-- OR junction merges both branches into the EStop contact -->
            <contact localId="12" negated="true" storage="none" edge="none">
              <position x="45" y="10" />
              <connectionPointIn>
                <connection refLocalId="10" />
                <connection refLocalId="11" />
              </connectionPointIn>
              <connectionPointOut /><variable>EStop</variable>
            </contact>
            <coil localId="13" negated="false" storage="none">
              <position x="70" y="10" />
              <connectionPointIn><connection refLocalId="12" /></connectionPointIn>
              <connectionPointOut /><variable>Run</variable>
            </coil>
            <rightPowerRail localId="2147483646">
              <position x="90" 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 obvious property

demo2/props.yaml

properties:
  - id: P1
    kind: invariant
    expression: "!(Run && EStop)"
    justification: "The motor must never run while the emergency stop is pressed."

The motor must never run while the emergency stop is pressed.

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

esbmc demo2/sealin.ld --ld-props demo2/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

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

master

esbmc demo2/sealin.ld --ld-props demo2/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 9
        ASSIGN Start=NONDET(_Bool);
        ASSIGN EStop=NONDET(_Bool);
        ASSIGN Run__prev=1 && Run;
        IF !1 THEN GOTO 2
        ASSIGN pf11=0;
     2: IF !(1 && Run__prev) THEN GOTO 3
        ASSIGN pf11=1;
     3: IF !1 THEN GOTO 4
        ASSIGN pf10=0;
     4: IF !(1 && Start) THEN GOTO 5
        ASSIGN pf10=1;
     5: IF !1 THEN GOTO 6
        ASSIGN pf12=0;
     6: IF !(1 && pf11 && !EStop) THEN GOTO 7
        ASSIGN pf12=1;
     7: IF !(1 && pf10 && !EStop) THEN GOTO 8
        ASSIGN pf12=1;
     8: ASSIGN Run=1 && pf12;
        GOTO 1
     9:

Proved at k = 2, in under a hundredth of a second. A results table would stop here and it would be misleading.

The discriminator

Look at the scan body above before reading on.

The front end builds pf12 out of both branches and reads Run__prev, a snapshot taken at the top of the scan, which gives Run := (Run_prev OR Start) AND NOT EStop. That is a latch, and you can see that it is a latch.

Now notice what the property could not have told you. !(Run && EStop) is satisfied by that encoding, by a plain conjunction with no memory in it, and by a program that never assigns Run at all. A property of this shape cannot separate a latch from a program that merely never runs the motor while the stop is pressed, so the verdict is compatible with a front end that dropped the self-hold branch entirely and never told you.

To make that difference a verdict rather than an inspection, ask for something only a real latch refutes. Can Run hold once Start is released?

demo2/latch_check.props.yaml

# Discriminator, not a safety requirement. A genuine seal-in latches, so Run can
# hold while Start is released, which VIOLATES this. A tool that proves it has
# encoded no latch at all.
properties:
  - id: P1
    kind: invariant
    expression: "!Run || Start"
    justification: "Run implies Start. A real seal-in must refute this."

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

esbmc demo2/sealin.ld --ld-props demo2/latch_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

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

master

esbmc demo2/sealin.ld --ld-props demo2/latch_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.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.

master

     1: IF !1 THEN GOTO 9
        ASSIGN Start=NONDET(_Bool);
        ASSIGN EStop=NONDET(_Bool);
        ASSIGN Run__prev=1 && Run;
        IF !1 THEN GOTO 2
        ASSIGN pf11=0;
     2: IF !(1 && Run__prev) THEN GOTO 3
        ASSIGN pf11=1;
     3: IF !1 THEN GOTO 4
        ASSIGN pf10=0;
     4: IF !(1 && Start) THEN GOTO 5
        ASSIGN pf10=1;
     5: IF !1 THEN GOTO 6
        ASSIGN pf12=0;
     6: IF !(1 && pf11 && !EStop) THEN GOTO 7
        ASSIGN pf12=1;
     7: IF !(1 && pf10 && !EStop) THEN GOTO 8
        ASSIGN pf12=1;
     8: ASSIGN Run=1 && pf12;
        GOTO 1
     9:

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
----------------------------------------------------
  Start = 1

State 2  thread 0
----------------------------------------------------
  EStop = 0

State 3  thread 0
----------------------------------------------------
  Run = 1

State 5  thread 0
----------------------------------------------------
  Start = 0

State 6  thread 0
----------------------------------------------------
  EStop = 0

State 7  thread 0
----------------------------------------------------
  Run__prev = 1

State 8  thread 0
----------------------------------------------------
  Run = 1

State 9 file demo2/sealin.ld thread 0
----------------------------------------------------
Violated property:
  file demo2/sealin.ld
  P1
  !Run || Start


** Results:
  NOT CHECKED  [global.assertion.1]  line 0  unwinding assertion loop 1
demo2/sealin.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)

Read the outcome column before the verdict. The expected result is VIOLATION, because a working seal-in has to be able to hold Run with Start back at 0, and the counterexample is the seal-in doing its job. States 1 to 3 are the first scan, with Start = 1 and EStop = 0 driving Run to 1. States 5 to 9 are the next scan, and Start has gone back to 0. Run__prev carries the 1 across the scan boundary, Run stays up, and the property falls over.

A front end that had flattened the rung would answer this one SAFE, and the SAFE would be sound about the program it built. That is the useful property of a discriminator: it does not ask the tool to be honest about its own limitations, it asks a question whose answer differs depending on what the tool actually encoded.

Why the run uses k-induction

record.py --mode kinduction forces it. Under incremental BMC a missing latch comes back unknown rather than SAFE, which is a far weaker statement: no counterexample within twenty unwindings, and nothing said about the twenty-first. On a discriminator you want the proof, because the point is to make the absence of the latch provable rather than merely unwitnessed.

Why this matters for the suite

The safety verdict was SAFE and the benchmark is named for a latch, and nothing about that verdict established that a latch was ever encoded. The property was insensitive to the one feature the task is named for.

That is the argument for publishing the encoding beside the label, and it sets a bar for any task named after a feature: the recorded evidence has to show the front end encoded the feature, not merely that a tool returned the verdict the task expected.

The bar is not hypothetical. Lesson 7.9 is a benchmark that fails it today, where the front end returns a confident verdict about a function block whose body never reached the scan loop.