VAREK

Kernel-enforced, proof-checked authorization for what an AI agent's process actually does.

Reporting vulnerabilities: private vulnerability reporting or SECURITY.md. Do not open public issues.

What VAREK is

VAREK decides whether an AI agent's planned actions are allowed before they execute, and enforces that decision at the kernel boundary.

An agent's intended actions are represented as an action-graph — a directed acyclic graph of planned actions. Before the agent starts, the Warden's optional --plan gate checks a declared action-graph: every step against the policy and, with --flow-policy, the data flowing along its edges. While the agent runs, the Warden pauses each file open, file lookup (stat, access, readlink), connect, program launch and datagram send at the kernel (via seccomp-BPF and seccomp user-notify) and decides it before the kernel carries it out. File opens, lookups and connects are decided by an SMT decision procedure: in the Warden, a purpose-built procedure for a decidable fragment — bounded strings for the object (prefix, exact, suffix, contains and glob matching), bitvectors for the open flags — that decides in microseconds with bounded worst case, is cross-checked against an off-the-shelf SMT solver, and returns UNKNOWN for anything outside its fragment rather than guessing. Every file open and connect it authorizes, and every lookup it decides, carries a certificate that a small, independently written checker must accept before the call takes effect. Lookups of the directories leading to an allowed path, and of descriptors the agent already holds, are answered without a decision. Since v1.21.0 a connect is decided on the destination the Warden copied once, and an allowed one is dialed by the Warden and handed to the agent as a connected socket; the agent's own network namespace stays empty. A datagram send that names a destination is refused whatever the policy says; a send with no destination goes to the peer of a connect the Warden decided. Every launch after the agent's own is refused too, unless the policy opts in with require warden 1.27 (v1.27.0): then each is decided, and the kernel's Landlock holds the agent to the programs the policy allows; from v1.27.1 the directories it may write are also mounted noexec, so nothing written during the run is launched or mapped executable. From v1.28.0 the agent can hold only placeholders for the credentials it uses: the egress proxy puts the value into a request only in the header an allowing rule names, on a request the Warden decided SATISFIED, and varek revoke refuses every later call of a run. From v1.28.1 every decision record says whom it was for: the user an identity provider vouched for, the agent, and the sub-agent that made the call, each sub-agent held in a control group of its own from its launch. From v1.29.0, sudo varek run -- claude (or another agent) runs with nothing set up first: VAREK writes a policy for the run, opens files as the agent's own user so the kernel's permissions hold as well as the policy, and a dry run records what a narrower policy would refuse, for varek policy suggest to draft from. From v1.31.0 a local MCP server is held to the rules written for it and none of the agent's, a call to a remote MCP server is decided by its method and tool, an MCP token reaches only the server it was issued for, and the verdict stream exports as OCSF events a SIEM can read. Every verdict is one of three — SATISFIED, UNSATISFIED, or UNKNOWN — and it fails closed: a paused call that cannot be proven allowed never runs. System calls the kernel filter admits without asking (memory, time, threads, and reads and writes on descriptors the agent already holds, whether the Warden opened them or the agent made them, such as sockets and pipes) run undecided, and the rest are refused outright.

The design premise is a clinical one: you do not deploy a system that is usually right when the cost of being wrong is unbounded. UNKNOWN is therefore a first-class verdict, not an error path — VAREK never coerces "cannot prove safe" into a pass.

VAREK has two layers, developed in sequence:

1. The Warden runtime — the verification and enforcement layer. It is where active development lives and where the verification thesis above is realized. Current release: v1.35.0.
2. VAREK the language — a statically-typed, LLVM-compiled language for AI/ML pipelines, where unsafe operations are not expressible in the first place. Stable at v1.0.

The runtime can protect any agent stack (LangChain, AutoGen, CrewAI, custom orchestrators), and it does not depend on the model provider or agent platform: the decision is made and enforced outside the agent, at the kernel boundary, and its evidence — the verdict stream and the CycloneDX 1.6 export — can be inspected without relying on the agent's vendor. The language is for pipelines you write fresh. They are useful independently and complementary together.

