OPEN SOURCE — MIT

VAREK
————

PRE-EXECUTION AUTHORIZATION RUNTIME

An autonomous agent decides what it wants to do. VAREK decides whether it may — and proves it against declared policy before the action reaches the kernel.

Verified before the first action. Enforced at the kernel.

READ THE v1.21.1 RELEASE NOTES → SEE IT DECIDE
8 µs
MEDIAN DECISION · LIVE WARDEN
ZERO
UNSAFE ALLOWS · HARNESS GATE
THREE
VERDICTS · FAIL-CLOSED
MIT
OPEN SOURCE
// POLICY

Refused before
the first action runs.

A policy declares what an agent may do. The Warden holds every file open, lookup, connect and launch at the kernel boundary and resolves it against that policy before it runs.

● POLICY
# Rules are evaluated in order. First match wins.
# No match -> UNKNOWN -> suppressed -> DENY.

allow path /tmp/varek_allowed_
allow path /etc/ld.so.cache
deny path /etc/shadow
deny path /root/

allow host 127.0.0.1:8080
● WARDEN — LIVE DECISIONS
# one line per mediated call (condensed; timings illustrative)

file.open /tmp/varek_allowed_demo
raw=ALLOW final=ALLOW 242us

file.open /etc/shadow
raw=DENY final=DENY 20us

file.open /tmp/not_in_policy
raw=UNKNOWN final=DENY 21us

# the agent sees: Permission denied
// FEATURES

Three layers.
One guarantee.

⚖
Three-state decision
Every proposed action is discharged by an SMT decision procedure — bounded strings for the object, bitvectors for the open flags — and resolves to SATISFIED, UNSATISFIED or UNKNOWN. Only SATISFIED executes, and UNKNOWN is never coerced into a pass.
SMT DECISION PROCEDURE
✔
Every authorization checked
Each SATISFIED verdict carries a certificate, and the action runs only if a small, independently written checker accepts it. Every record is hash-chained, and checkpoints can be signed and anchored off the host, so whoever holds the log cannot quietly rewrite it.
CERTIFIED · TAMPER-EVIDENT
🛡
The Warden
Enforcement sits at the kernel boundary through seccomp-BPF and seccomp user-notify, on a default-deny allowlist. The agent runs unprivileged, and if the supervisor stops, the agent and everything it started stop too. A verdict is not advice the agent can decline to take.
KERNEL ENFORCEMENT
🔌
Decided connections
Each outbound connect is decided on the destination copied once, dialed by the Warden itself and handed to the agent as a connected socket. The agent's own network stays empty, so a second thread cannot swap the destination after the check.
v1.21
🕸
Whole-plan verification
The declared action-graph is verified before the first action runs, including data flow across actions. A secret source cannot reach a forbidden sink, even when each step looks safe alone. Steps can declare how they open a file, so read-only grants verify at the gate.
COMPOSITIONAL · v1.21.1
⏱
Progress-safety
A load-time liveness proof certifies that an agent can make safe progress unattended. A flow policy that can refuse without a bounded refusal budget is not certified, and the Warden refuses to start.
NO HUMAN IN THE LOOP (HOOTL)
// PLATFORM RISK

Platforms build agents.
VAREK checks every one.

🌐
Any agent, any platform
Agents run on many model providers, frameworks and in-house stacks. A platform's guardrail covers only its own agents. VAREK enforces one policy at the kernel boundary every agent's actions cross — beneath each platform's own guardrails, not in place of them.
VENDOR-NEUTRAL
🔍
The checker isn't the vendor
The decision is made and enforced outside the agent. The signed verdict stream and its CycloneDX 1.6 export can be verified without relying on the vendor that built the agent.
INDEPENDENT EVIDENCE
⛔
Built to refuse, not steer
Platform controls are built to keep agents working — they steer and score. VAREK refuses anything it cannot prove, including UNKNOWN.
FAIL-CLOSED
// ROADMAP

From spec to verified.

v0.1 - v1.0
Core Language
Compiler backend, LLVM compilation, Hindley-Milner type inference, standard library (261 functions), package manager. Stable at v1.0.
COMPLETE ✓
v1.1 - v1.5
The Warden
Kernel-enforced containment with fail-closed semantics: seccomp user-notify binding the policy evaluator to the Linux syscall boundary, a production supervisor in C (cross-process argument extraction, in-kernel verdict injection, latency measurement), and a fast-path matcher for the common case.
COMPLETE ✓
v1.6 - v1.8.2
Plans, Data Flow & the Refusal Breaker
The agent's planned action-graph is verified before execution begins; verification reasons across sequences of actions — where data originates and where it may go; and a non-bypassable loop bound stops a planner from resubmitting a refused plan forever.
COMPLETE ✓
v1.9 - v1.9.3
Progress-Safety & a Complete Boundary
A load-time liveness proof certifies human-out-of-the-loop operation per policy. The boundary is hardened and completed: io_uring refused, TOCTOU-safe file mediation, a default-deny syscall allowlist with the x32 bypass closed and a hard-deny set, and the agent's lifetime coupled to the supervisor's.
COMPLETE ✓
v1.12
Mediation Correctness
The verifier decides on the object it actually delivers: resolve-then-decide closes path-traversal, symlink and /proc/self escapes; a denied open has no side effect; the verdict stream is authenticated; inbound networking is refused. Threads, child processes and dynamically linked agents are supported. Adds CycloneDX 1.6 evidence export.
COMPLETE ✓
v1.13 - v1.15
The Verification Program, Shipped
An SMT decision procedure in the enforcement path over bounded strings and bitvectors, with read-only flag clauses and load-time rule reachability; suffix, contains and glob matchers; a verdict-distribution harness gated on zero unsafe authorizations; and a certificate for every authorization, checked by an independent checker before the action runs.
COMPLETE ✓
v1.16 - v1.17
Tamper-Evident Record & an Unprivileged Agent
A hash-chained, Ed25519-signed verdict stream anchored off the host; a bound on the work of every decision; a deployment preflight. The Warden's own key, anchor and log are refused by identity through any path; stat, access and readlink are decided like opens; the agent runs with no privileges.
COMPLETE ✓
v1.18 - v1.20
The Plan Gate in the Warden
The claims and the code agree: the Warden's --plan gate runs the data-flow check, the refusal breaker and the progress-safety proof. A refusal limit per session stops a planner that changes one step each time, and plan steps can carry fields the flow policy can match.
COMPLETE ✓
v1.21.0
Decided Connections
The Warden decides each outbound connect on the destination it copied once, dials it itself from outside the agent's empty network namespace, and hands the agent the connected socket. TCP, connected UDP and Unix sockets; tested with curl, Python and Node.js; 0 of 2,000 destination-swap attempts reached the denied side.
COMPLETE ✓
v1.21.1
Plan Steps Say How They Open
A file_open step may declare its open flags (open=read, or an access mode and flags), and the plan gate decides and certifies it with exactly those flags — so a plan that declares reading a read-only grant is authorized, as the runtime would allow. Anything malformed is UNKNOWN, never SATISFIED.
current
v1.21.2
Host Names Without Agent DNS
Policies name hosts. The Warden resolves the allowed names itself and shows the agent only those, so the agent never sends a DNS query and DNS cannot carry data out.
PLANNED
v1.11
Bounded Sequence Fragment
Element-level reasoning for the cross-action data-flow subsystem — collections modeled as a fixed N slots plus a length, composed on the string and bitvector fragments so its soundness inherits theirs.
CANDIDATE