The Safety Verification Loop

Formal Verification vs. Testing

In traditional PLC environments, testing is empirical. Systems are simulated or tested in the field, and engineers try to discover edge cases. As interlock logic scales, the number of potential states increases exponentially (state explosion), making exhaustive manual testing impossible.

PAML shifts this burden to computer science. Before any generated PAML logic is allowed to compile into WebAssembly, it must pass through a formal **SMT (Satisfiability Modulo Theories)** solver like Microsoft Z3. The Z3 solver does not execute code; it evaluates the logical expressions symbolically across infinite value spaces in milliseconds to prove whether a violation can occur.

How the Loop Works

When a human operator prompts for a change (e.g., to override a valve or smooth out a pump rotation), the AI Agent edits both the PCN and the PAML logic. The verification script compiles these changes alongside the Safety Invariants and executes the SMT check:

[Candidate PAML + Invariants] → [Z3 SMT Solver]
                                      ⊞
        │                                     │
  [PASSED (unsat)]                      [FAILED (sat)]
        │                                     │
[Compile to WASM]              [Counter-Example Generated]
                                      │
                               [AI Auto-Correction]

Z3 SMT Script Structure

This script translates PAML logic into symbolic statements, seeking a conflict state where safety invariants are violated:

from z3 import *

# Initialize symbolic variables
PT301 = Real('PT301')       # Reactor Pressure (bar)
XV301_state = Real('XV301_state') # 0 = Closed, 1 = Open
FIT101 = Real('FIT101')     # Feed Flow

s = Solver()

# Immutable Invariant: Over-pressurization rule
s.add(Implies(PT301 > 42.5, XV301_state == 0.0))

# Proposed PAML rule 1 (Interlock)
s.add(Implies(PT301 > 42.5, XV301_state == 0.0))

# Proposed PAML rule 2 (Optimization Policy)
# "If flow drops, open the isolation valve to prevent pump cavitation"
s.add(Implies(FIT101 < 10.0, XV301_state == 1.0))

if s.check() == sat:
    print("❌ SAFETY BREACH SATISFIED. Counterexample:")
    print(s.model()) # Outputs conflicting inputs (e.g. Pressure = 43.0, Flow = 5.0)
else:
    print("✅ Logic verified. No overlapping states possible.")

Autonomous Self-Correction

If Z3 returns a conflict (SAT), the compiler captures the mathematical proof, translates the variable states into natural language, and passes the error block back to the AI Agent. The agent reasons through the overlap, updates the PAML rule to be conditional (e.g., adding an over-pressure constraint to the pump protection rule), and re-submits it until the solver passes with an `unsat` (unsatisfiable failure) status. The verified logic is then flashed to the virtual PLC.