The verdict model

Every decision is total and three-state. There is no fourth outcome and no silent default.

Verdict	Meaning	Disposition
SATISFIED	Provably allowed under the policy, within the decidable fragment.	Proceed.
UNSATISFIED	A concrete policy violation, identified.	Refuse.
UNKNOWN	Cannot be decided either way within bounds.	Fail closed — never coerced to a pass.

A two-state allow/deny system must convert every UNKNOWN into a false allow or a false block. VAREK refuses that conversion. In the running agent an UNKNOWN is refused, like an UNSATISFIED (symmetric suppression). At the --plan gate with a --flow-policy, it goes to the deterministic disposition that policy declares, and the Warden refuses to start unless a check at load time certifies that every refusal ends in an automated outcome, so none needs a human to break a loop (see progress-safety, below). That refusal is what separates a verifier from a heuristic — nothing is SATISFIED unless it is provably safe.

Layer 1 — the Warden runtime

What it does

Warden sits between an agent framework and the operating system. Before contained code opens or looks up a file, connects, sends a datagram or launches a program, the Warden decides that call and enforces the verdict at the kernel; with --plan, the whole declared action-graph is also checked before the agent starts. Since v1.21 an allowed connect is dialed by the Warden itself and the connected socket handed to the agent, the way allowed files have been handed over since v1.12. This is structural containment — not a string-match denylist that falls to absolute paths, base64 encoding, or renamed binaries.

The runtime line has progressed well beyond simple syscall containment:

• v1.7 — cross-action data-flow verification. Reasoning across edges of the action-graph, not just per-action checks. Run by the Warden's --plan gate with --flow-policy since v1.18.0; through v1.17.0 it was a library with tests that the Warden did not call. Since v1.20.0 a plan step can declare fields besides its target, which the flow rules can match.
• v1.8.2 — bounded-refusal breaker. A loop bound in the trusted boundary, keyed by (session, action-graph signature), so a stuck planner cannot resubmit the same refused action-graph forever: after the policy's refusal budget, the outcome is a declared terminal (deny, or a pre-authorized action). Each verdict stays a pure function of (plan, policy); the breaker only interprets the sequence of verdicts. In the Warden since v1.18.0, with its counts kept across runs in a state file the agent cannot reach. Since v1.19.0 it also bounds each session (session_refusal_budget), so a planner that submits a different graph each time is stopped too.
• v1.9.0 — progress-safety / HOOTL. A load-time liveness proof that certifies human-out-of-the-loop operation per policy: for every non-authorizing verdict, a deterministic, automated terminal outcome is reachable in finitely many steps. "Never requires a human" becomes certified rather than hoped. Since v1.18.0 the Warden runs it on the --flow-policy at startup and refuses to start if it fails.
• v1.35.0 — Agent frameworks: plans from the framework. Through v1.34 a plan was a file nothing outside the tests wrote, checked once and never held to. From v1.35.0 varek plan generate writes an agent's plan from its framework (Amazon Bedrock AgentCore, IBM watsonx Orchestrate, LangGraph, the OpenAI Agents SDK, the Claude Agent SDK and Claude Code), the adapter itself confined by the Warden, and varek run --plan PLAN --hold-to-plan holds the run to it: a call the policy allows and the plan does not name is refused as the agent makes it. Plans name MCP calls, sub-agents and credentials; require plan refuses a run not held to one; pods name theirs under the node agent. The plan's records name it by its SHA-256 in the audit, OCSF and CycloneDX. 24 hours on a host (a DigitalOcean droplet, Ubuntu) with an OpenAI Agents SDK agent held to its generated plan under require plan: 1,439 turns, every one done; each of the 429 probes refused outside the plan, and nothing else refused but what every run refuses; the stream audited and its 31,711 OCSF events valid; memory flat. Reviewed by AI review agents. See RELEASE-v1.35.0.md.
• Through v1.32 the Warden ran inside the agent's container, with capabilities and a cgroup namespace a cluster's admission policy refuses. From v1.34.0 one Warden on each node (a DaemonSet) supervises each annotated pod's containers from outside them, so the agent's pod passes Pod Security's "restricted" level: the runtime hands the node agent each container's seccomp notifications (), and its calls are decided as on a host, with one signed, anchored stream per container. An NRI plugin (containerd 2.2+, CRI-O 1.35+) sets the Warden's own filter and puts a small launcher first to apply the launch set; a container it cannot carry, or does not adjust, does not run. The pod's network, stub resolver and egress proxy work in the pod; resources, an admission webhook, an OCSF exporter and a signed Helm chart, with OpenShift's constraints. Credentials, sub-agents, confined MCP servers, plans and the dry run are not carried in pods yet (planned for v1.36.0). 24 hours each on Amazon EKS and on single-node OpenShift with SELinux enforcing, every probe held and every stream audited. Reviewed by AI review agents. See .

