VAREK has shipped through v1.21.1. The v1.10 verification program — move cases out of UNKNOWN into a provable verdict, raising the clear rate on safe agent actions, under an invariant that forbids ever authorizing an unsafe one — shipped its first three releases as v1.13–v1.15. Host names and the bounded sequence fragment are next.
| Version | Capability |
|---|---|
| v1.0 | Public launch — formal-verification layer, MIT license. |
| v1.4–v1.5 | The Warden — kernel-boundary enforcement (seccomp-BPF and seccomp user-notify); fast-path matcher. |
| v1.6 | Pre-execution, compositional verification of agent action-graphs. |
| v1.7 | Vertical stack — verification bound to enforcement at the system boundary. |
| v1.8 | Cross-action data-flow verification; audited declassification; bounded-refusal breaker. |
| v1.9 | Progress-safety verification — a load-time liveness proof. Certified human-out-of-the-loop. |
| v1.9.1 | Enforcement hardening — io_uring refused; TOCTOU-safe file mediation. |
| v1.9.2 | Mediation completeness — default-deny seccomp-BPF allowlist, x32 ABI closure, hard-deny syscall set. |
| v1.9.3 | Lifecycle coupling in the live Warden — if the supervisor stops, the agent stops, and so does everything it started. |
| v1.12 | Mediation correctness — the verifier decides on the resolved object it delivers; side-effect-free denial; authenticated verdict stream; inbound networking refused; threads, children and dynamically linked agents supported; CycloneDX 1.6 evidence export. |
| v1.13 | The SMT decision procedure in the enforcement path — bounded strings and bitvectors, read-only flag clauses, load-time rule reachability, solver cross-check, verdict-distribution harness. |
| v1.14 | Bounded string fragment — exact, suffix, contains and glob matchers on the resolved path, with exact reachability and witnesses. |
| v1.15 | Certificates — every authorization checked by an independent checker before it takes effect. |
| v1.16 | A verdict stream its holder cannot rewrite — hash-chained, Ed25519-signed, anchored off the host; a bound on the work of every decision; deployment preflight. |
| v1.17 | The Warden's own files refused by identity; stat, access and readlink decided; the agent runs unprivileged. |
| v1.18 | The claims and the code agree — the plan gate runs the data-flow check, refusal breaker and progress-safety proof; signed, schema-tested CycloneDX export. |
| v1.19–v1.20 | A refusal limit per session; fields on plan steps. |
| v1.21.0 | Decided connections — each connect decided on the destination copied once, dialed by the Warden and handed to the agent as a connected socket. |
| v1.21.1 current | Plan steps say how they open a file (open=), so the plan gate authorizes declared reads on read-only grants, as the runtime would. |
The marketable end is a measured number: on a realistic agent workload, VAREK clears X% of safe actions with zero unsafe authorizations at sub-millisecond decision latency. Theory extension is the means; the verdict-distribution metric is the end. Each step was gated by the harness.
Measurement and regression gating over a corpus of agent actions, with a hard unsafe_satisfied == 0 gate. On its synthetic seed corpus of file opens, v1.13 clears 85.4% of safe opens with none unsafe authorized. A baseline on a customer workload and policy is next.
Decidable reasoning over open-flag bits at the Warden boundary, so a policy can say read-only. Bits outside the ABI set force UNKNOWN, never a silent pass.
Prefix and equality in v1.13; suffix, contains and glob in v1.14 — so a policy can deny a kind of file wherever it appears under an allowed tree. A length guard keeps it sound: over-length inputs return UNKNOWN, never truncate-then-check.
Every SATISFIED verdict carries a certificate, and an independently written checker must accept it before the action runs — the decision procedure moves from trusted to checked.
Policies name hosts (allow host api.example.com:443). The Warden resolves the allowed names itself and answers the agent's host lookup with only those names, so the agent never sends a DNS query, a name the policy does not allow does not resolve, and DNS cannot carry data out. The decision is made on name:port, certified like any host rule, and recorded with the resolution it relied on.
Element-level reasoning for the cross-action data-flow subsystem — collections modeled as a fixed N slots plus a length. Composes on top of the string and bitvector fragments (an element is one of those), so its soundness inherits theirs.
The DARPA/NSF AI Forge program (June 2026) names provably secure-by-construction agent sandboxes with verifiable action and information-flow bounds and low-latency runtime intervention as a national priority — the problem class VAREK's shipped architecture addresses. Cited as third-party validation of the problem, not as a claim of program involvement.
Items under "Next" and "Also on the line" are stated as direction. They are not present in a released tag and are not claimed as shipped.