PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Tengfei Zhou, Yifan Zhou, Dasheng Yang, Xiaofeng Mou, Hui Zhang, Yi Xu

arXiv:2608.18565v1cs.SE

TL;DR

PLC code generation has been evaluated mainly on isolated units and limited integration or runtime tests. SemaPLC grounds generation in existing projects and gates completion on external specification, compilation, and live-runtime checks, achieving the best strict verified pass rate across models and sharply stronger dynamic behavior.

  • Problem

    Existing evaluations provide limited evidence of how reliably generated PLC logic integrates into projects and behaves at runtime across methods and models.

  • Method

    SemaPLC uses project-grounded generation and verification-gated iteration, requiring logged external specification, compilation, and live-runtime checks before completion.

  • Results

    72.6% mean strict verified pass rate was achieved across seven models, alongside the best integrated compilation and dynamic behavior means on project-context tasks.

  • Takeaways & Limitations

    Runtime execution is necessary to distinguish reliable PLC-generation methods because similar static scores can conceal sharply different dynamic behavior.

  • Takeaways & Limitations

    Formal verification provided no conclusive verdict for timer-bearing programs, leaving stateful timing constructs to runtime validation in this pipeline.

Abstract

from arXiv · show

Programmable logic controllers (PLCs) run industrial plants, and large language models can already generate independent program organization units (POUs) for them. Whether such logic integrates into an existing PLC project and then runs correctly has been checked only in limited tests. We present \textsc{SemaPLC}, a project-grounded and verification-gated agent harness assembled from conventional tools but governed by a strict completion rule. Rather than stopping when the model judges its own output adequate, \textsc{SemaPLC} declares a task complete only when logged external checks confirm it. Those checks cover the specification, the compilation, and the behavior on a live runtime. On 117 independent-POU tasks matching existing benchmarks, it attains the highest strict verified pass rate on all seven models (72.6\% mean). On a project-context track of 65 tasks whose generated logic must compile and run inside a real project, it attains the highest mean on integrated compilation, static behavior, and dynamic behavior. Of the three layers, dynamic behavior is the most revealing. We measure it by deploying the generated and the reference logic to a live PLC runtime and comparing their executed traces. All methods fall within 10 static points of one another, whereas dynamic scores separate them sharply, from 22.4 to 31.4 for the baselines against 52.2 for \textsc{SemaPLC}. Overall, our verification-gated harness raises the mean at every layer and most sharply at runtime. Execution, not static scoring, is the faithful test of whether generated control logic actually works. \textsc{SemaPLC} is open-sourced at https://github.com/midea-ai/SemaPLC.

1 Introduction

SemaPLC addresses the gap between isolated PLC code generation and reliable deployment by grounding generation in project context and requiring logged external verification through live runtime validation. Its two-track evaluation shows that static evaluation can miss sharp differences in runtime reliability.

  • Motivation: PLC logic must integrate with established projects, respecting existing modules, variables, interfaces, build conventions, initialization, reset, and safety requirements.Compilation and static checks alone can still miss runtime misconfiguration.
  • Findings: Static evaluation can make methods appear similar even when their runtime reliability differs sharply, so stopping before execution cannot distinguish reliable methods from unreliable ones.SemaPLC achieves the best dynamic behavior with every model, although its lead narrows on the strongest models.
  • Method: SemaPLC combines project-grounded generation with specification checks, compilation, and live runtime validation as binding completion evidence.Termination requires logged external verification results, edits void prior verdicts, and claimed passes are cross-checked against tool logs.
  • Evaluation: The function track supports fair comparison on independent-POU benchmarks, while the project-context track measures integrated compilation, static behavior, and dynamic behavior separately.The project-context evaluation requires generated logic to adapt to and execute within established industrial projects.

2 Related Work