See CHANGELOG.md for the full v1.0–v1.17.0 history.

Network

A supervised agent's network is decided connection by connection (v1.21). When it calls connect, the Warden copies the destination once, decides it against the policy's host rules with the SMT decision procedure (the independent checker must accept any ALLOW), dials it itself from outside the agent's network namespace, which has no working interface, and hands the agent the connected socket in place of its own, the way it hands over files. The kernel never reads the agent's copy of the destination, so a second thread cannot change it after the check. Every connection is logged, chained and signed like a file open.

allow host 10.20.0.15:443              # an address and port
allow host [2001:db8::15]:443          # IPv6
allow host 127.0.0.1                   # any port on this address
allow host unix:/run/fhir/gw.sock      # a Unix socket, by its canonical path
allow host api.salesforce.com:443      # a host name (v1.24, after `require warden 1.24`)

Covered: TCP and connected UDP over IPv4 and IPv6, Unix stream, datagram and seqpacket sockets named by a path. IPv6 destinations are decided and certified like IPv4 ones; dialing them was not exercised on the v1.21.0 release host (its kernel has no IPv6), where make test-v1210 reports that case as SKIPPED. Refused whatever the policy says: sends that name their own destination (an unconnected datagram), inbound connections, abstract Unix addresses, raw and other socket kinds.

Host rules may name hosts (v1.24). The Warden resolves every name a host rule names itself, refreshes each at its TTL, and records every lookup in the verdict stream. The agent reads an /etc/hosts view that lists only the allowed names, and every connect to port 53 is refused, so the agent sends no DNS of its own. A connect is decided on its address and on each allowed name that address belongs to; a loopback, link-local, unspecified, multicast or cloud metadata address is decided on the address alone, so only a numeric rule can allow it. A name decides where the agent connects, not which site it asks for there: an address on a shared content network also serves other sites, which the v1.26 egress proxy closes on the ports it proxies. See RELEASE-v1.24.0.md.

A rule may also allow every name under a domain (v1.25): allow host *.example.com:443 acknowledge=dns-channel. Those names are known only when the agent asks for one, so its lookups go to a stub resolver the Warden runs, and from there out of the host: the acknowledgment is required so the policy says so. Wildcards over domains where anyone can create a name are refused at load, each rule's names and lookups are budgeted (256 new names a run and 30 lookups upstream a minute by default, names= and rate= to change them), and every question is recorded. See RELEASE-v1.25.0.md.

With proxy on (v1.26), connects on the proxied ports (80 and 443 by default) go to an unprivileged egress proxy, and the Warden decides each on the name the client sends (TLS SNI, HTTP Host), not on the address. Names allowed only on those ports get synthetic addresses from 198.18.0.0/15, so the agent looks nothing up for them. A numeric rule still dials its address directly. proxy upstream http://HOST:PORT chains to your own egress proxy after the Warden has decided. In this mode only the ClientHello is read inside TLS. See RELEASE-v1.26.0.md.

With proxy inspect (v1.26.1), every request is decided too:

require warden 1.26
proxy inspect
allow host api.example.com:443
deny  request * https://api.example.com/v1/admin/**
allow request GET https://api.example.com/v1/models
allow request GET https://api.example.com/v1/files?limit=*
allow request POST https://api.example.com/v1/chat/completions max_body=256k

