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

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; all numbers, page and table references, Algorithm 1 lines, quotations and the case study checked against the text; corrected the Figure 2 caption quotation scope, the engineers credited as the authors’, the best dynamic score that is a mean, and three unmarked inferences; Verus forms are marked inference and rest on no Verus source, so they are unchecked.

source: Tu et al. (Midea AIRC, KUKA, SJTU, ZJU), arXiv:2608.18565v1, 19 Aug 2026; 14 pages, appendices A–E included. Pages below are the printed page numbers.

terms: a PLC (programmable logic controller) is the computer that runs a factory line; ST (Structured Text) is its textual programming language; a POU (program organization unit) is one function or function block of such a program. The paper is not about Verus or Rust. Every Verus form below is an inference.

what is measured, and what stays trusted

Nothing is proved. The paper measures how often LLM-written PLC logic passes checks the generator never saw, for four generation methods and seven models, on two task sets:

• function track: 117 single-POU tasks from the Agents4PLC benchmark, graded by a held-out judge that compiles with RuSTy and model-checks requirement-derived properties with PLCverif on nuXmv (§5.4, p.6)
• project-context track: 65 tasks over ten plants from Spec2Control, where the new logic must build and run inside an existing ST project, scored on three layers: compilation, assertions on the program text, and trace agreement with a hidden reference on a live runtime (§3, p.3; §5.4, p.6)

The headline claim: “Rather than stopping when the model judges its own output adequate, S EMA PLC declares a task complete only when logged external checks confirm it.” (Abstract, p.1)

Trusted, per the paper’s own description:

• the hidden reference implementations and the 607 judge properties, 43 of 117 tasks having been repaired by PLC engineers (§5.2) (Appendix A, p.12)
• the scoring scenarios: at most six per task (Appendix B, p.12)
• RuSTy, PLCverif, nuXmv and the runtime

Inference: the specification check is not external in the sense the compiler is. §4.3 (p.5) says it is “Encoded as checklist skill documents”, and Table S4 (p.14) lists it as “Agent’s own audit feedback”. The model runs the checklist on its own code. Only the compile and runtime verdicts come from a program that is not the model.

technique 1: the verification gate (completion is decided by logged checks, not by the agent)

what it is: a loop wrapper with one rule. The agent may not end a task. A gate ends it, and only when every required check has a verdict that (a) is in the tool-call log and (b) was produced after the last edit.

when to use: any agent loop where the agent can say “done” without having run the checker, or after changing the file once more. The paper’s motivation: “To make these checks binding, verification-gated iteration forbids the agent from terminating on its own judgment; when results indicate failure, absence, or an indeterminate outcome, it must repair or report incompletion.” (§1, p.2)

how it is done (Algorithm 1, p.4; inputs are requirement R, context X, required checks K with completion criteria, per-check retry limit r, interaction budget B):

1. ground and generate: Γ ← GROUND(X); L ← GENERATE(R, Γ); V ← ∅ (line 1). V is the verdict table.
2. while budget remains, for every check c in K that has no valid verdict in V, run it: (v, e_c) ← RUNCHECK(c, L) (lines 3–4). e_c is the log entry.
3. earned claims: store v only if the log entry confirms it; otherwise store unchecked (line 5).
4. if V meets the completion criteria, return (L, V) (line 7).
5. else collect F, the failed checks that still have retries left; if F is empty, return failure with V (lines 8–9).
6. repair from the log entries of the failed checks only: L′ ← REPAIR(L, {e_c | c ∈ F}) (line 10).
7. edit invalidation: if L′ differs from L, set V to empty, so every check reruns (line 11).
8. on budget exhaustion return failure with V (line 14).

§4.5 (p.5) names the three invariants and fixes r: “Bounded retries: each check allows at most r = 2 repair rounds, with retries(c) maintained by the harness.” and “Edit invalidation: any modification voids all prior verdicts and every check re-runs, so verdicts attach to exact bytes.” and “Earned claims: each outcome is a machine-readable sentinel cross-validated against the tool-call log, and an unlogged claim is downgraded to unchecked.”

The gate does not require perfection: “The gate demands not perfect scores but logged external evidence that matches the delivered bytes.” (§4.5, p.5) What the completion criteria are per track is not given in numbers anywhere in the paper.

The concrete delivery gate (Appendix D, p.14) admits a task only when three conditions hold:

1. the delivered file contains no located address literal (a test-injection artifact)
2. the delivered bytes hash-match the content of the last successful compilation whose input list included that file
3. the session log carries deployment and forced-input evidence

Verus form (inference; the paper has no Verus):

