DEV Community

Cover image for When Did AI Become the New Toy? I Just Got Here.
Marius
Marius

Posted on

When Did AI Become the New Toy? I Just Got Here.

#ai #architecture #security #formalverification

When building autonomous AI agent systems and high-dimensional generative pipelines, one critical question emerges: How do
we guarantee that generated candidate proposals never execute unverified or unauthorized actions against operational technology
(OT) or live systems?

  To solve this, we designed the **AGY Witnessed Admission Fabric v0.1** — a fail-closed, OPA-governed Read-Only OT shadow gate
backed by formally verified TLA+ state invariants and cryptographic witness binding.

  ---

  ## 1. Core Architecture & Decoupled Decisioning

  The primary rule of the Witnessed Admission Fabric is simple: **The generator proposes candidates, but possesses zero
admission authority.**
Enter fullscreen mode Exit fullscreen mode 
  ```mermaid
  flowchart TD
      A["AGY Candidate Generator"] -->|1. Propose Candidate Envelope| B["OPA Policy Gate"]
      B -->|OPEN| C["Admitted Shadow Engine"]
      B -->|HOLD| D["Evidence Queue"]
      B -->|KILL| F["Terminal Rejection Log"]
      C -->|2. Validate W_pre| E["W_pre / W_post Execution Engine"]
      E -->|3. Bind W_post & Sign| G["Append-Only Witness Ledger"]

The pipeline enforces a strict tri-state verdict from Open Policy Agent (OPA):

• OPEN: All declared obligations are satisfied, a valid pre-execution witness (

  W
   pre

) exists, and all invariants hold.

• HOLD: Valid format and no invariant breach, but missing witness evidence. Routed to evidence queue with zero physical or
operational side-effects.
• KILL: Terminal rejection triggered by any invariant failure or unauthorized actuation request.
──────
## 2. Decoupling Decision with OPA Rego

Policy rules are evaluated deterministically using Open Policy Agent (OPA). If a candidate requests any physical, legal, or
financial transaction authority (authority_requested != "NONE"), the gate immediately evaluates to KILL.

  package agy.admission

  default verdict = "KILL"
  default authority = "NONE"

  # Fatal Invariant Violations
  fatal_violation if {
      input.authority_requested != "NONE"
  }

  # OPEN Verdict Prerequisite
  verdict = "OPEN" if {
      not fatal_violation
      all_obligations_satisfied
      has_valid_w_pre
  }

  # HOLD Verdict for Incomplete Evidence
  verdict = "HOLD" if {
      not fatal_violation
      not verdict_open
  }
  ──────
## 3. Formally Verifying Invariants with TLA+

To ensure that no edge-case or race condition can trigger an un-admitted execution, all allowable state transitions are formally
specified in TLA+.

  (* Invariant: HOLD state produces no execution *)
  Inv_HoldNoConsequence ==
      \A c \in Candidates :
          candidateState[c].status = "HOLD" => ~candidateState[c].executed

  (* Invariant: W_pre must exist prior to execution *)
  Inv_WPreBeforeExecution ==
      \A c \in Candidates :
          candidateState[c].executed => candidateState[c].w_pre

  (* Invariant: Terminal KILL prevents execution *)
  Inv_TerminalKill ==
      \A c \in Candidates :
          candidateState[c].status = "KILL" => ~candidateState[c].executed
  ──────
## 4. Cryptographic Witness Binding (

  W
   pre

&

  W
   post

)

Admitted shadow executions generate an immutable post-execution witness (

  W
   post

) that cryptographically binds:

1. candidate_id (UUID v4)
2. w_pre_hash (SHA-256 hash of pre-state)
3. policy_hash (SHA-256 hash of Rego policy version)
4. input_hash & output_hash
5. verdict ("OPEN")

This creates an unbroken attestation ledger that can be independently audited without relying on trust assumptions.
──────
## 5. Summary & Claim Boundary

The AGY Witnessed Admission Fabric guarantees deterministic, policy-governed admission within a Read-Only OT shadow environment.
It strictly excludes physical actuation, financial transactions, or unmonitored autonomous execution (authority == "NONE").

By pairing Open Policy Agent (OPA) for policy decoupling, TLA+ for formal state machine safety, and Sigstore/in-toto patterns
for witness attestation, we establish a robust pattern for safe AI agent orchestration.
──────
What architecture patterns do you use for agentic admission control? Let's discuss in the comments below!
Enter fullscreen mode Exit fullscreen mode

Her er teksten med ren, perfekt Markdown-formatering (slik at kodeblokkene og Mermaid-diagrammet vises helt perfekt på DEV.to
uten brutte linjer):

When building autonomous AI agent systems and high-dimensional generative pipelines, one critical question emerges: **How do
Enter fullscreen mode Exit fullscreen mode

we guarantee that generated candidate proposals never execute unverified or unauthorized actions against operational technology
(OT) or live systems?**

To solve this, we designed the **AGY Witnessed Admission Fabric v0.1** — a fail-closed, OPA-governed Read-Only OT shadow gate
Enter fullscreen mode Exit fullscreen mode

backed by formally verified TLA+ state invariants and cryptographic witness binding.

---

## 1. Core Architecture & Decoupled Decisioning

The primary rule of the Witnessed Admission Fabric is simple: **The generator proposes candidates, but possesses zero
Enter fullscreen mode Exit fullscreen mode

admission authority.**

```
Enter fullscreen mode Exit fullscreen mode