Prior work spans LLM-based PLC code generation, general agentic code repair, and formal or runtime PLC validation. SemaPLC adapts these directions to project-grounded, continuously executing PLC programs.

  • LLM-based PLC code generation: LLM4PLC, AutoPLC, and Agents4PLC established compiler-, retrieval-, debugging-, and validation-assisted approaches to PLC structured-text generation.Agents4PLC also introduced the 117-task benchmark used by the function track.
  • Agentic code generation and repair: General agentic code-generation research combines execution or critique feedback, tool use, reusable infrastructure, standardized protocols, and repository context.SemaPLC adapts these ideas to continuously executing, state- and time-sensitive PLC programs.
  • Formal verification and runtime validation for PLCs: PLC verification research includes model checking and PLCverif translations, but timers and large state spaces can make results unsupported or inconclusive in practice.Formal verification provides strong guarantees for supported, formalized properties.

3 Problem Formulation

The paper formulates separate function and project-context tracks, evaluating generated PLC logic through held-out verification or integrated project metrics. Algorithm 1 accepts logic only when logged checks satisfy completion criteria; otherwise it returns failure.

  • Function track: In the function track, the system generates a POU Lf from requirement Rf and local interface If, then a held-out judge compiles and model-checks it.The primary metric is based on Vf, the fraction of verified properties satisfied; compilation is auxiliary.
  • Function track: The function-track verification threshold is 0.80, while inconclusive model checks and generation failures count as failures.Inconclusive checks include unsupported constructs, translation failures, and timeouts.
  • Project-context track: In the project-context track, generated logic Lp is integrated into an existing project P, rather than synthesizing a whole plant from scratch.The project includes a function-block library, variable declarations, interfaces, an entry harness, and build configuration.
  • Project-context track: The integrated program is scored independently by integrated compilation C(P ′) ∈{0, 1} and static behavior S(P ′, Rp) ∈[0, 100].The supplied formulation continues the static-behavior definition beyond the excerpt.
  • Verification-gated generation: Algorithm 1 runs required checks for specification audit, compilation, and live runtime, records only log-confirmed verdicts, and returns failure when the budget is exhausted.It accepts implementation L only when the logged verification results satisfy the completion criteria.

4 The SemaPLC Agent Harness

SemaPLC combines project-grounded PLC code generation with specification, compilation, and runtime verification, accepting implementations only when logged checks satisfy track-specific criteria. Its bounded repair loop invalidates stale verdicts and requires machine-readable, tool-log-backed claims.

  • Inputs and architecture: SemaPLC receives only a natural-language control requirement plus either a local POU interface or an existing PLC project as task context.The skill library, PLC tools, checks, retry limit, and budget remain internal harness capabilities rather than per-task inputs.
  • Inputs and architecture: Five components organize the harness: an agent core, project and task grounding, a PLC skill library, verification processes, and a verification gate.The core is generic and event-driven, with no PLC-specific logic, and is accessed through a standard chat-completion interface.
  • Project grounding: Project grounding retrieves structure, reuses existing variables and function blocks, avoids redefining interfaces, and edits within a bounded scope to preserve project conventions.On the function track, grounding reduces to parsing the POU interface; domain knowledge is supplied through rules, curated documentation, and procedural skills.
  • Verification processes: Verification combines clause-by-clause specification audits with compilation and live runtime validation against requirement-derived assertions or trusted golden traces.The specification audit covers devices, signals, published variables, thresholds, interlocks, mutual exclusion, priorities, and scan-cycle semantics; runtime validation deploys, initializes, injects scenarios, and samples external variables.
  • Verification gate: r = 2 repair rounds are allowed per check, every edit invalidates all prior verdicts, and unlogged claims are downgraded to unchecked.Each outcome is a machine-readable sentinel cross-validated against the tool-call log, so verdicts attach to the exact implementation bytes.

5 Experimental Setup

