Vaked declares. Nix materializes. OTP supervises. Zig enforces. eBPF testifies. CrabCC indexes. Surfaces reveal.

Vaked

A language that describes what an AI system is allowed to do — and a compiler that proves it before anything runs.

Research Snapshot · June 2026 · Pre-release

What is this?

Vaked is a safety language for AI systems. You write down what each part of your system can do — read files, make network calls, spawn processes — and the compiler checks, mathematically, that nothing exceeds its permissions. Then it turns your declaration into a real, running system on a dedicated server.

📝

Write Once, Prove Once

One file describes your entire system: what runs, what it can touch, who it talks to. No scattered config files. No YAML drift.

🔒

Permissions Are Checked Before Anything Runs

The compiler proves that no component can do anything you didn't explicitly allow — before a single line of code executes.

🪵

Everything Is Witnessed

The Linux kernel itself testifies what happened. There's an unforgeable log. If the kernel says it didn't happen, it didn't.

Why does this matter?

AI agents are starting to do real work: writing code, sending emails, managing servers. The question isn't if they'll be given authority — it's how much, and whether we can prove they won't exceed it.

Today, most AI systems are configured with hand-written YAML files and runtime checks. Mistakes are caught when something breaks — or worse, when something doesn't break but quietly exceeds its permissions. There's no proof. There's no audit trail you can trust. There's no single source of truth.

Vaked changes that. It makes authority explicit, checkable, and provable — at the level of a mathematical guarantee, not a policy document.

The analogy

If a regular config file is like writing house rules on a sticky note, Vaked is like having an architect certify the blueprints — and then having the building inspector live in the walls.
— from the project documentation

How it works

A Vaked system goes through four stages, from idea to running reality:

① Declare
Write one .vaked file
describing permissions
and structure
→
② Check
Compiler proves
no permission violations
exist
→
③ Lower
Produces real configs:
Nix, Zig, eBPF policies,
audit log setup
→
④ Run
Deploys to bare-metal
server. Kernel enforces.
Everything logged.
Technical detail: what does the compiler actually check?

The type system enforces two rules for every component in the system:

  1. Use Check: every action a component takes must be covered by a permission it was granted. If component A tries to read a file it wasn't granted access to, the compiler rejects the declaration.
  2. Attenuation Check: when component A delegates authority to component B, B can never receive more authority than A had. Permissions only shrink along delegation chains — they never grow.

This is called POLA — Principle of Least Authority — and Vaked enforces it at compile time, not runtime. The check is mathematically decidable: it always terminates with a yes/no answer, no edge cases.

What makes it different

🔐 Compile-time proof, not runtime hope

Most systems check permissions while running. Vaked proves they're correct before anything starts. No permission error can occur at runtime that wasn't caught at compile time.

🧬 One source of truth

One Vaked file replaces scattered config files across multiple systems. Change it in one place, regenerate everything consistently. No drift.

🪵 The kernel is the witness

eBPF — Linux kernel technology — records every action. Not an agent's self-report. Not a log file that can be edited. The kernel itself is the authoritative witness.

🔗 Tamper-evident audit chain

Every event is hash-chained. Every compilation produces a provenance.json linking source code → compiled artifacts. You can trace any running system back to its exact declaration.

📐 Deterministic

Same declaration → same result, every time. Byte-identical artifacts across repeated runs. Verified at 100,000 concurrent workers (273ms avg parse time).

🤖 Self-operating

The project is maintained by a fleet of 10 AI agents running on GitHub Actions — reviewing code, managing merges, labeling issues, posting updates. The agents are themselves declared in Vaked.

What's built, what's next

ComponentStatusPlain-language meaning
Language & Grammar Done The language exists. You can write .vaked files today: 29 kinds of things you can describe (servers, networks, permissions, workflows).
Compiler (Python) Done vakedc: reads your .vaked file, checks permissions, produces real configs. Standard library only — no external dependencies.
Compiler (Zig) Early A faster, cache-native version in Zig. Parser works; checker and lowerer in progress.
eBPF Membrane Done First vertical slice: network egress policy declared in Vaked → compiled → loaded into kernel → enforced. Real eBPF, real kernel.
Agent Fleet Live 10 AI agents actively operating the repo on GitHub Actions — reviewing PRs, managing merges, posting updates.
Wire Protocol (RFCs) RFCs Drafted 7 RFCs define how daemons talk to each other. Implementation starts June 24.
Runtime Daemons Stubs Python reference implementations exist for the main daemons (network guard, event log, memory, sandbox). Production Zig versions not yet built.
Full Deployment Planned The vakedos server exists (EPYC 4345P, 256GB RAM). No daemons deployed to it yet. Target: end-to-end smoke test later this year.
Research Paper Finalizing Arxiv upload targeted for July 1–8, 2026.