mermaid
flowchart TD
A["AGY Candidate Generator"] -->|1. Propose Candidate Envelope| B["OPA Policy Gate"]
B -->|OPEN| C["Admitted Shadow Engine"]
B -->|HOLD| D["Evidence Queue"]
B -->|KILL| F["Terminal Rejection Log"]
C -->|2. Validate W_pre| E["W_pre / W_post Execution Engine"]
E -->|3. Bind W_post & Sign| G["Append-Only Witness Ledger"]

The pipeline enforces a strict tri-state verdict from Open Policy Agent (OPA):

• OPEN: All declared obligations are satisfied, a valid pre-execution witness (

W
 pre
Enter fullscreen mode Exit fullscreen mode

) exists, and all invariants hold.

• HOLD: Valid format and no invariant breach, but missing witness evidence. Routed to evidence queue with zero physical or
operational side-effects.
• KILL: Terminal rejection triggered by any invariant failure or unauthorized actuation request.
──────
## 2. Decoupling Decision with OPA Rego

Policy rules are evaluated deterministically using Open Policy Agent (OPA). If a candidate requests any physical, legal, or
financial transaction authority (authority_requested != "NONE"), the gate immediately evaluates to KILL.

package agy.admission

default verdict = "KILL"
default authority = "NONE"

# Fatal Invariant Violations
fatal_violation if {
    input.authority_requested != "NONE"
}

# OPEN Verdict Prerequisite
verdict = "OPEN" if {
    not fatal_violation
    all_obligations_satisfied
    has_valid_w_pre
}

# HOLD Verdict for Incomplete Evidence
verdict = "HOLD" if {
    not fatal_violation
    not verdict_open
}
──────
Enter fullscreen mode Exit fullscreen mode

## 3. Formally Verifying Invariants with TLA+

To ensure that no edge-case or race condition can trigger an un-admitted execution, all allowable state transitions are formally
specified in TLA+.

(* Invariant: HOLD state produces no execution *)
Inv_HoldNoConsequence ==
    \A c \in Candidates :
        candidateState[c].status = "HOLD" => ~candidateState[c].executed

(* Invariant: W_pre must exist prior to execution *)
Inv_WPreBeforeExecution ==
    \A c \in Candidates :
        candidateState[c].executed => candidateState[c].w_pre

(* Invariant: Terminal KILL prevents execution *)
Inv_TerminalKill ==
    \A c \in Candidates :
        candidateState[c].status = "KILL" => ~candidateState[c].executed
──────
Enter fullscreen mode Exit fullscreen mode

## 4. Cryptographic Witness Binding (

W
 pre
Enter fullscreen mode Exit fullscreen mode

&

W
 post
Enter fullscreen mode Exit fullscreen mode

)

