Vertep

Statecharts · Actors · Agents · Proofs

Vertep

Statecharts that run as durable actors, write down every step they take, let a language model choose only among the moves the chart allows, and agree step for step with a model proven in Lean.

Begin here See the examples Why deterministic agents

A theatre in a box

The vertep is the travelling puppet theatre of Ukrainian Christmas: a wooden box of two tiers, carried from house to house behind a star on a pole, with the goat dancing among the carollers. Its puppets cannot wander. Each moves along a slot cut into the stage floor, and the puppeteer, however clever, can only choose which slot a puppet takes next.

Vertep the library is built the same way. A chart is the stage with its slots. An actor is a puppet that moves only along transitions. A guard, a person or a language model may choose the next move, but none of them can cut a new slot. And the whole play is written down, so it can be performed again, exactly, without the puppeteer.

Read: The shape of behaviour →

A chart as a stage: states connected by transitions, with a decide state where the decider picks one of the offered moves idle decide vt:decide tooling human done task call_tool escalate finish vt:reply
Plate I. The slots of the stage. The decider picks among the offered transitions only.

Six pillars

One deterministic core, and around it everything a long-lived, auditable process needs.

I

Full SCXML

The W3C SCXML algorithm in full, checked against the W3C conformance suite. Write charts in SCXML, YAML or the statechart! macro; all lower to one typed IR.

Writing charts →
II

Durable actors

Virtual actors addressed by IRI. Every accepted input is journaled before it is processed, with compare-and-set appends, a transactional outbox and durable timers.

The runtime →
III

Deterministic agents

At a vt:decide state an LLM, a person or a guard picks among the enabled events. Decisions and model results are journaled, so a run replays without any model.

Agents →
IV

Charts as RDF

Every chart projects losslessly to RDF 1.2 with SHACL shapes. Its version is the hash of its canonical form, and journals can be queried with SPARQL, as of any moment.

RDF and versions →
V

Anywhere it must run

Clusters with leased shards over QUIC, federation across trust boundaries with DIDs and relay mailboxes, and the same core in the browser through WebAssembly.

Cluster, federation, browser →
VI

Proven in Lean

A Lean model of the semantics replays the Rust traces as a differential oracle. Decider safety, grant enforcement and legal configurations are theorems, not hopes.

Verification →

The way of one event

Nothing nondeterministic touches the core. Time, randomness, model output and the network arrive only as events in a mailbox, and each one is written to the journal before the pure step function sees it.

step takes a configuration, a datamodel and an event, and returns the next configuration and a list of effects. The shell carries out the effects: it sends messages, arms timers and asks deciders. Their answers come back as new events.

So the journal is the whole truth of an actor. Replay it and you get the same states, on a server, in a browser or in the Lean model.

An event goes from the mailbox to the journal to the pure step function; its effects are performed by the shell and their results return to the mailbox pure and replayable Mailbox Journal step (config, dm, event) Effects Shell sends · timers · deciders append deliver results as new events
Plate II. The way of one event. Append first, then step.

A choice point, in the chart's own words

From crates/vertep-agent/examples/support-agent.scxml: the model may call a tool, finish or escalate, and nothing else.

<state id="decide" vt:decide="llm/claude" vt:fallback="human/support" vt:deadline="30s"
       vt:maxDecisions="10" vt:candidates="call_tool finish escalate">
  <transition event="call_tool" target="tooling">
    <send event="tool.call" targetexpr="ev.data.tool"><content expr="ev.data.args"/></send>
  </transition>
  <transition event="finish" target="done"><assign location="answer" expr="ev.data"/></transition>
  <transition event="escalate" target="human"/>
  <transition event="vt.agent.budget-exhausted" target="budget_out"/>
  <transition event="error.decide.invalid" target="decide"/>
  <transition event="vt.decide.refused" target="human"/>
</state>

On entry, the core computes the events that would be enabled and offers them to the decider named llm/claude. Its answer returns as the event vt.decision, is journaled, and is accepted only if it was one of the offered candidates. If no answer comes within 30 seconds, the durable deadline hands the choice to a person. After ten decisions, the budget event ends the loop.

Get Vertep

Rust crates on crates.io, JavaScript packages on npm, source on GitHub.

[dependencies]
vertep = "0.1"
cargo install vertep-cli      # the vt command
npm install @vertep/web       # browsers and Node.js

Where it stands

Seven milestones, from the SCXML core to the browser, are built. Every requirement is traced from its spec to the code that implements it and the test or proof that checks it.

✶

Specified

303 requirements in OpenSpec, with scenarios, linked to decisions and constraints in a typed graph.

✶

Built

Twenty Rust crates and two npm packages: core, surfaces, runtime, agents, cluster, federation, WebAssembly.

✶

Checked

The W3C SCXML suite, Rust-against-Lean differential traces, container fault tests, and Lean theorems with no sorry.