Vertep

Explainable agents for decisions that matter

Vertep

Let a language model choose, but only among the moves your policy allows. Vertep writes every step down before it happens, so any decision can be replayed and explained later, without the model.

Statecharts that run as durable actors, in Rust and the browser, with a core checked against the W3C SCXML suite and a model proven in Lean.

Why Vertep Watch a loan decision For regulated work Docs

When an AI makes a decision that matters

Someone will ask why, months later. Vertep makes the answer a replay, not a reconstruction.

I

Lending

A model underwrites loans. A policy limit declines by rule, approval is never offered above the ceiling, and an officer decides referrals. Three real applications, with the audit read from the journal alone.

Run the example →
II

Healthcare

A model approves routine prior authorisations or refers them. Deny exists in exactly one state, and a clinician decides it. Statutory deadlines become durable timers.

See the chart →
III

Insurance

A model fast-tracks small, clean claims and flags the rest. Only an adjuster can refuse payment, and the reason is journaled with the decision.

See the chart →

Three promises hold, each checked rather than claimed. The model cannot choose a move the chart does not offer. Every input and answer is journaled before it is acted on. And a run replays without the model, so the thing under examination is not needed to examine it. Read: Explainable by construction →

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

Version 0.1.x. Eleven milestones, from the SCXML core to agent protocols, are built or in progress. Every requirement is traced from its spec to the code that implements it and the test or proof that checks it. It is young software: try it on a small case first, and tell us what breaks.

✶

Specified

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

✶

Built

Twenty-five workspace crates and two npm packages: core, surfaces, runtime, agents, cluster, federation, durable objects, a TSP mediator, did:webvh hosting, agent wallets, agent protocols and WebAssembly.

✶

Checked

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