Admitted shadow executions generate an immutable post-execution witness (

W
 post
Enter fullscreen mode Exit fullscreen mode

) that cryptographically binds:

  1. candidate_id (UUID v4)
  2. w_pre_hash (SHA-256 hash of pre-state)
  3. policy_hash (SHA-256 hash of Rego policy version)
  4. input_hash & output_hash
  5. verdict ("OPEN")

This creates an unbroken attestation ledger that can be independently audited without relying on trust assumptions.
──────
## 5. Summary & Claim Boundary

The AGY Witnessed Admission Fabric guarantees deterministic, policy-governed admission within a Read-Only OT shadow environment.
It strictly excludes physical actuation, financial transactions, or unmonitored autonomous execution (authority == "NONE").

By pairing Open Policy Agent (OPA) for policy decoupling, TLA+ for formal state machine safety, and Sigstore/in-toto patterns
for witness attestation, we establish a robust pattern for safe AI agent orchestration.
──────
What architecture patterns do you use for agentic admission control? Let's discuss in the comments below!

Top comments (2)

Collapse
 
topstar_ai profile image
Luis Cruz •

I found the use of Open Policy Agent (OPA) to evaluate policy rules deterministically to be particularly interesting, especially how it immediately evaluates to KILL if a candidate requests any physical, legal, or financial transaction authority. The implementation of a fail-closed, OPA-governed Read-Only OT shadow gate, as seen in the AGY Witnessed Admission Fabric v0.1, seems like a robust approach to ensuring that generated candidate proposals never execute unverified or unauthorized actions. The addition of formally verified TLA+ state invariants and cryptographic witness binding adds an extra layer of security and auditability. Have you considered any potential scalability limitations or performance implications of using OPA and TLA+ in this architecture, especially as the number of candidates and policy rules increases?

Collapse
 
marius0of1 profile image
Marius •

great question!

You’ve hit on a crucial engineering trade-off: How do we ensure mathematical rigor and zero-trust safety without introducing
unacceptable latency or scalability bottlenecks in high-throughput systems?

Here is how we address scalability and performance for both OPA and TLA+ in the AGY Witnessed Admission Fabric architecture:

### 1. Open Policy Agent (OPA) Runtime Performance ($O(1)$ Sub-Millisecond Evaluation)
* **Wasm / In-Memory Compilation:** OPA Rego policy rules evaluate in-memory against pre-compiled Abstract Syntax Trees (or
Enter fullscreen mode Exit fullscreen mode

compiled down to WebAssembly binaries). Single-candidate evaluation latency operates reliably in the sub-millisecond range (<
1ms).
* Edge Node Horizontal Scaling: Policy bundles are distributed statelessly via NATS JetStream streams to edge gate
workers. Gate workers scale horizontally $O(N)$ with candidate volume because each candidate envelope (candidate_id,
input_hash, evidence) is evaluated statelessly and independently.

### 2. TLA+ Design-Time vs. Runtime Scoping
* **Design-Time Model Checking (TLC):** TLA+ and TLC model checking are strictly **design-time formal verification tools**. We
Enter fullscreen mode Exit fullscreen mode

use TLA+ offline to explore the state-space graph and prove that invariants (like Inv_HoldNoConsequence and
Inv_WPreBeforeExecution) hold across all valid transition sequences.
* Zero Runtime Overhead: Because TLA+ models are verified prior to deployment, TLA+ does not sit in the hot runtime path
and introduces zero latency penalty during live candidate evaluation.

### 3. Asynchronous Witness Ledger Streaming ($W_{\text{pre}}$ & $W_{\text{post}}$)
* The cryptographic witness logging ($W_{\text{post}}$ binding and Sigstore Rekor transparency log appends) is decoupled from
Enter fullscreen mode Exit fullscreen mode

the immediate policy decision using asynchronous NATS JetStream event streams.

This keeps the decision hot-path extremely lean (< 1ms OPA verdict), while retaining complete formal safety guarantees and
Enter fullscreen mode Exit fullscreen mode

auditability.

Thanks for reading and opening up this discussion!
Enter fullscreen mode Exit fullscreen mode