Vor

A BEAM language designed as a compilation target for AI coding agents — with verified state machines, protocol checking, chaos testing, and compiler-generated telemetry

Named for the Norse goddess who witnesses oaths. Vor programs are oaths about system behavior — declared, witnessed by the compiler, and enforced. And when an oath was never actually tested, Vor says so.

GitHub

Why

AI agents are writing more and more code. They’ll inevitably build distributed systems. And they’ll produce that code faster than humans can review it.

We need compilers that catch what human review would miss. That includes a failure most tools can’t see: a check that passes without ever engaging the behavior it claims to cover.

The BEAM already provides process isolation, supervision, and distributed message passing — eliminating entire classes of bugs. Vor adds a checking layer: state machines, protocols, invariants, and chaos scenarios declared in one source file, read by three tiers of tooling:

mix compile        →  proves local safety properties        (milliseconds)
mix vor.check      →  finds multi-agent counterexamples     (seconds)
mix vor.simulate   →  chaos-tests real BEAM processes       (minutes)

An AI agent writes one file. Three tiers check it. The compiled binary is a standard OTP process, pre-instrumented with telemetry — no separate spec, no instrumentation code.

The part that matters: Vor tells you when it checked nothing

A checker that returns “✓ Proven” over a state space where the property’s subject can’t exist is sound, honest about its bounds, and useless — and most tools can’t tell the difference. Vor can, because it knows what your program declared and compares that against what was actually reached.

Every invariant reports two axes:

Axis	Values	Meaning
Strength	`proven` / `bounded` / `monitored`	How strong is the evidence
Relevance	`substantive` / `vacuous` / `unexercised`	Did the check engage with anything

✓ Proven    "no grant when held"    substantive   (subject true in 2 of 4 states)
⚠ Bounded   "at most one leader"    VACUOUS       (subject `role == :leader` never true)
⚠ Monitored "breaker recovers"      UNEXERCISED   (`half_open` never reached)

A proven-tier invariant whose subject is unreachable is a compile error, not a warning. The simulator carries the same discipline: a run whose fault injection degraded reports UNDER-TESTED, never a clean pass. Both tiers report declared-vs-observed coverage — which declared states, handlers, and messages were actually reached.

This is what a language buys that a library can’t: detecting that a check engaged with nothing requires a machine-readable declaration of what “something” would have been.

What it looks like

agent LockManager(lock_timeout_ms: integer) do
  state phase: :free | :held
  state holder: atom
  state wait_queue: list
  state auth_token: binary sensitive

  protocol do
    accepts {:acquire, client: atom, priority: integer} where priority >= 1 and priority <= 10
    accepts {:release, client: atom}
    emits {:grant, client: atom}
    emits {:queued, position: integer}
    emits {:ok}
  end

  on {:acquire, client: C, priority: P} when phase == :free do
    transition phase: :held
    transition holder: C
    emit {:grant, client: C}
  end

  on {:acquire, client: C, priority: P} when phase == :held do
    transition wait_queue: list_append(wait_queue, C)
    qlen = list_length(wait_queue)
    emit {:queued, position: qlen}
  end

  on {:release, client: C} when phase == :held do
    is_empty = list_empty(wait_queue)
    if is_empty == :true do
      transition phase: :free
      transition holder: :nil
      emit {:ok}
    else
      next_client = list_head(wait_queue)
      transition wait_queue: list_tail(wait_queue)
      transition holder: next_client
      emit {:ok}
    end
  end

  safety "no grant when held" proven do
    never(phase == :held and emitted({:grant, _}))
  end

  liveness "lock released eventually" monitored(within: lock_timeout_ms) do
    always(phase == :held implies eventually(phase != :held))
  end

  resilience do
    on_invariant_violation("lock released eventually") ->
      transition phase: :free
      transition holder: :nil
  end
end

The safety invariant is proven at compile time — and rejected if it turns out to be vacuous. The where constraint rejects invalid input before handlers run. The sensitive field is redacted in telemetry. The liveness invariant is monitored at runtime with automatic recovery, and the monitored tier reports when its deadline fires and whether recovery succeeded. Every state transition and message generates telemetry. This compiles to a standard OTP gen_statem.

Multi-agent checking

Wire agents together and mix vor.check explores message interleavings within configured bounds:

