Paper Explainer: SemaPLC — The Agent That Isn't Allowed to Say "Done"

Most work on LLM-generated factory control code stops at showing that the code can run. SemaPLC forbids the agent from declaring completion until logged external checks confirm it, lifting live-runtime behavior from a baseline ceiling of 31.4 to 52.2.

SemaPLC: A Project-Grounded, Verification-Gated Agent Harness for PLC Code Generation

Letting an AI write the code that runs a factory

A PLC (Programmable Logic Controller) is the box that actually runs a production line, a power plant, or a water-treatment facility (§1). Spin the pump, throttle back when flow drops, fail to the safe side when a fault appears — those decisions run in a loop for as long as the power is on.

The programs are written under the IEC 61131-3 standard, whose textual dialect is Structured Text (ST). It looks a lot like Pascal, which makes it convenient for an LLM to produce. A body of work already exists on generating a single POU (Program Organization Unit — one building block of a program, such as a function block), with compiler errors fed back for repair, model checkers applied, and multi-agent loops tried (§2).

But control logic in the field is not a self-contained part. It has to land inside an existing project, reuse the variables, types, and function blocks already there, honor the build and initialization conventions of that project — and then behave correctly, with the right timing, once the power is on. The paper names these two demands project grounding and correct runtime behavior (§1).

An analogy: the electrician who says "looks right" vs. the one who powers it up

The core of this paper is, technically, a single unglamorous idea: the agent is not permitted to declare its own completion.

Suppose you had a control panel wired. One electrician compares it to the drawing and says "looks right." The other buzzes out continuity, actually energizes the panel, watches it run, shows you the recording, and only then says "finished." The wiring may look identical. Only the second one hands you external evidence.

SemaPLC mechanizes the second electrician. It does not stop when the model judges its own output adequate; a task is complete only when logged external checks confirm it (Abstract). Those checks come in three kinds: an audit against the specification, compilation, and behavior on a live runtime. The tooling itself is conventional — existing compilers, model checkers, a runtime — and what the authors claim as new is how those tools are turned into a constraint (§1).

"Demonstrated" is not "measured"

The paper's charge against prior work is literally a section heading — Demonstrated, not measured (§1). Existing systems execute the generated code to show that it can run, which is not the same as measuring how reliably it runs. So the authors ship a method and the measurement to test it together.

What gets measured: three properties of the same program

On the function track (standalone POUs), a POU $L_f$ is generated from a requirement $R_f$ and an interface $I_f$, and a held-out judge — which no method may query — model-checks properties derived from $R_f$. With $V_f$ the fraction of properties verified satisfied:

Here $\mathbb{1}[\cdot]$ returns 1 when the bracketed condition holds and 0 otherwise. So equation (1) says only this: a candidate passes only when at least 80% of the requirement-derived properties are verified as satisfied. The 0.80 threshold follows prior work (Agents4PLC), and any property whose model check returns neither satisfied nor violated — unsupported constructs, translation failures, timeouts — is inconclusive, and counted as a failure (§3).

The project-context track is closer to the plant floor. New logic $L_p$ is dropped into an existing project $P$, giving an integrated program $P' = P \oplus L_p$, scored by three separate metrics (§3):

$$C(P')\in\{0,1\},\qquad S(P',R_p)\in[0,100],\qquad D(P',\mathcal{T})\in[0,100]$$

$C$ is a binary "did the integrated program build." $S$ is the percentage of requirement-derived assertions satisfied by the program text, checked without executing it. $D$ deploys to a live runtime, injects scenario inputs $\mathcal{T}$, and scores how far the observed traces agree with a hidden reference implementation's. In order: does it assemble, does it read correctly, and does it actually behave correctly under power. These three are distinct properties of the same program — that is the paper's starting premise (§1).

Formal verification has places where it goes silent

Why insist on a live runtime? Model checking of PLC code — exhaustively exploring reachable states — is long established, but the paper is explicit about its limits: it gives strong guarantees for supported, formalized properties, while TON timers or large state spaces can yield unsupported or inconclusive results in practice (§2). Every additional bit of state doubles what must be explored, so "large state space" arrives sooner than intuition suggests.

The verification gate: no self-reported completion

The heart of the harness (the framework that wraps execution) is three invariants (§4.5).

Bounded retries. Each check allows at most $r=2$ repair rounds. The agent cannot grind forever.

Edit invalidation. Change a single character of code and every prior verdict is discarded; all checks re-run. A verdict attaches not to "the program" but to those exact bytes.

Earned claims. Each outcome is emitted as a machine-readable sentinel and cross-validated against the tool-call log. An unlogged claim is downgraded to unchecked.

Together these give what the paper calls delivery integrity: the delivered program is identical to the candidate that earned every reported pass, and no self-reported pass survives without a tool log (§4.5). Appendix D makes the delivery gate concrete — the delivered bytes must hash-match the content of the last successful compilation, and the session log must carry deployment and forced-input evidence. What the gate demands is not a perfect score but recorded external evidence tied to the bytes you shipped. Termination conditions in general are covered in LLM Agents: The Basics; SemaPLC is the version where that decision has been moved entirely outside the model.