✓
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 compiled language and runtime for deterministic, pre-execution verification of AI agent actions.
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. 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
One vertical stack
From the policy you write
to the syscall it gates.
surface language · var::
You write policy in a typed surface language, compiled to a formal obligation.
decision procedure
A satisfiability-modulo-theories decision procedure discharges it — SATISFIED / UNSATISFIED / UNKNOWN.
action-graph · v1.6
Plans are verified compositionally and re-verified as the agent revises them mid-task.
Warden · kernel boundary · v1.7
Enforced at the system boundary — the same policy you reason about gates the agent's real behavior.
data-flow · v1.8
Tracks where data may travel across actions — a secret source cannot reach a forbidden sink.
05
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.5The Warden. Kernel-boundary enforcement via seccomp-unotify.
v1.6Action-graphs. Pre-execution, compositional verification of agent plans.
v1.7Vertical stack. Verification bound to enforcement at the system boundary.
v1.8Data flow. Cross-action information-flow verification, with audited declassification.
v1.9Progress-safety. A load-time liveness proof — certified human-out-of-the-loop. current
06
VAREK
v1.9 · what's new
Safety, and now
liveness.
Through v1.8, VAREK proves safety: nothing unauthorized executes. But safety alone does not guarantee the system always has a legal, automated next move. Without that, "never requires a human" is a hope — a policy could deadlock in a state only a person could break.
v1.9 proves liveness too. At policy load, before anything runs, it certifies that every refusal resolves to an automated terminal in finitely many steps. Human-out-of-the-loop becomes a property the verifier certifies per policy — not a setting taken on faith. If it cannot certify, the system never reaches run time.
07
VAREK
The next move · 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 next line moves those cases into provable SATISFIED, raising the clear rate on safe work — while a hard invariant forbids ever turning an unsafe action into SATISFIED.
1
Verdict-distribution harness. Measure the clear rate on a realistic workload; gate every change on zero unsafe authorizations. planned
2
Bitvector fragment. Prove syscall flag/argument bits at the Warden boundary. Lowest audit cost. planned
3
Bounded string fragment. Prove path-prefix and host-allowlist predicates instead of refusing them — the headline reduction in over-refusal. planned
4
Bounded sequence fragment. Element-level reasoning over payloads, composed on the fragments above. candidate
// the invariant, never violated:
every extension may only move cases UNKNOWN → SATISFIED / UNSATISFIED.
none may ever move a genuinely unsafe action → SATISFIED.
08
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 patents cover the SMT decision-procedure layer, the Warden kernel architecture, and action-graph compositional policy decision. Patent-pending.
09
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
10