system RaftCluster do
  agent :n1, RaftNode(node_id: :n1, cluster_size: 3)
  agent :n2, RaftNode(node_id: :n2, cluster_size: 3)
  agent :n3, RaftNode(node_id: :n3, cluster_size: 3)

  connect :n1 -> :n2
  connect :n1 -> :n3
  connect :n2 -> :n1
  connect :n2 -> :n3
  connect :n3 -> :n1
  connect :n3 -> :n2

  safety "at most one leader per term" proven do
    never(exists A, B where A.role == :leader and B.role == :leader
                            and A.current_term == B.current_term)
  end
end

mix vor.check is a bug-finder first. Finding a counterexample is fast — often under a second. Exhaustive verification is available too, but only at small bounds: the state space explodes with message-queue depth, and it never runs during mix compile.

That invariant has a history. The original version — “at most one leader,” globally — reported ✓ Proven (1,001 states). The result was vacuous: the explorer wasn’t firing election timeouts, so no node ever became a leader. Once the model was honest, the checker found a counterexample in 0.16 seconds — and it turned out the invariant itself was wrong (Raft guarantees one leader per term; a stale leader legitimately coexists with its successor until it steps down). Two errors, and the first hid the second. That’s why relevance reporting exists — the full account is in the repo’s evidence directory.

Chaos testing

Chaos testing exercises real compiled code under failure — catching implementation bugs, timing issues, and recovery failures the model checker can’t reach. It’s also structurally immune to vacuity: there’s no abstract model to be empty. Real processes either did the thing or didn’t, and the coverage report says which.

mix vor.simulate --partition --delay --workload 10

Starts real BEAM processes, injects real failures, checks invariants against live state:

Kill agents randomly, let supervisors restart them
Partition connections via proxy processes
Delay messages for configurable durations
Generate client workload from protocol declarations
Check invariants periodically against live state
Report declared-vs-observed coverage, and flag degraded runs as UNDER-TESTED
Seeded inputs: a given seed reproduces the same fault schedule and workload (scheduler interleaving is not controlled, so replay is highly reliable rather than byte-for-byte)

For BEAM-native systems, no external chaos infrastructure is needed — the BEAM provides failure injection as function calls.

Auto-generated telemetry

The compiler knows every state field, message type, and transition. It generates telemetry calls in the compiled bytecode — no instrumentation code in the source file.

Event	Fires on
`[:vor, :agent, :start]`	Agent initialization
`[:vor, :message, :received]`	Handler invocation
`[:vor, :transition]`	State field change (sensitive fields redacted)
`[:vor, :message, :emitted]`	Reply, send, or broadcast
`[:vor, :constraint, :violated]`	Protocol constraint rejection
`[:vor, :monitored, :deadline_exceeded]`	Monitored invariant deadline expiry
`[:vor, :backpressure, :rejected]`	Queue limit reached

Attach any :telemetry backend and every agent is observable. This same stream feeds simulation coverage — telemetry generated from the declaration is how coverage knows what to look for.

How it fits with Gleam

Vor is designed as a two-language stack:

Vor — coordination logic: state machines, protocols, invariants, checking, chaos testing, telemetry
Gleam — data processing when needed: type-safe transformations called through validated extern gleam blocks

The extern boundary fails closed: the checker never claims to verify code it can’t analyze.

Design principles

The spec is the program. No separate specification. No drift between what’s checked and what runs.

Guarantee tiers are explicit — on two axes. proven / bounded / monitored for strength; substantive / vacuous / unexercised for relevance. The compiler fails closed: it never claims to verify what it can’t, and it never claims a check meant something when it didn’t.

Observable by default. The compiler generates telemetry from the program’s structure.

Input validated at the protocol level. where constraints reject invalid messages before handler code runs.

Sensitive data declared. Fields marked sensitive are redacted in telemetry.

Failure is first-class. Resilience handlers define recovery; the monitored tier reports when they fire and whether recovery succeeded.

Honest about limits. Multi-agent exhaustive checking is intractable beyond small bounds; value-and-time-rich invariants (rate windows, per-item guarantees) are not yet expressible. KNOWN_ISSUES is part of the product.

The BEAM is the foundation. Thirty years of production-proven concurrency, fault tolerance, and distribution.

VorDB — a CRDT-based distributed database built with Vor for coordination and Gleam for data processing
Tyn — a minimal Rust microkernel that runs the BEAM on bare metal (no Linux). Vor + Tyn is the long-term vision: verified distributed systems on a purpose-built kernel.

500+ tests · 9 property-based test suites · Generated codegen-conformance matrix · MIT License

Vor

Why