VAREK has shipped through v1.9. The next line is a single 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.
| Version | Capability |
|---|---|
| v1.0 | Public launch — formal-verification layer, MIT license. |
| v1.5 | The Warden — kernel-boundary enforcement (seccomp-unotify). |
| 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 current | Progress-safety verification — a load-time liveness proof. Certified human-out-of-the-loop. |
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. Built in this order, each step gated by the harness.
Measurement and regression gating over a corpus of realistic agent action-graphs. Reports the safe-action clear rate and enforces a hard zero-unsafe-authorization gate. Ground truth is the customer-authored policy; adversarial near-miss labels come from an independent oracle, never from us. A measured baseline ships as its own milestone.
Decidable reasoning over syscall flag and argument bits, aligned with the Warden kernel layer. Lowest audit cost; lands first to prove the loop end to end. Conservative-mask rule: bits outside the policy's mask force UNKNOWN, never a silent pass.
A length-bounded fragment (prefix/suffix/contains, fixed regex set) so path-prefix and host-allowlist predicates are provable instead of refused — the largest expected reduction in over-refusal. A length-guard escape keeps it sound: over-length inputs return UNKNOWN, never truncate-then-check. No new decision procedure.
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. Sequenced after strings for that reason.
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.
v1.10 and v1.11 are stated as direction. They are not present in a released tag and are not claimed as shipped.