The proxy verifies the server, answers the agent with a certificate from a CA made for the run (added to the host's roots at the system bundle's paths, and named in SSL_CERT_FILE, NODE_EXTRA_CA_CERTS and JAVA_TOOL_OPTIONS), and holds each request until the Warden has decided METHOD scheme://host:port/path?query. A request no rule allows is refused with a 403, an allow rule without a ? allows no query, and a deny rule without one holds whatever the query. See RELEASE-v1.26.1.md.

VAREK decides where an agent may connect and, in inspecting mode, which requests it makes there. What it sends in them (headers, bodies beyond their length) is for your DLP tooling, which VAREK works alongside: an allowed request is a channel.

Installation

# Linux host (kernel-enforced containment requires Linux; see requirements below)
git clone https://github.com/kwdoug63/varek.git
cd varek
pip install -e ".[dev]"

Production requirements (for kernel-enforced containment):

• Linux with cgroups v2 mounted
• libseccomp Python binding (pyseccomp or python3-libseccomp)
• Unprivileged user namespaces enabled
• /sys/fs/cgroup/varek.slice writable by the test user

The C Warden (varek/v1_4) additionally requires CAP_SYS_ADMIN (run it as root or via sudo); it checks at startup and refuses to run without it. See varek/v1_4/README.md.

The runtime fails closed if these are unmet. The package installs and imports cleanly everywhere, but SeccompBpfBackend.is_available() returns an explanatory string on non-Linux hosts or environments without kernel support. No silent degradation.

Supported platforms

Each platform below is checked in CI; the job named is the one to read. "Each PR" means each pull request that touches the code the workflow watches. A release runs both matrices on its tag's commit and publishes nothing unless every cell passes (v1.36, D11).

Platform	What runs	CI job	When
Ubuntu 24.04, x86_64 and arm64 (host)	the Warden's build and its suites	warden-build.yml: Build the Warden with libseccomp + libsodium	each PR
RHEL 9 (host), tested on Rocky Linux 9	every host suite, in a VM	matrix-vm.yml: Rocky Linux 9 host: every suite	each PR and release
Amazon Linux 2023 (host, Linux 6.1)	every host suite, in a VM	matrix-vm.yml: Amazon Linux 2023 host: every suite	each PR and release
Kubernetes, CRI-O 1.35, 1.36 and 1.37, under runc and crun, amd64 and arm64	the Helm chart, on a kubeadm node	matrix.yml: CRI-O 1.35, runc, CRI-O 1.35, runc, arm64 (and the other five, each on both)	each PR and release
Kubernetes, containerd 2.2 and 2.3, amd64 and arm64	the Helm chart, on a kubeadm node	matrix.yml: containerd 2.2, runc, containerd 2.3, runc, each also …, arm64	each PR and release
Kubernetes, SELinux enforcing (CRI-O 1.35 on Rocky Linux 9)	the Helm chart, SELinux's denials counted	matrix-vm.yml: SELinux enforcing: CRI-O 1.35 on Rocky Linux 9	each PR and release
Kubernetes on kind, amd64 and arm64	the Helm chart; the suites under the node agent

On CRI-O, install the chart with --set runtime=cri-o. The node image is published for amd64 and arm64 as one image (v1.36), each architecture built and checked on its own runner, and the chart's DaemonSet runs on every Linux node of either.

Verify your installation

# Linux host or Codespaces
python verify_guardrails.py

This exercises every public entry point through an eight-step verification. In most environments (including GitHub Codespaces) steps 1, 2, 3, 5, 6 PASS and steps 4, 7, 8 SKIP with SeccompBpfBackend unavailable — cannot exercise kernel boundary. The SKIP pattern is itself a correctness property: the backend refuses to initialize rather than run without containment. To convert the three SKIPs to PASSes, run on a Linux host meeting the production requirements.

Quick start

Legacy (v1.1). varek_guardrails and the integration demos below run in the agent's own process and use none of the Warden. They are kept so existing copies keep working (v1.35, D10). For an agent built on a framework, varek plan generate writes its plan from the framework (varek/v1_4/adapters/README.md) and varek run --plan PLAN --hold-to-plan runs it under the Warden held to it.

