One-sentence Summary

Researchers from Midea AIRC, KUKA, SJTU, and ZJU propose SemaPLC, a project-grounded, verification-gated agent harness for PLC code generation that applies a strict completion rule requiring confirmed specification, compilation, and live-runtime checks, achieving a 72.6% mean strict pass rate on 117 independent-POU tasks and lifting dynamic behavior scores from 22.4 to 31.4 for baselines to 52.2 for SemaPLC.

Key Contributions

• SEMAPLC is a verification-gated agent harness for PLC code generation that grounds generation in an existing task or project and declares completion only after logged external checks for specification, compilation, and live-runtime behavior confirm the result.
• It contributes a project-context evaluation track with 65 tasks scored by integrated compilation, static assertion-based behavior, and dynamic golden-trace comparison on a live PLC runtime, where generated and reference logic are executed under scenario inputs.
• Across seven backbone models, SEMAPLC achieves the highest strict verified pass rate on the 117-task function track with a 72.6% mean, the best mean integrated compilation score of 89.4, and the best dynamic behavior score of 52.2 versus at most 31.4 for baselines. The results show that similar static scores can mask sharply different runtime behavior, so live execution is needed to separate reliable methods.

Introduction

Programmable logic controllers (PLCs) run factory lines, power plants, and water-treatment facilities, and they are commonly programmed in Structured Text from the IEC 61131-3 standard. Prior work shows that large language models can generate isolated PLC program organization units and improve them with compiler, formal verification, and execution feedback, but production logic must also integrate into an existing project and behave correctly at runtime. Earlier systems often demonstrate that generated code runs on limited cases rather than measuring runtime reliability at scale, and their benchmarks focus mostly on independent units or isolated requirements. The authors introduce SEMAPLC, a verification-gated agent harness that grounds generation in the target project and requires logged compilation, specification, and live runtime checks before completion, alongside a two-track evaluation that separately scores integrated compilation, static behavior, and dynamic behavior.

Dataset

The authors use two task sets for evaluation.

Function track

• Composition: 117 independent-POU tasks from the Agents4PLC benchmark.
• Repair/filtering: the released oracle contained defective verification properties and task descriptions that fail correct implementations. PLC engineers audited and repaired 43 of the 117 affected tasks.
• Usage: all methods are evaluated on the identical repaired data.

Project-context track

• Composition: 65 tasks derived from Spec2Control, based on ten industrial plants with reviewed control narratives converted to IEC 61131-3 ST projects.
• Task schema: each task targets one plant section and provides the section narrative, the function-block interface catalog and library, and an empty entry harness. Generated logic must compile and deploy within the full project.
• Leakage control: reference implementations, runtime traces, and original answers remain hidden. A leakage audit found no verbatim copying.

Processing and data use

• The excerpt does not specify training split, mixture ratios, cropping strategy, or metadata construction details.
• The datasets function as evaluation benchmarks: repaired tasks in the function track and hidden-reference project-level tasks in the project-context track.

Method

The authors formulate the PLC code generation task across two tracks: a function track, where the system produces a Program Organization Unit (POU) $L_f = G(R_f, I_f)$Lf​=G(Rf​,If​) given a requirement $R_f$Rf​ and local interface $I_f$If​, and a project-context track, where it generates new logic $L_p = G(R_p, P)$Lp​=G(Rp​,P) integrated into an existing project $P$P. To operationalize this, the authors introduce the SemaPLC agent harness, which accepts a natural-language control requirement $R$R and task context $X$X.

The harness is built upon a generic event-driven tool-use core that contains no PLC-specific logic. On top of this core, the system organizes five key components: an agent core for planning and editing, project and task grounding, a PLC skill library, verification processes, and a verification gate.

As illustrated in the framework diagram, the agent core acts through a shared PLC MCP tool layer, which exposes tools for syntax checking, compilation, deployment, runtime status, live variable reading, trace sampling, and scripted behavior checks. The harness accepts the control requirement and context, allowing the agent core to plan, generate, edit, and repair the logic. External verification results from specification checks, compilation, and live runtime validation are fed into the verification gate, which accepts the implementation only when track-specific completion criteria are met. Failed checks generate diagnostic feedback for repair iterations, provided retries and budget remain.

For project grounding, the agent retrieves the project structure and locates relevant modules on the project track. It reuses existing variables and function blocks, avoiding redefinition of established interfaces and preserving project conventions. Domain knowledge is encapsulated in documents rather than code, including a rules file for verification order and scan-cycle semantics, a curated wiki for function-block signatures and control patterns, and procedural skills for multi-step checks.

The authors employ a multi-source verification approach. Specification results are derived from a structured requirement audit that checks the candidate clause by clause against the natural-language requirement, covering devices, signals, thresholds, and interlocks. Compilation results check syntax, types, symbols, and interfaces, returning the first diagnostic to keep repairs local. Live runtime validation builds and deploys the implementation, initializes the runtime, injects scenario inputs, and samples external variables. It compares observed behavior against runtime assertions or a golden trace. Mismatches and execution failures become diagnostic feedback, targeting specific failure stages such as wiring, block logic, or timer behavior.