The experiments evaluate function-level reliability on 117 repaired independent-POU tasks and project-grounded reliability on 65 industrial control tasks. Both tracks use seven backbone models, while project tasks are assessed through integrated compilation, static behavior, and dynamic behavior.

  • Project-context track: 65 project-context tasks span ten industrial plants and require generated logic to compile and deploy within full IEC 61131-3 projects.Inputs include section narratives, function-block interfaces and libraries, and empty entry harnesses; reference implementations and runtime traces remain hidden.
  • Models and baselines: Both tracks use the same seven backbone models from five vendors and two capability tiers, with all methods calling identical model endpoints.The models are MiniMax-M2.7, MiniMax-M3, Qwen3.5-Plus, DeepSeek-V4-Flash, DeepSeek-V4-Pro, GLM-5.2, and GPT-5.5.
  • Evaluation criteria: Function-track candidates must compile under RuSTy and pass PLCverif model checking for every requirement-derived property.The judge follows the Agents4PLC comparison protocol and uses the nuXmv backend for PLCverif.
  • Evaluation criteria: Project-context evaluation measures integrated compilation C as a binary build result and static behavior S as deterministic oracle-assertion satisfaction on program text.Static assertions cover required calls, normalized numeric constants, structural references, substring conditions, and any-of sets, and require hidden-reference satisfaction.

6 Results

SemaPLC achieves the strongest verified performance across both independent-POU and project-context tracks, with its largest advantage emerging from live-runtime verification. Ablations and case analysis show that external checks convert hidden integration and behavioral defects into repairable feedback.

  • Function track: 72.6% mean strict verified pass rate makes SemaPLC best on all seven models, exceeding Agents4PLC’s 63.9% mean by 8.8 points.Its strongest GPT-5.5 result is 82.1% versus 79.5%.
  • Harness effect: 8.5 to 33.3 points are the per-model gains from bare to full SemaPLC, while cross-model spread shrinks from 37.6 to 14.6 points.Bare compile rates also rise from an 85.5% mean to 99.2%.
  • Case study: 500 versus 2500 is the runtime-detected mismatch in the low-flow case, where SemaPLC repairs its compiling intermediate candidate and re-verification confirms correctness.Agents4PLC also compiles but lets the low-flow assignment overwrite the fault default.
  • Runtime discrimination: 22.4 to 31.4 dynamic spread versus 71.7 to 75.7 static spread shows runtime behavior separates methods that static scoring compresses.SemaPLC’s static-to-dynamic drop is 29.4.
  • Layer ablation: 54.1 dynamic score after all verification layers, up from 23.1 with generation alone, reflects cumulative gains of +13.4 from compilation and +10.4 from runtime checks.Static behavior changes much less, from 71.5 to 78.0.

7 Conclusion

SEMAPLC grounds PLC code generation in the task or project and withholds completion until logged specification, compilation, and live-runtime checks confirm the result. Across function and project-context tracks, it achieves the strongest verified and runtime results across seven backbone models.

  • Conclusion: SEMAPLC grounds generation in the task or project and requires logged specification, compilation, and live-runtime checks before completion.The completion rule is verification-gated rather than based on the model’s judgment.
  • Conclusion: 72.6% mean strict verified pass rate, +17.3 over bare, was the best result on every model across the 117-task function track.The comparison used seven backbone models.
  • Conclusion: 89.4 mean integrated compilation was the best result on the 65-task project-context track.Generated logic had to work within project context for this track.
  • Conclusion: 52.2 mean dynamic behavior exceeded every baseline, whose score was at most 31.4.Dynamic behavior was evaluated in the project-context results.

A Function-Track Oracle Audit

A three-round audit of the Agents4PLC function-track oracle confirmed defects across 43 of 117 tasks, leading to repairs or deletions in the released data. The audit targeted logical and specification errors, reducing the property count from 629 to 607.

  • Audit procedure: Three audit rounds used independent review, scratch re-derivation, brute-force truth tables, state-machine simulation, and blind adjudication.Only defects confirmed by at least two rounds were repaired; baseless properties were deleted rather than replaced.
  • Defect findings: 43 of 117 tasks contained confirmed oracle defects spanning five classes: wrong constants or polarities, tautological assertions, design contradictions, invented thresholds, and copy-paste duplicates.These classes capture both logical errors and properties inconsistent with the intended design.
  • Released data: 53 samples were modified in the released data: 46 with repaired properties and 7 with completed task descriptions only.The confirmed defects affected the function-track oracle’s released benchmark data.