import sys
from varek_guardrails import (
    SeccompBpfBackend,
    ExecutionPayload,
    IsolationError,
    default_python_policy,
    configure_backend,
    execute_untrusted,
    subscribe_telemetry,
)

# Arm the containment layer. Fails closed if kernel support is missing.
configure_backend(SeccompBpfBackend())

# Optional: stream PEP 578 audit events to your observability stack.
subscribe_telemetry(lambda event, args: print(f"[audit] {event}"))

# Run untrusted code under the default policy:
# 512 MB / 50% CPU / 64 pids / 30 s wall-clock / network denied / execve denied
payload = ExecutionPayload(
    interpreter_path=sys.executable,
    code="print(2 + 2)\n",
)

try:
    outcome = execute_untrusted(payload, default_python_policy())
    contained = (
        outcome.exit_code != 0
        or outcome.killed_by_signal is not None
        or outcome.violation is not None
    )
    print(
        f"contained={contained} "
        f"exit_code={outcome.exit_code} "
        f"wall_clock_s={outcome.wall_clock_s:.3f}s "
        f"stdout={outcome.stdout!r}"
    )
except IsolationError as e:
    # Raised only at the orchestration boundary (backend not configured,
    # policy malformed). Ordinary containment events surface on the outcome.
    print(f"orchestration error: {e}")

Integration demos

Numbered demos (legacy, v1.1: in-process, without the Warden; see the note above) apply the v1.1 containment layer to popular agent frameworks. Each follows the same Target / Vector / Defense pattern and runs end-to-end.

File	Surface
04-huggingface-smolagents-sandbox.ipynb	Hugging Face smolagents
05-openai-gpt4o-varek-hardened.ipynb	OpenAI GPT-4o tool-calling
06-crewai-gemini-ast-intercept.ipynb	CrewAI + Gemini
07-bare-metal-mobile-intercept.py	Edge inference
08-autogen-local-executor-intercept.py	Microsoft AutoGen
09-prefect-task-intercept.py	Prefect task orchestration
16-wandb-pipeline-verification.py	Weights & Biases / Weave evals

These are engineering demonstrations of containment patterns, not statements of customer relationships.

Layer 2 — VAREK the language

Why a new language

Modern AI pipelines stitch together four tools — Python for logic, YAML for configuration, JSON Schema for validation, shell for orchestration. Each format boundary erases type information; schema drift and silent coercion errors follow. VAREK replaces all four with one statically-typed language. Unsafe operations are not expressible, so a VAREK pipeline needs no runtime containment.

Syntax at a glance

-- Complete pipeline: schema, logic, and config in one file

schema ImageInput {
    path: str,
    label: str?,
    width: int,
    height: int
}

pipeline classify_images {
    source: ImageInput[]
    steps:  [preprocess -> embed -> infer -> postprocess]
    output: ClassificationResult[]
    config { batch_size: 32, parallelism: 8 }
}

fn preprocess(img: ImageInput) -> Tensor {
    load_image(img.path)
        |> resize(224, 224)
        |> normalize(mean=[0.485, 0.456, 0.406])
}

async fn infer(tensor: Tensor) -> RawOutput {
    let model = load_model("resnet50.varekmodel")
    model.forward(tensor)
}

The equivalent Python requires four files in two languages. The full language description is in the spec paper.

Core language features

Feature	Description
LLVM backend	Native code generation via ctypes bindings to libLLVM-20. SSA form, phi nodes, full optimization passes.
Hindley-Milner inference	Algorithm W, Robinson unification with occurs check, let-polymorphism. Types inferred across module boundaries.
Tensor types	First-class Tensor<T, D> with symbolic dimension tracking and compile-time shape checking.
Pipeline operator	|> for linear composition. x |> f |> g desugars to g(f(x)).
Schema types	Structural typing, optional fields, runtime SchemaValidator. Replaces JSON Schema and Pydantic.
Result types	Result<T> for errors-as-values. ? propagates errors without hiding them.
Native async	First-class async fn with channels, futures, parallel_map, mutex, atomic.
Python/C/Rust interop	import python::numpy as np — typed FFI for the existing ML ecosystem.