• K = {specification audit, verus run on the crate, tests of the executable code}
• earned claim: the harness, not the agent, parses the verifier’s own summary line from the logged process output; an agent message saying the proof passes counts as unchecked
• edit invalidation: store the hash of every source file with each verdict; any later write to a .rs file clears all verdicts, including the specification audit, because a requires or ensures clause may have changed
• the analogue of condition 1: the delivered file must contain no proof-skipping artifact. A scan for assume(, admit() and #[verifier::external_body] that the task did not allow plays the role of the address-literal scan
• the analogue of condition 2: hash the delivered crate and compare with the hash of the crate the last zero-error verus run read
• what does not carry over: a retry limit of 2 per check. Inference: Verus proof repair commonly takes more rounds than fixing one compile diagnostic, so r is a parameter to set from VL’s own data

evidence: the gate is never ablated alone. The closest measurements:

• bare versus full (Table 1, p.7; strict verified pass rate, denominator 117, “inconclusive and empty generations count as failure”): mean over seven models 55.3% bare, 72.6% full. Per model the gain is 8.5 points (MiniMax-M3, 60.7 to 69.2) to 33.3 points (DeepSeek-V4-Flash, 34.2 to 67.5). Bare removes skills and tools together, and the paper says so: “Because bare-versus-full conflates declarative knowledge with the verification loop, we attribute the gain to the harness as a whole; the layer ablation in RQ3 decomposes the loop.” (§6.1, p.7)
• against the strongest baseline, Agents4PLC: 72.6% versus 63.9% mean; on GPT-5.5, 82.1% versus AutoPLC’s 79.5% (Table 1, p.7)

where it fails or what it assumes:

• it gates on the agent’s own scenarios, not the scoring ones (§4.4, p.5); Inference: a wrong scenario passes a wrong program
• Inference: the runtime verdict does not attach to the delivered bytes. Appendix D (p.14) says “Runtime validation exercises an injected test copy while the delivered file stays untouched, so a gate guards the two from drifting apart.” The hash condition ties the delivered file to a compilation, and the log condition only shows that some deployment happened. So the sentence in §4.5 that the delivered program “is identical to the candidate that earned every reported pass” holds for compilation and is weaker for runtime
• cost: on the project track 34.1 requests per task versus 6.9 for Agents4PLC, range across models 16.4 to 60.4 (Table 6, p.9). “In S EMA PLC’s open-ended loop each tool call is a model decision and the gate keeps it interacting until the checks pass, so requests vary with the backbone (16.4 to 60.4) rather than by a preset loop count.” (§6.4, p.10)

technique 2: three check layers added in a fixed order, each feeding repair

what it is: specification audit, then compilation, then live runtime validation; each returns either pass or a concrete defect that becomes the repair prompt.

when to use: Inference: when cheap checks can remove the failures that would make the expensive check unrunnable. The paper fixes the order only in the Table 3 ablation, which adds the layers cumulatively.

how it is done (§4.3 and §4.4, p.5):

1. specification audit: check the candidate clause by clause against the natural-language requirement. It “covers every named device, signal, and published variable; threshold and boundary conditions; interlock, mutual-exclusion, and priority invariants; and scan-cycle state semantics.” Each item returns pass or a concrete revision.
2. compilation: return source line, error category and diagnostics, but pass on only one: “Feedback is the first diagnostic only, so repair stays local and avoids cascading rewrites.” The matching skill (Table S3, p.13) reads: “Repair the earliest diagnostic only, recheck, at most two rounds, then report stuck”.
3. runtime validation: build, deploy, initialize, inject scenario inputs, sample external variables, compare with assertions derived from the requirement or with a golden trace.
4. map the failure shape to a repair target: “a flat trace points to wiring, a changing but wrong trace to block logic, a late transition to a timer or edge detector.”
5. because sampling can miss short events: “Because traces are sampled rather than recorded every scan cycle, transient events are checked through persistent assertions.”

The paper’s worked case (Figure 2 and §6.3, p.8; coking-refinery plant, task “Section 8”): the requirement gives one setpoint two competing causes, low flow ⇒ 500 and transmitter fault ⇒ 2500. The intermediate SemaPLC candidate compiled and wired one constant, ManOut := 2500.0, for both. Forcing the flow input to 30 kg/hr gave expected 500, observed 2500. The repair selected the value by cause (IF Fault_Active THEN FFIC701_ManOut := 2500.0; ELSE FFIC701_ManOut := 500.0; END_IF;) and the rerun confirmed both cases. The Agents4PLC candidate had the mirror defect: a later independent IF overwrote the fault value. The caption warns that for Agents4PLC “the 500 result is inferred from source logic, not a runtime trace”.

Verus form (inference):

• layer order for VL: specification audit of requires/ensures against the requirement text, then cargo check-level compilation, then verus, then run the compiled code on scenarios
• first-diagnostic-only repair carries over directly: give the agent the first Verus error and its source span, not the whole list
• the runtime layer does not become redundant once Verus passes. Verus proves the code meets its ensures; the Figure 2 defect is a wrong priority between two requirement clauses, which a wrong ensures would encode faithfully. Running scenarios derived from the requirement text checks the specification, which the proof cannot
• the failure-shape table has a Verus counterpart that the paper does not give: precondition failure at a call site points to the caller, postcondition failure to the body or a missing loop invariant, a resource-limit failure to the proof’s structure

evidence: Table 3 (p.9), project track, DeepSeek-V4-Flash only, 65 tasks, checks added cumulatively. Columns are integrated compile rate, static score, dynamic score (all 0–100 over 65 tasks), mean tokens and mean model requests per task:

• none (generate only): 64.6, 71.5, 23.1, 34k, 8.9
• • spec: 70.8, 74.0, 30.3, 60k, 14.6
• • compile: 83.1, 77.8, 43.7, 74k, 25.5
• • runtime (full): 84.6, 78.0, 54.1, 129k, 47.8

The compile layer gives the largest dynamic gain (+13.4) because “non-building programs score 0 at runtime”; runtime adds +10.4; the specification audit +7.2 (difference computed here from the table). The paper’s own caveat: “the ablation is single-model.” (§6.3, p.8)

Table 4 (p.9) splits the same arms over 3,590 scenario–port value checks. From none to full: not built or run 33.4% to 3.3%; port missing 41.3% to 18.2%; wrong value 2.1% to 24.4%; correct 23.1% to 54.1%. The paper reads the rise in wrong values as coverage: “a check must run before it can be wrong, and an observed wrong value is exactly what runtime feedback repairs.” (§6.3, p.9)

where it fails:

• even the full harness leaves 45.9% of value checks failed on this model (Table 4)
• the order is cumulative only; no arm has runtime without the specification audit, so the layers’ separate effects are not known
• Inference: the 17.3% (limit breach) versus 7.1% (normal) wrong-value shares are shares of all 3,590 checks, not rates within each scenario kind. Each task has one normal scenario and one breach scenario per limited analog input (Appendix B, p.12), so breach checks are likely more numerous, and the paper’s reading that breach behavior “is hardest” is not established by these two numbers alone

technique 3: project grounding with bounded edits

what it is: before generating, retrieve the existing project’s structure, interfaces and declarations, and restrict the edit to the part the task targets.

when to use: when new code must build inside existing code.

how it is done (§4.2, pp.4–5): “On the project track, the agent retrieves the project structure and locates the relevant modules. It reuses existing variables and function blocks, avoids redefining established interfaces, and edits logic within a bounded scope, preserving project conventions rather than regenerating the whole project.” Figure 1 (p.1) shows the grounded context Γ as project tree, function-block interfaces and I/O summary. On the function track grounding “reduces to parsing the POU interface”. The paper gives no retrieval algorithm.

Verus form (inference): Γ for a Verus crate is the list of existing spec fn definitions, the requires/ensures of functions the new code will call, type invariants, and the lemmas (proof fn) already available. Bounded scope means the agent may not edit existing specifications to make its proof pass.

evidence: integrated compilation, Table 2 (p.7), 65-task denominator: SemaPLC mean 89.4 against 58.7 (LLM4PLC), 81.5 (AutoPLC), 71.2 (Agents4PLC); worst model 80.0 against 16.9, 58.4, 40.0. Grounding is not ablated; the attribution in §6.2 (p.7) is the authors’ explanation, not a measurement. On DeepSeek-V4-Pro, AutoPLC compiles more (95.4 versus 89.2).

technique 4: domain knowledge as documents and procedural skills

what it is: knowledge is kept outside the agent core in three kinds of files. “Domain knowledge lives in documents, not code: a rules file states the verification order, tool usage, and scan-cycle semantics; a curated wiki records function-block signatures, control patterns, and compiler pitfalls distilled by PLC developers from engineering practice; procedural skills script the multi-step checks.” (§4.2, p.5)

how it is done (Appendix D, pp.12–14):

1. one Markdown skill per check layer, loaded on demand: “Each skill states when it applies, what it may read, the ordered steps it prescribes, and the actions it forbids.”
2. every review skill forbids reading or guessing hidden artifacts and limits itself to the requirement text
3. the review checklist is ordered by defect class: “It walks contract extraction, coverage, boundary discipline, global invariants, behavioral fidelity, and scan-cycle semantics.”
4. coverage asks whether each named device has an instance, is called every scan, and whether every published variable has a driver; this “catches the dead output that compiles and then holds its initial value forever”
5. boundary discipline: “Boundary discipline forces an explicit choice between strict and non-strict comparison at each threshold and an explicit destination for the otherwise case.”
6. six domain axioms close the checklist, for example “Mutually exclusive commands may not be true together.”

Verus form (inference): the same checklist applied to a Verus specification asks: does every quantity named in the requirement appear in an ensures clause (coverage); is each bound < or <= on purpose, and is the else-branch result specified (boundary discipline); is there a state invariant that holds whatever the requirement says (the axioms). The dead-output defect has a Verus twin: an output the postcondition never mentions, which verifies with any value.

evidence: none separate from bare versus full (technique 1). Bare compile rates on the function track rise from an 85.5% mean to 99.2% (§6.1, p.7).

technique 5: scoring by layer, with hidden oracles validated on the reference

what it is: an evaluation design. The same program gets three independent scores, and each oracle is accepted only if the hidden reference passes it fully.

how it is done:

1. static oracle (Appendix B, p.12): for 63 of 65 tasks a parser extracts string and numeric literals from the corpus’s runtime tests and generates six assertion types on program text. “Only items that also occur in the hidden reference implementation become assertions, and every generated oracle must score full marks on that reference or it is rejected.” The other two tasks have hand-written oracles. 502 assertions in total, 1 to 20 per task, median 7.
2. dynamic oracle (§5.4, p.6; Appendix B, p.12): up to six scenarios per task: one normal, one per analog input with a configured limit, one that flips Boolean inputs. “Each scenario scores the fraction of core output ports whose traces agree with the reference’s, exactly for booleans and numerics; D is the mean scenario score.”
3. no task is dropped: “for the dynamic score, a compilation, deployment, timeout, or missing-trace failure on either side scores 0.”
4. function track (§3, p.3): pass means at least 0.80 of the properties verified, and “A property whose model check returns neither satisfied nor violated (unsupported constructs, translation failures, or timeouts) is inconclusive and counted as failure, and generation failures stay in the denominator.”
5. isolation is by file placement (Appendix E, p.14): “A workspace holds only the task inputs, such as the requirement, the interface catalog, and an empty target file, so the held-out judge, the assertion oracle, and the golden references and traces are absent from it.”

Verus form (inference): for a VL benchmark, hold out the reference specification and score an agent’s submission by (a) whether verus accepts it, (b) whether its specification implies the hidden one, (c) whether its executable agrees with a reference on scenarios. Count verifier timeouts as failures and keep failed generations in the denominator.

evidence that the layers differ: Table 2 means over seven models (p.7). Static: 75.7, 74.0, 71.7 for the three baselines and 81.6 for SemaPLC. Dynamic: 22.4, 31.4, 30.3 and 52.2. “Similar static scores therefore do not imply similar dynamic behavior: the runtime layer separates, and even reorders, methods that static scoring compresses.” (§6.3, p.8)

evidence that the formal judge has a blind spot: Table 5 (p.9), 1,293 delivered programs from SemaPLC runs. Programs without REAL or timer: 916 programs, 4,653 properties, 75.7% conclusive. With REAL: 345 programs, 1,845 properties, 87.0% conclusive. With a TON timer: 32 programs, 174 properties, 0.0% conclusive. “Timers are not unverifiable in principle, but in this pipeline the stateful timing constructs that span scan cycles fall outside conclusive coverage, and precisely these are what runtime validation exercises directly.” (§6.3, p.9)

where it fails: the static oracle is substring and constant matching on program text, so it measures similarity to the reference’s vocabulary, not behavior (inference from the six assertion types). Appendix E (p.14) limits the dynamic score itself: “Dynamic scores therefore measure behavior on the benchmark scenarios rather than generalization to unseen operating conditions.”

technique 6: three-round audit of a benchmark’s oracle

what it is: a procedure for repairing wrong properties in a published benchmark before using it.

the three rounds (Appendix A, p.12):

1. independent parallel reviews flag candidate defects
2. a second round re-derives every flag from scratch, “using brute-force truth tables for Boolean logic and step-by-step simulation for state machines”, and adds missed defects
3. a blind third round adjudicates disagreements
4. “Only defects confirmed by at least two rounds were repaired, and baseless properties were deleted rather than replaced by invented thresholds.”

The five defect classes found: “wrong constants or polarities, tautological assertions, properties that contradict the design, invented thresholds, and copy-paste duplicates.”

Verus form (inference): the same classes occur in benchmark specifications for Verus tasks. A tautological ensures is the direct counterpart of a tautological assertion, and VL’s own task specifications can be audited with the same three rounds. Brute-force truth tables correspond to testing a spec fn on all small inputs.

evidence: defects confirmed in 43 of 117 tasks; property count from 629 to 607 (Appendix A, p.12).

numbers that do not add up, and unexplained ones

• Appendix A says the audit “confirmed defects in 43 of the 117 tasks” and then that the released data “modifies 53 samples, 46 with repaired properties and 7 with completed task descriptions only”. 46 samples with repaired properties is more than 43 tasks with confirmed defects; the paper does not reconcile them. §5.2 (p.6) gives only 43.
• Table 5 pools 1,293 delivered programs. Seven models times 117 tasks is 819 for one configuration. The paper does not say which runs make up 1,293.
• The abstract’s “from 22.4 to 31.4 for the baselines against 52.2” are means over seven models. On GPT-5.5 the dynamic gap is 65.4 versus 63.6 (Agents4PLC), and SemaPLC’s static score there (84.1) is below all three baselines (86.3, 88.8, 88.6) (Table 2, p.7). The paper states this narrowing in §6.2 and §7.
• All checked sums hold: Table 1 means, the 8.8-point margin (72.64 − 63.86 before rounding), the bare spread 37.6, the full spread 14.6, Table 4’s 74.7 → 21.5 and 2.1 → 24.4, and the Table 5 program total.
• Time in Table 6 is a median and requests a mean, so the two columns are not the same statistic. Function-track time is 71 s versus 454 s for Agents4PLC, which the paper attributes to Agents4PLC running the model checker on each iteration (§6.4, p.10).

what VL should not redo

Inference:

• measuring that a compile-and-property-check loop beats bare generation; the bare versus full column already shows it on seven models
• building a multi-agent fixed pipeline as the baseline design: Agents4PLC’s request count is nearly constant (6.8 to 7.0 per task on the project track) and its dynamic score is 30.3 mean, so a fixed workflow buys predictability and loses on behavior
• the three gate invariants need no new design; Algorithm 1 is 14 lines and can be copied

What remains open in the paper and is VL’s to do: an ablation of the gate alone (edit invalidation and earned claims on or off), which the paper does not have.

threat level for VL (inference)

Inference: low as a competitor, useful as a design. The domain is PLC Structured Text, the guarantee is test agreement on at most six scenarios, and the paper’s own best mean dynamic score is 52.2 of 100 (65.4 on its best single model, GPT-5.5). It does not produce proofs. The finding that carries weight for VL is the opposite of a threat: with a formal judge in the loop (Agents4PLC runs PLCverif every iteration) behavior on a live runtime was still wrong more often than right (dynamic mean 30.3 of 100). The paper ties this to self-derived properties only for the function track (§6.1); on the project track, build failures also score 0 (Agents4PLC compiles 71.2% on average), so the cause is not isolated. A product that sells proofs must answer the same question about where its specifications come from.

techniques for the catalog

• verification gate — the harness, not the agent, ends a task, and only when every required check has a logged verdict produced after the last edit
• edit invalidation — any change to the candidate clears all stored verdicts so each verdict attaches to exact bytes
• earned claims — a pass counts only if the tool-call log holds the matching check result; otherwise it is recorded as unchecked
• delivery hash gate — the delivered file must hash-match the input of the last successful build and contain no test-injection artifact
• first-diagnostic-only repair — feed the agent only the earliest compiler diagnostic, with at most two repair rounds per check
• layered checks in cost order — specification audit, compile, then live execution, each failure becoming the next repair prompt
• failure-shape repair targeting — map the kind of runtime mismatch (flat, wrong, late) to the part of the program to repair
• defect-class specification checklist — audit code against the requirement by coverage, boundary strictness, otherwise-case, global invariants and domain axioms
• project grounding with bounded edits — retrieve existing interfaces and declarations first and forbid redefining them
• reference-validated hidden oracle — accept a generated test oracle only if the hidden reference scores full marks on it
• inconclusive-as-failure scoring — count verifier timeouts and unsupported results as failures and keep failed generations in the denominator
• three-round oracle audit — flag, re-derive from scratch, adjudicate blind, and repair only defects confirmed twice

Last edited: 2026-10-13