B Project-Track Oracle and Scenario Details · C PLC Tool Suite

The project track evaluates generated PLC logic across 65 plant-specific control tasks using automatically derived static oracles and runtime scenarios. A unified PLC tool server supports both agent tool-calling and scripted verification workflows.

  • B Project-Track Oracle and Scenario Details: 65 tasks each target one control task within a plant section, drawn from 130 function-block implementations with empty bodies.An automated exact-string audit found no verbatim copying of hidden references in task packages or method run directories.
  • B Project-Track Oracle and Scenario Details: No verbatim reuse was detected because the audit matched exact strings, ruling out copied hidden references but not semantic imitation.The audit covered both generated task packages and each method’s run directory.
  • B Project-Track Oracle and Scenario Details: 63 of 65 tasks receive automatically derived static assertions from per-plant runtime tests.A parser locates section-specific test functions and extracts their string and numeric literals.
  • B Project-Track Oracle and Scenario Details: Six assertion types cover substring presence and absence, required calls, numeric constants, structural references, and any-of sets.Only items also occurring in the hidden reference implementation become assertions.
  • B Project-Track Oracle and Scenario Details: Each task receives up to six dynamic scenarios, including normal operation, configured analog-limit violations, and discrete Boolean-input flips.Candidate and reference logic run in identical harnesses, with observed ports based on the reference’s function interface.
  • C PLC Tool Suite: All PLC tools reside in one server exposing an MCP stdio surface for tool-calling agents and a CLI surface for scripted procedural skills.Tables S1 and S2 list the MCP tools and CLI entry points.
  • C PLC Tool Suite: The declarative verify runner builds, drives cases, asserts, and cleans up under one plan, without a single-tool MCP equivalent.It is among the CLI entry points exposed for script-driven use.

D PLC Skill Library

The PLC skill library packages procedural knowledge as on-demand Markdown skills that prescribe permitted and forbidden actions without task-specific answers. Its review checklists cover major PLC defect classes, while the delivery gate admits work only after artifact integrity and runtime-validation evidence are logged.

  • Skill packaging: Skills are on-demand Markdown documents under .sema/skills/ specifying applicability, readable inputs, ordered steps, and forbidden actions.They carry no task-specific answer, and review skills forbid reading or guessing hidden verification properties, reference implementations, or recorded traces.
  • Review checks: The review checklist covers contract extraction, coverage, boundary discipline, global invariants, behavioral fidelity, and scan-cycle semantics.Coverage checks named devices and signals, boundary discipline resolves threshold comparisons and otherwise cases, and scan-cycle semantics distinguishes persistent from recomputed state.
  • Review checks: Reviewers enforce safety and control invariants, including alarm or interlock actuator states, mutually exclusive commands, faulted sensors, fail-safe behavior, calibrated ranges, and permissives.Each item is reported as passed or revised.
  • Delivery gate: The delivery gate admits a task only when the delivered file has no address literal, hash-matches the last successful compilation input, and has logged deployment and forced-input evidence.Runtime validation uses an injected test copy while leaving the delivered file untouched.

E Evaluation Isolation and Information Access

Evaluation separates information available during generation from information used for final scoring. Methods generate from task inputs and compiler diagnostics, without access to held-out judges, assertion oracles, golden references, or traces.

  • Information access: Generation workspace contains only task inputs, including the requirement, interface catalog, and empty target file.Held-out judges, assertion oracles, golden references, and traces are absent.
  • Information access: Compiler diagnostics are visible during generation and determine the integrated-compilation layer.This makes compiler feedback part of generation-time access while remaining distinct from held-out scoring resources.
  • Information access: All methods operate under the same restriction separating generation-time information from final-scoring information.Table S4 documents this structural separation rather than relying on declarations.
Loading 2608.18565v1…