VAREK verifies what an autonomous AI agent is about to do — and proves it complies with policy — before it does it.
Agentic systems act in the world. They call tools, read and write data, and chain actions toward goals. The dominant safety posture is probabilistic — a model that is usually right. But the tail is where harm lives.
Medicine does not deploy systems that are usually right. VAREK applies that clinical standard to what an agent is allowed to do.
Every action is checked against an explicit, human-authored policy — with a determinate decision — before it is allowed to take effect. The decision procedure does not guess. A refusal is a safe outcome; an unverified action is not.
A two-state system must turn every UNKNOWN into a false pass or a false block. VAREK refuses that conversion. That is the difference between a verifier and a heuristic — and why the verdict is sound: nothing is SATISFIED unless it is provably safe.
Agents run on many model providers, frameworks and in-house stacks, and a platform’s own guardrail covers only its own agents. VAREK enforces one policy at the kernel boundary every agent’s actions cross — beneath each platform’s guardrails, not in place of them.
The checker is not the vendor: the decision and its signed evidence are produced outside the agent, so they can be verified without trusting the vendor that built it. And where platform controls steer and score to keep agents working, VAREK refuses anything it cannot prove.
Through v1.20 a supervised agent had no network at all. v1.21 gives it one without giving up the guarantee: the Warden decides each connect on the destination it copied once, dials it itself, and hands the agent the connected socket — the same resolve-decide-deliver discipline it has applied to files since v1.12. In 2,000 attempts to swap the destination after the check, none reached the denied side.
v1.22 puts the runtime behind one command: varek sets up a host, supervises an agent, explains every refusal, re-checks the evidence and exports it signed. And varek bench measures what the Warden adds to each call on your own machine, checking every verdict while it does. On a 2-vCPU host the agent waits about 55 µs for a refused file open and 70–80 µs for an authorized one. v1.23 ships it as VAREK Enterprise on AWS Marketplace: a hardened Amazon Linux image with the Enterprise policy packs, licensed through AWS License Manager, with a deployment guide.
Underneath, since v1.13–v1.16: an SMT decision procedure in the enforcement path; a certificate for every authorization that an independently written checker must accept; a record of every decision hash-chained, signed and anchored off the host; the agent unprivileged. v1.21.1 lets a plan step declare how it opens a file, so read-only grants verify at the gate. Verdict semantics are unchanged throughout: no extension may move a genuinely unsafe action to SATISFIED.
UNKNOWN is the safe residue, but every UNKNOWN on a safe action is utility lost. The verification program moves those cases into a provable verdict, raising the clear rate on safe work — while a hard invariant forbids ever turning an unsafe action into SATISFIED. Its first three releases have shipped.
The DARPA/NSF AI Forge program (June 2026) calls for provably secure-by-construction agent sandboxes with verifiable action and information-flow bounds and low-latency runtime intervention. That is the problem class VAREK's shipped architecture already addresses — cited as third-party validation of the problem, not as a claim of program involvement.
Open source under the MIT license. Three provisional patent applications cover the SMT decision-procedure layer, the Warden kernel architecture, and action-graph compositional policy decision. Patent-pending.