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

Summary (Overview)

• SemaPLC is a verification-gated agent harness for PLC (Programmable Logic Controller) code generation that grounds generation in the target project and withholds completion until external checks confirm the result—rather than relying on the model's own self-assessment.
• The harness enforces three verification layers: specification audits, compilation checks, and live runtime validation, with a strict completion rule requiring logged external evidence for every claimed pass.
• On the function track (117 independent-POU tasks), SemaPLC achieves the highest strict verified pass rate on all seven models (72.6% mean vs. 63.9% for the strongest baseline), improving every backbone by 8.5–33.3 points.
• On the project-context track (65 tasks across ten industrial plants), SemaPLC leads in integrated compilation (89.4%), static behavior (81.6%), and dynamic behavior (52.2% vs. at most 31.4% for baselines)—demonstrating that methods looking similar under static evaluation differ sharply at runtime.
• The harness is open-sourced at https://github.com/midea-ai/SemaPLC.

Introduction and Theoretical Foundation

Background

Programmable logic controllers (PLCs) run industrial plants—factory lines, power plants, and water-treatment facilities—and are programmed primarily in IEC 61131-3 languages, of which Structured Text (ST) is the textual member. Prior work has established that LLMs can generate independent PLC program organization units (POUs), benefiting from:

• Compiler-in-the-loop repair
• Formal or property checking
• Multi-agent iteration
• Vendor IDEs
• Physical or simulated testbeds

The Gap

In production, control logic is rarely an isolated POU. Deployment imposes two further requirements:

1. Project grounding: Generated logic must integrate into an established project, reuse its modules and function blocks, respect its variables/types/interfaces, and honor build, reset, initialization, and safety conventions.
2. Correct runtime behavior: Even when integrated programs compile and pass static checks, they can still misconfigure timers, take wrong state transitions, miss resets, break interlocks, or drive outputs with wrong timing.

Key insight: Prior systems execute generated code to demonstrate it can run, not to measure how reliably it runs. No unified assessment establishes, across methods and models, how reliably generated logic meets these two requirements.

Three Design Principles of SemaPLC

1. Project-grounded generation: Anchors code generation and editing in available task or project context.
2. Multi-source verification: Treats specification checks, compilation, and live runtime validation as first-class external evidence.
3. Verification-gated iteration: Forbids the agent from terminating on its own judgment; failures, absences, or indeterminate outcomes require repair or incompletion reporting.

Methodology

Problem Formulation

Function track: Given requirement $R_f$ and local interface $I_f$, the system produces a POU $L_f = G(R_f, I_f)$. The primary metric is:

$$\operatorname{VerifiedPass}(L_f) = \mathbb{1}[V_f \geq 0.80], \tag{1}$$

where $V_f$ is the fraction of model-checked properties verified satisfied, with the 0.80 threshold following Agents4PLC.

Project-context track: Given requirement $R_p$ and existing project $P$, the system produces logic $L_p = G(R_p, P)$ and integrated program $P' = P \oplus L_p$, scored by three independent metrics:

• Integrated compilation $C(P') \in \{0, 1\}$
• Static behavior $S(P', R_p) \in [0, 100]$ (assertion-based, on program text)
• Dynamic behavior $D(P', \mathcal{T}) \in [0, 100]$ (golden-trace differential on live runtime)

Algorithm: Verification-Gated Generation

The harness runs on a generic event-driven tool-use core with five components:

1. Agent core: Plans, edits, interprets verification results
2. Project/task grounding: Retrieves project structure, reuses existing variables and function blocks
3. PLC skill library: Domain knowledge in documents (rules file, curated wiki, procedural skills)
4. Verification processes: Specification audits, compilation, live runtime validation
5. Verification gate: Decides completion per Algorithm 1

Three gate invariants:

• Bounded retries: Each check allows at most $r = 2$ repair rounds
• Edit invalidation: Any modification voids all prior verdicts; every check re-runs
• Earned claims: Each outcome is a machine-readable sentinel cross-validated against the tool-call log

Live Runtime Validation

Builds and deploys the implementation, initializes the runtime, injects scenario inputs, and samples external variables. Failure stages prescribe repair targets:

• Flat trace → wiring problem
• Changing but wrong trace → block logic
• Late transition → timer or edge detector

Empirical Validation / Results

RQ1: Function-Level Reliability

Table 1: Function track strict verified pass rate (%, denominator 117)

Key findings:

• SemaPLC attains the highest rate on all seven models (+8.8 points mean over strongest baseline)
• Cross-model spread shrinks from 37.6 points (bare) to 14.6 points (full)
• Weakest models gain most (MiniMax-M2.7 +29.9, DeepSeek-V4-Flash +33.3)

RQ2: Project-Grounded Reliability

Table 2: Project-context track (0–100, best per column in bold)

RQ3: Verification Across Layers

Key finding: All methods fall within 10 static points of one another, whereas dynamic scores separate them sharply (22.4 to 31.4 for baselines vs. 52.2 for SemaPLC).

Layer ablation (Table 3, DeepSeek-V4-Flash, 65 tasks):

Formal verification coverage (Table 5): Timers are the boundary—none of the 174 properties across 32 timer-bearing programs obtained a conclusive verdict, motivating runtime validation for stateful timing constructs.

RQ4: Interaction Cost

Theoretical and Practical Implications

1. Execution is the faithful test: Static scoring compresses and even reorders methods that runtime validation separates sharply. Benchmarks must execute generated logic to distinguish reliable methods from unreliable ones.

2. Verification-gated iteration is a model-agnostic reliability layer: The harness improves every backbone model (8.5–33.3 points), with the weakest models gaining most—the external checks compensate for model limitations.

3. Delivery-integrity guarantee: The three invariants (bounded retries, edit invalidation, earned claims) ensure the delivered program is identical to the candidate that earned every reported pass, with no unlogged self-reported pass surviving.

4. Formal verification has coverage boundaries: Timers (TON) fall outside conclusive model-checking coverage in practice, making runtime validation a necessary complement rather than an alternative.

5. Cost is architectural: SemaPLC's open-ended loop issues more requests (each tool call is a model decision), but achieves comparable wall-clock time on the project track and lower time on the function track.

Conclusion

SemaPLC demonstrates that a verification-gated agent harness—assembled from conventional tools but governed by strict external-check completion discipline—substantially improves PLC code generation reliability across models and evaluation layers. Key takeaways:

• Best results across all layers: 72.6% mean verified pass rate (function track), 89.4% integrated compilation, 81.6% static behavior, and 52.2% dynamic behavior (project track).
• Runtime validation is essential: Similar static scores mask sharply different runtime behavior; execution, not static scoring, is the faithful test.
• Two limitations remain: (1) dynamic scoring exercises a bounded scenario set, so behavior under unseen conditions remains unmeasured; (2) the advantage narrows on the strongest model (GPT-5.5).

Future directions: An end-to-end PLC development environment on this harness architecture, with editing, generation, and deployment governed by the same verification gate, and validation extended to process simulation.