Skip to main content

Filed under

Oscal

2 entries

  1. Security·7 min read·

    You Can't Prove the Agent. Prove the Gate.

    Formal verification for AI-agent security. You can't prove a probabilistic model does the right thing — but the deterministic gate in front of it is small enough to prove outright. Dafny proofs, a Rego twin, and differential testing, following the method AWS used for Cedar.

  2. Security·7 min read·

    The Firewall Stays Put. The Agent Improvises.

    Rewriting security controls for probabilistic agents. Static control catalogs assume systems that do what they're told; AI agents don't — so here's how to express agent guardrails (tool allowlists, secret-egress denial, audit) as machine-checkable OSCAL component definitions.