The varek CLI provides 20 commands (new, build, run, check, test, bench, repl, fmt, doc, install, publish, search, add, remove, update, clean, init, info, registry update, version). The standard library is 261 functions across 7 modules: var::io, var::tensor, var::http, var::async, var::pipeline, var::model, var::data.

How the layers compose

Your AI workload VAREK (.varek) Python agent code

typed, LLVM-compiled (LangChain, AutoGen,

unsafe ops inexpressible CrewAI, custom ...)

| |

|                          action-graph

|                                |

|                                v

|                    +-----------------------------------+

|                    | two-tier decision procedure       |

|                    |   decidable matcher (fast)        |

|                    |   + SMT for richer policy         | 

|                    |   -> SATISFIED /                  | 

|                    |      UNSATISFIED /                | 

|                    |      UNKNOWN                      |

|                    +-----------------------------------+

|                                |

|                                v

|                    +-----------------------------------+

|                    | Warden runtime                    |

|                    | kernel enforcement                |

|                    | seccomp user-notify (seccomp-BPF) |

|                    | fail closed                       |

|                    +-----------------------------------+

v

native binary (runs directly)

A VAREK pipeline is verified at compile time. Python agent code is verified per-action at run time and bounded at the kernel. The two layers address different risks at different points in the stack.

Roadmap

Runtime (verification + enforcement)

• v1.0–v1.5 — Warden supervisor, fail-closed semantics, linear rule evaluation, kernel-enforced containment
• v1.6 — C Warden adapter; public-repo cleanup; data room
• v1.7 — Cross-action data-flow verification
• v1.8.2 — Bounded-refusal breaker
• v1.9.0 — Progress-safety / HOOTL liveness proof
• v1.9.1 — Enforcement hardening: io_uring closed; TOCTOU-safe file mediation (race-harness leaks → 0); connect/execve deny-only
• v1.9.2 — Mediation completeness: default-deny allowlist; native-ABI/x32 lockdown; hard-deny set; CLONE_NEWUSER denial; live-Warden integration + conformance validation
• v1.9.3 — Lifecycle coupling in the live Warden: PID-namespace isolation, death-signal coupling, fork-race guard, pidfd watch; crash test
• v1.12 — Mediation correctness: resolve-then-decide (traversal / symlink / /proc/self), audit-log integrity, datagram-egress mediation; authorization-evidence export in the CycloneDX 1.6 format
• v1.12.1 — Side-effect-free denials (resolve, decide, then open), authenticated verdict stream, inbound networking refused
• v1.12.2 — Threads and child processes: clone3 answers ENOSYS (libc falls back to the filtered clone), wait4/waitid, narrow ioctl allowlist, kill report; bootstrap exec granted once per run
• v1.12.3 — Dynamically linked agents: follow symlinks and decide on the canonical path; /proc/self mapped to the agent
• v1.12.4 — The gate authorizes file opens again (decide on the lexically canonical declared path)

Language

• v0.1–v0.4 — Grammar + parser, HM type system, LLVM backend, standard library
• v1.0 — Stable release, package manager, RFC process

The verification program (v1.10 / v1.11)

Partly shipped. No v1.10 or v1.11 tag exists: the program's releases ship as v1.13.0, v1.14.0 and v1.15.0 so version numbers keep increasing (marked below); the rest is planned or candidate work. v1.12 (mediation correctness) shipped ahead of the program and does not touch it. Shipped behavior is in CHANGELOG.md.

The post-v1.9 program has a single goal: migrate cases out of the UNKNOWN verdict into a provable verdict, raising the clear rate on safe agent actions — under a hard invariant that no extension may ever move a genuinely unsafe action into SATISFIED. "Cannot prove safe" stays UNSATISFIED/UNKNOWN.

The program proceeds by adding small, individually-auditable decidable fragments, each with one named soundness obligation and the trusted code it introduces:

• v1.10 step 1 — verdict-distribution harness + corpus. The measurement baseline. Hard gate: zero unsafe authorizations across the corpus. Shipped in v1.13.0 with a synthetic seed corpus; a customer-derived corpus is outstanding.
• v1.10 step 2 — bitvector fragment. Decidable reasoning over fixed-width syscall flag/argument bits. Lowest audit cost. Shipped in v1.13.0.
• v1.10 step 3 — bounded string fragment (headline). Length-bounded path-prefix and host-allowlist predicates made provable instead of refused. Shipped: prefix/equality in v1.13.0; suffix, contains and globs in v1.14.0.
• v1.11 candidate — bounded sequence fragment. Element-level reasoning for the cross-action data-flow subsystem, composed on the fragments above.

Race-free network mediation (a supervisor-dials-and-injects path replacing the v1.9.1 deny-only posture for connect) shipped in v1.21.0 and host names (stage 2) in v1.24.0, wildcard names in v1.25.0, and the egress proxy in SNI mode (stage 3) in v1.26.0, and its inspecting mode, with rules on each request's method, path and query, in v1.26.1. Decided program launches, held by a Landlock execute ruleset built from the policy, follow in v1.27.0, and the policy's writable directories mounted noexec in v1.27.1. Credential release, with the agent holding only placeholders, and revocation follow in v1.28.0, and the on-behalf-of chain in every decision record in v1.28.1. The default-deny syscall allowlist closing the alternate-ABI and variant-syscall bypass classes shipped in v1.9.2, and supervisor/target lifecycle coupling shipped in the live Warden in v1.9.3.

Design and auditor notes live in docs/verification/: the harness spec, corpus schema, and one note per fragment.

Testing

Language test suites, as each archived release runs them (counted for v1.18.0, Python 3.11; through v1.17.0 this table said 109 tests for v0.1 and 659 passing in all). The v0.1–v0.4 releases are zip files in archive/; v1.0 is in varek-v1.0/:

Component	Tests	Passing
v0.1 — Lexer + Parser + AST	91	88 (2 fail; 1 hangs)
v0.2 — Type System + HM Inference	163	163
v0.3 — LLVM Codegen	97	97
v0.4 — Standard Library	182	173 (9 fail: unfinished syn:: to var:: rename)
v1.0 — Package Manager + REPL	108	108
Total	641	629