The verification-gated iteration loop is governed by three invariants to ensure delivery integrity. First, bounded retries limit each check to at most $r = 2$r=2 repair rounds. Second, edit invalidation ensures that any modification voids all prior verdicts, requiring every check to re-run so that verdicts attach to exact bytes. Third, earned claims require each outcome to be a machine-readable sentinel cross-validated against the tool-call log, downgrading any unlogged claim to unchecked. Together, these invariants guarantee that the delivered program is identical to the candidate that earned every reported pass.

Experiment

The study evaluates SEMAPLC against three established baselines across seven backbone models on both function-level and project-grounded PLC generation. The function-level results show that the harness improves strict correctness for every model and acts as a model-agnostic reliability layer, while the project-level results show the largest gains in dynamic runtime behavior, though the advantage narrows on the strongest model. Verification layer analysis indicates that live runtime validation is the most discriminative check and that each added verification layer converts previously unrunnable checks into measurable and repairable behavior. The main tradeoff is interaction cost, since the reliability gains come from additional model-driven verification and execution loops rather than from generation alone.

The full SEMAPLC harness achieves the highest strict verified pass rates across all listed models, with a clear average lead over the strongest baseline. Comparing bare and full configurations shows the harness improves every backbone, with the largest gains for weaker models and a much narrower score spread. The improvement comes from checks beyond compilation, especially specification auditing and live runtime validation, which catch semantic mismatches before delivery. SEMAPLC full records the top strict pass rate on every model shown, outperforming all baselines by a substantial margin. Every model improves from bare to full configuration, and the weakest backbones gain the most while the cross-model spread shrinks. The bare-to-full gain is attributed to the harness verification loop, especially specification and runtime checks that repair semantic errors before delivery.

On the project-context track, SEMAPLC leads the baselines across integrated compilation, static behavior, and live-runtime dynamic behavior, with the widest advantage in dynamic performance. The runtime layer is the most discriminative: baselines have similar static scores but spread widely on dynamic scores and remain far below SEMAPLC. SEMAPLC also shows the smallest static-to-dynamic drop, though every method's dynamic score stays well below its static score. SEMAPLC achieves the highest mean integrated compilation rate and the highest mean static score among the compared methods. Dynamic behavior is the most discriminative layer; baseline static scores cluster closely, but their dynamic scores spread widely and stay far behind SEMAPLC. SEMAPLC's dynamic score never falls below 30, while baseline methods fall to single digits on their worst models, and SEMAPLC has the smallest static-to-dynamic drop.

Adding verification layers cumulatively raises the dynamic score from 23.1 to 54.1, while the static score moves only from 71.5 to 78.0. Compilation provides the largest single dynamic gain, followed by runtime validation, but each layer increases token and request costs, with runtime validation the most expensive step. Dynamic performance improves monotonically as specification, compilation, and runtime checks are added, while static performance changes only modestly. Token and request costs climb with every verification layer, and full runtime validation is the most expensive stage.

Adding specification, compilation, and runtime checks gradually raises correct outcomes and reduces structural failures. Because more checks become runnable, wrong-value outcomes also increase, especially in limit-breach scenarios, reflecting broader coverage rather than degradation. Correct outcomes rise from 23.1% to 54.1% as structural failures fall from 74.7% to 21.5% across the cumulative layers. Wrong-value outcomes concentrate in harder limit-breach conditions, reaching 17.3% compared with 7.1% under normal operation once runtime checks are active.

Formal verification coverage is strong for delivered programs that do not use timers, with programs involving REAL constructs reaching the highest conclusive rate. Timer-bearing programs are the clear gap: none of their properties reached a conclusive verdict in this pipeline. This leaves stateful timing behavior outside formal coverage and motivates direct runtime validation. Programs without REAL or timer constructs show mostly conclusive formal coverage, and programs with REAL constructs achieve an even higher conclusive share. Timer-bearing programs have no conclusive verification outcomes, with all timer-related properties remaining inconclusive. The formal pipeline handles many non-timer cases but does not reach conclusive results for timing constructs that span scan cycles.

The experiments evaluate SEMAPLC through strict pass-rate comparisons, project-context integrated and dynamic behavior benchmarks, cumulative verification-layer ablations, outcome analysis, and formal coverage assessment. The full harness improves every backbone, with the largest gains for weaker models, and leads most clearly on dynamic runtime behavior, which is the most discriminative layer. Adding specification, compilation, and runtime checks raises correct dynamic outcomes from 23.1% to 54.1% mainly by converting structural failures into runnable cases, though runtime validation is the most expensive step. Formal verification handles many non-timer and REAL programs conclusively but leaves timer-bearing constructs inconclusive, motivating direct runtime validation.