Vor compiles to OTP gen_server/gen_statem. You write agents with declared states, message protocols, and safety invariants. The compiler proves the invariants, a model checker explores multi-agent message interleavings, and a chaos simulator stress-tests real BEAM processes under failure.
mix compile → proves safety properties (milliseconds)
mix vor.check → model-checks multi-agent invariants (seconds)
mix vor.simulate → chaos-tests real BEAM processes (minutes)
What it looks like
agent LockManager(timeout_ms: integer) do
state phase: :free | :held
state holder: atom
state 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 {:ok}
end
on {:acquire, client: C, priority: P} when phase == :free do
transition phase: :held
transition holder: C
emit {:grant, client: C}
end
on {:release, client: C} when phase == :held do
transition phase: :free
transition holder: :nil
emit {:ok}
end
safety "no grant when held" proven do
never(phase == :held and emitted({:grant, _}))
end
end
The safety invariant is proven at compile time — the program is rejected if any reachable state violates it. The whereclause rejects invalid input before handlers run. sensitive fields are redacted in telemetry. This compiles to a normal gen_statem.
The key design decision
The model checker and code generator share the same intermediate representation. What the checker verifies is what the codegen compiles to BEAM bytecode. No separate spec, no drift.
A three-node Raft consensus is bounded-verified (leader uniqueness) in 1,001 states with symmetry reduction, under one second.
What else it does
-
Chaos simulation — kills real BEAM processes, partitions messages via proxies, generates workload from protocol declarations. All seed-reproducible. No external chaos infrastructure needed.
-
Auto-generated telemetry — the compiler knows every transition and message, so it generates
:telemetry.executecalls in the bytecode. Zero instrumentation code. -
Gleam externs for data processing the native expression language can’t handle, with a type-validated boundary.
Status
394 tests, 9 property-based suites, zero warnings. Five fully native examples (lock, circuit breaker, Raft, G-Counter CRDT, rate limiter). VorDB is the first real consumer — a CRDT database using Vor for coordination and Gleam for data processing.
Known limitations: expression language is limited (complex logic needs Gleam externs), safety only (no liveness yet), bounded verification (reports honestly when bounds are reached), no external users yet.
Why
I work on telecom systems where protocol bugs affect millions of subscribers. In my opinion, the BEAM has been the right runtime for decades. Verification has been the missing piece — TLA+ exists but requires a separate spec that drifts. Vor makes the spec and implementation the same file.
Code: github.com/vorlang/vor — MIT license. Happy to answer questions !
With AI agents writing more and more code, I think verification that’s built into the compiler — not bolted on as a separate practice — is going to matter a lot more. The code is being produced faster than humans can review it.