Runtime test suites are version-scoped and run clean under -fsanitize=address,undefined — e.g. the v1.8.2 breaker (19/19) and the v1.9 progress-safety verifier (10/10), both in make -C v1_7 check since v1.18.0. v1.9.1 enforcement is measured directly by a TOCTOU race harness (tests/seccomp_toctou_harness.c): in three runs of 20,000 attempts on a 2-vCPU host, approve-then-continue leaked the protected file 1,848 to 1,889 times and resolve-and-inject leaked it 0 times (tests/toctou_results_v1.18.0.txt; the count depends on the host). io_uring is denied by the live Warden filter (varek/v1_4/tests/test_v14_filter, v1.18.0; from v1.21 its creation answers ENOSYS rather than killing, so Node.js runs). Decided connections (v1.21) are tested with real clients (curl, Python requests, Node.js) and a destination-swap race: 2,000 attempts, 0 reached the denied side (make test-v1210). Inspecting mode (v1.26.1) is tested with Python, curl, Node.js and Java against servers that log what reaches them, and with forged streams the audit must refuse (make test-v1261, 193 checks). Decided launches (v1.27.0) are tested with real launches, a compile, a measured table of what the kernel's Landlock refuses, two threads launching at once, and forged streams (make test-v1270, 164 checks). The noexec mounts (v1.27.1) are tested with copies of host libraries the agent must fail to load, the agent's own view of its mounts, the host changing a writable path during the run, and forged streams (make test-v1271, 73 checks). Credential release (v1.28.0) is tested against stand-ins for Vault and AWS Secrets Manager (which check each request's signature), a TLS server that logs what reaches it, a run revoked mid-run, a hard link and a bind mount of a credential file, and forged streams (make test-v1280, 168 checks). The on-behalf-of chain (v1.28.1) is tested against a stand-in identity provider and SPIFFE authority (each check of a token or SVID failing on its own), sub-agents that fork, double-fork, use threads, nest and fail to launch, a token expiring mid-run, and forged streams (make test-v1281, 208 checks). varek run (v1.29.0) is tested with agents opening and changing files as their own user, the baseline and each profile, dry runs of every kind of call and of what stays refused, drafts varek policy suggest writes and runs under them, and forged streams (make test-v1290, 316 checks); make crosscheck-profiles cross-checks the baseline with each profile, and tests/profiles_v1290.sh runs the real agents' CLIs against their profiles. MCP servers, calls and tokens and the OCSF export (v1.31.0) are tested with confined servers and their children, a stand-in MCP server and authorization server, every call and token form the review found, the events validated against the vendored OCSF schema, and forged streams (, 317 checks). Build and run with in the relevant version directory. Containment verification: (see above).

Security

Reporting vulnerabilities. Do not open public issues. Use GitHub private vulnerability reporting or SECURITY.md. Reports receive acknowledgment within 72 hours.

Threat model and trusted computing base. Adversary models, in-scope guarantees, and out-of-scope conditions are documented in docs/security/threat-model.md; the per-component trusted-vs-verified status of the verification chain is in docs/security/TRUSTED-COMPUTING-BASE.md. The cross-action data-flow threat model is in docs/security/threat-model-dataflow.md. The runtime fails closed on unsupported platforms and denies boundary syscalls at the kernel, not via string matching or audit hooks. As of v1.12 the Warden filter is default-deny (an explicit allowlist, native ABI only, with a hard-deny set that includes io_uring_enter and io_uring_register, while io_uring_setup answers ENOSYS from v1.21 so that Node.js falls back to epoll); since v1.21 each outbound connect is decided and dialed by the Warden, which hands the agent the connected socket (an agent's own network namespace stays empty); and the agent runs in its own PID namespace, so it and everything it spawned die with the supervisor. The per-class status is in docs/security/bypass-classes.md.

v1.1.0 fix. Resolved a subprocess-escape weakness in v1.0's audit-hook-based containment (issue #223, reported by @dengluozhang). See VAREK_v1.1_SECURITY_UPDATE.md.

Architecture review. External review by QEEK-AI addressed AST-gate framing (documented as UX-only, not a security boundary), a libc-binding fallback bug, and platform-gating CI coverage (now macOS, Windows, Linux).

Documentation

• Spec paper: varek-spec-paper-v1.32.0.md — language and runtime specification, design rationale, the verdict model
• VAREK Enterprise on AWS: docs/aws-deployment-guide.md — deploying and operating the AWS Marketplace image
• Security: docs/security/threat-model.md, docs/security/TRUSTED-COMPUTING-BASE.md, docs/security/bypass-classes.md, RELEASE-v1.31.0.md, RELEASE-v1.29.0.md, RELEASE-v1.28.1.md, RELEASE-v1.28.0.md, RELEASE-v1.27.1.md, RELEASE-v1.27.0.md, RELEASE-v1.26.1.md, , , , , , , , ,

Community

• Discussions: github.com/kwdoug63/varek/discussions
• Issues: github.com/kwdoug63/varek/issues
• Releases: github.com/kwdoug63/varek/releases

License

VAREK is open-source software licensed under the MIT License. Copyright (c) 2026 Sober Agentic Infrastructure, Inc. See NOTICE.

Trademarks

CycloneDX is a trademark of the OWASP Foundation. VAREK and Sober Agentic Infrastructure, Inc. are not affiliated with, endorsed by, or certified by the OWASP Foundation or the CycloneDX project. The CycloneDX name is used only to describe interoperability with the openly published CycloneDX format (standardized as ECMA-424, with Apache-2.0-licensed schemas). All other product names and marks are the property of their respective owners.

Examples

• Sandboxing an agent that downloads media — Warden-supervised media fetch with a policy auto-generated by setup.sh. Framework-agnostic (Hermes Agent, LangChain, etc.) and LLM-agnostic.