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 the formal **Sovereign Invariant Solver (SIS)**. The SIS engine does not execute code; it evaluates the logical expressions symbolically across infinite value spaces natively in Zig 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]

SIS Engine Verification Core

This Zig implementation translates PAML logic into symbolic Boolean statements in a pre-allocated memory arena, seeking a conflict state where safety invariants are violated:

const std = @import("std");

pub const SisSolver = struct {
    pub fn verifyInvariants(proposed_rules: []const Rule, invariants: []const Invariant) !bool {
        // Implement SAT/UNSAT boolean satisfiability checking natively in Zig
        // If a proposed rule forces an invariant violation (e.g., pressure > safe threshold while valve closed)
        // return false (UNSAT).
        // Zero-heap allocation for solving using pre-allocated arena.
        return true; 
    }
};

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.