Safety guarantees — what's proven and what's not

Vaked makes specific, bounded claims about what it can guarantee. It's equally explicit about what it cannot guarantee. This clarity is part of the design.

✅ Vaked DOES guarantee

  • No component can use a permission it wasn't granted (proven at compile time)
  • Permissions only shrink along delegation chains — never grow
  • The permission check always finishes; no infinite loops
  • Same input always produces identical artifacts (reproducible builds)
  • Every artifact traces back to its source declaration (provenance)

❌ Vaked does NOT guarantee

  • Runtime enforcement — that's the kernel's job (eBPF)
  • Secret management — Vaked doesn't handle passwords or keys
  • Protection if root authority is compromised
  • Timing attacks or side-channel attacks
  • OS or hypervisor exploits

The philosophy: Vaked proves what can be proven at the language level. Everything else is delegated to battle-tested layers (Linux kernel, eBPF, NixOS) that have their own security models. No single layer claims to solve everything.

The project runs itself (mostly)

The Vaked repository is operated by a fleet of 10 AI agents — not as a gimmick, but as the first dogfooding target for the language. The agents review code, manage the merge queue, label issues, coordinate releases, and post updates. Their actions are logged to a hash-chained event ledger.

The notable part: the SWE agent (software engineering agent) can take an issue labeled agent, write a plan, produce code changes, get reviewed by another agent, and open a pull request — all without holding a GitHub token during the code-writing phase. The broker step that creates the PR is the only part with write access. This is POLA in practice.

Meet the agent fleet (10 agents)
ralphSurfaces the most important open decision every 3 hours
pr-reviewReviews every pull request (7-perspective council, never blocks merge)
@vaked-ciResponds to maintainer comments on PRs
doc-keeperChecks that documentation references are valid and up-to-date
yardmasterConductor for the merge train — builds dependency graphs, merges safe PRs
vaked-telebotTelegram bot for interactive control (workflow dispatch, CI checks)
label-taggerAuto-labels issues and PRs from the project taxonomy
provostProduct-owner coordination — links issues to goals, creates epics
swe-afFull software engineering agent: plan → code → review → publish
social-postPosts development updates to Mastodon (as "Carcin")

Where we are on the timeline

Phase 0
Scaffold
Monorepo, dev shell,
vakedos host config
Phase 1
Language + Compiler
Grammar v0.3, type system,
vakedc: parse→check→lower
Phase 2
Wire Protocol
7 RFCs drafted.
Implementation starts Jun 24.
Phase 3
Runtime Daemons
Stubs exist. First daemon
design cycle open.
Phase 4
Materialize
Deploy to vakedos.
Kernel enforces. Surfaces reveal.
Phase 5
Language v1
Stable grammar. Self-hosting.
Published reference.

We are roughly at the Phase 2/3 boundary. The language and compiler are real and tested. The wire protocol is designed and awaiting implementation. The runtime daemons have reference implementations but not production builds. The path to a running deployment is clear but not yet complete.

At a glance

29
Kinds of things you can describe in the language
2
Compiler implementations (Python + Zig)
8
Types of artifacts one declaration produces
7
Protocol RFCs (wire format, crypto, multi-agent)
10
AI agents running the repo
100k
Workers verified at 273ms avg parse time
~19
Real-world example declarations
120+
Documentation artifacts across the project

What kind of feedback helps

This is a research project seeking peer review. The kinds of questions we're trying to answer:

🎯 Is the problem clear?

Does "prove what AI systems are allowed to do before they run" make sense as a goal? Is it explained well enough for someone who doesn't write compilers?

🔒 Are the safety claims honest?

The project is explicit about what it can't guarantee. Does this clarity build trust, or does it raise concerns?

📐 Is the scope right?

Language + compiler + protocol + daemons + agents: is this too much for one project, or does the integration add value that pieces alone wouldn't?

🤖 Are the agents credible?

A fleet of AI agents operating the repo — does this read as genuine dogfooding or as over-automation? Where's the line?