✓
varek-lang.org · MIT · patent-pending
What is
VAREK?
VAREK verifies what an autonomous AI agent is about to do — and proves it complies with policy — before it does it.
A runtime and companion language for deterministic, pre-execution verification of AI agent actions. Current release: v1.21.1.
01
VAREK
The problem
"Usually right" is
not a safety standard.
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.
02
VAREK
The principle
Authorization
before execution.
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.
03
VAREK
Three verdicts, not two
It is honest about
its own limits.
SATISFIED
proceed
Provably compliant with policy — and the certificate is accepted by an independent checker. Execution may proceed.
UNSATISFIED
deny
Provably violates policy. Execution is denied.
UNKNOWN
fail closed
Cannot be proven either way within bounds. Fail closed — never coerced to a pass.
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.
04
VAREK
Not a platform feature
Platforms build agents.
VAREK checks every one.
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.
05
VAREK
One vertical stack
From the plan you declare
to the syscall it gates.
plan gate · action-graph · v1.6 → v1.21.1
The declared plan is verified before the agent starts — every step against policy, and data flow along its edges. A secret source cannot reach a forbidden sink.
decision procedure · v1.13 – v1.14
An SMT decision procedure over bounded strings and bitvectors decides each action — SATISFIED / UNSATISFIED / UNKNOWN — in microseconds, with a bounded worst case.
certificates · v1.15
Every authorization is independently checked — a small checker that shares no code with the procedure must accept its certificate before the action runs.
Warden · kernel boundary · seccomp-BPF + user-notify
Every file open, lookup, connect and launch is held and decided at the kernel boundary, on a default-deny allowlist, with the agent unprivileged and its lifetime tied to the supervisor's.
resolve · decide · deliver · v1.12 → v1.21
Decides on the object it delivers — each file is resolved once and the same descriptor handed over; each connect is dialed by the Warden and the connected socket handed over. Nothing can be swapped after the check.
evidence · v1.16
A record no one can quietly rewrite — every record hash-chained, with checkpoints Ed25519-signed and anchored off the host, exportable in the CycloneDX 1.6 format.
06
VAREK
From v0.1 to today
How it got here.
v0.xOrigins. A compiled, statically typed pipeline language — Hindley-Milner inference extended to tensor shapes, LLVM backend.
v1.0Public launch. The formal-verification layer, MIT-licensed.
v1.4–v1.5The Warden. Kernel-boundary enforcement via seccomp-BPF and seccomp user-notify.
v1.6–v1.8Plans and data flow. Pre-execution verification of agent action-graphs; cross-action information flow with audited declassification.
v1.9Progress-safety. A load-time liveness proof — certified human-out-of-the-loop. Then a complete boundary: default-deny allowlist, x32 closed, lifecycle coupling.
v1.12Mediation correctness. The Warden decides on the object it actually delivers; the record cannot be forged by agent input.
v1.13–v1.15The verification program. An SMT decision procedure in the enforcement path; glob and suffix matching; a certificate for every authorization. shipped
v1.16–v1.17Evidence and privilege. A signed, anchored verdict stream; the agent unprivileged; the Warden's own files refused by identity. shipped
v1.18–v1.20The plan gate in the Warden. Data flow, the refusal breaker and progress-safety run before the agent starts. shipped
v1.21Decided connections. The Warden dials each allowed connect itself and hands over the socket (v1.21.0); plan steps declare how they open a file (v1.21.1). current · v1.21.1
07
VAREK
v1.13 → v1.21.1 · what's new
Checked, signed,
and connected.
From v1.13 the SMT decision procedure runs in the enforcement path, and from v1.15 it no longer has the last word: every authorization carries a certificate that an independently written checker must accept before the action takes effect. From v1.16 the record of every decision is hash-chained, signed and anchored off the host, so whoever holds the log cannot rewrite it.
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.
Along the way: the agent runs with no privileges; stat, access and readlink are decided like opens; the plan gate runs the data-flow check, the refusal breaker and the progress-safety proof before the agent starts; and 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.
08
VAREK
The program · v1.10 → v1.11
Shrink UNKNOWN —
without weakening
soundness.
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.
1
Verdict-distribution harness. Measures the clear rate and gates every change on zero unsafe authorizations — 85.4% of safe file opens cleared, none unsafe, on the seed corpus. shipped v1.13
2
Bitvector fragment. Proves open-flag bits at the Warden boundary, so a policy can grant read-only access. shipped v1.13
3
Bounded string fragment. Prefix, exact, suffix, contains and glob — deny a kind of file wherever it appears under an allowed tree. shipped v1.14
4
Host names without agent DNS. Policies name hosts; the Warden resolves them and the agent never sends a DNS query. planned v1.21.2
5
Bounded sequence fragment. Element-level reasoning over payloads, composed on the fragments above. candidate
// the invariant, never violated:
every extension of the decision fragment may only move cases out of UNKNOWN.
none may ever move a genuinely unsafe action → SATISFIED.
09
VAREK
Why this, why now
The problem is now
a national priority.
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.
10
VAREK
In one line
Prove what your agent
is about to do —
before it does it.
Kenneth Wayne Douglas, MD · Sober Agentic Infrastructure, Inc. · MIT · patent-pending
11