A deterministic bytecode VM for agent execution. Verified bytecode, serializable continuations, exact replay.
cinderc β verify β run β replay --seek. Full transcript in docs/walkthrough.md.
- What this is
- Why a VM
- Mental model
- Quickstart
- The instruction set
- The verifier
- Continuations
- Determinism and replay
- The supervisor
- Performance
- Building from source
- Repository layout
- Stability
- FAQ
- License
An agent run is a long-lived, effectful, resumable computation. Most frameworks
model it as a Python while loop with a list of dicts, which means the run's
state lives in interpreter frames you cannot serialize, on a machine you cannot
lose, in an order you cannot reproduce.
cindervm models it as bytecode on a machine designed for it. Agent
control flow β issuing a tool call, awaiting it, forking speculative branches,
checkpointing, yielding to a scheduler β is expressed in the instruction set
rather than in host-language coroutines. Consequences follow from that one
decision:
| Property | Mechanism |
|---|---|
| A run can be moved between hosts mid-flight | The entire machine state is a value (cont.rs) |
| A crashed run resumes without re-executing effects | Append-only, hash-chained journal (journal.rs) |
| A bug is reproducible from the log alone | The interpreter is a pure function of (image, journal) |
| Malformed bytecode cannot corrupt the interpreter | Bytecode is verified before it is admitted (verify.rs) |
| Cost is bounded before a token is spent | Budget reservations are instructions, not middleware |
The alternative designs and why they were rejected:
Host coroutines (async fn, Python async def). Suspension points are
implicit and the suspended state is a compiler-generated struct with no stable
representation. You cannot write it to disk, you cannot inspect it, and you
cannot resume it in a different process. Fine for I/O concurrency; wrong for
durable execution.
Durable-execution engines with replay-based recovery. Recovery works by
re-running the whole program and short-circuiting completed calls from a log.
This makes non-determinism catastrophic: one unlogged now() and the replay
diverges from the original. cindervm restores state directly instead of
re-deriving it, so divergence is impossible by construction β and every source
of non-determinism is an instruction that reads from the journal.
Interpreting a graph / AST. Workable, but the state is a tree of live objects with sharing and cycles, so serialization becomes a graph-walk with identity preservation. A flat operand stack over a flat heap of tagged values serializes as a memcpy of two arrays plus a relocation pass.
The VM approach costs an assembler and a verifier. It buys a state representation that is already a byte string.
ββββββββββββββββββββββββββββββββββββββββββββ
.cdx source β cinderc β
ββββββββββββββββββββΊ β lex ββΊ parse ββΊ resolve ββΊ encode β
β β β
βββββββββββββββββββββββββΌβββββββββββββββββββ
βΌ
image.cdxb (verified once,
hash-sealed)
β
βββββββββββββββββββββββββββββββββββββββββ΄ββββββββββββββββββββ
βΌ βΌ
βββββββββββββββββββββ ββββββββββββββββββββββ
β interp.rs β trap(CALL_TOOL, args) β supervisor (Go) β
β β ββββββββββββββββββββββββββββββββββΊ β β
β pc, stack, heap β β scheduler β
β frames, budget β ββββββββββββββββββββββββββββββββββ β syscall broker β
β β journal record #n (sealed) β quota ledger β
βββββββββββ¬ββββββββββ ββββββββββββββββββββββ
β
β YIELD_CTX / CHECKPOINT
βΌ
βββββββββββββββββββββ
β cont.rs β snapshot βββΊ blob βββΊ object store
β frozen machine β blob βββββββΊ restore (any host, any time)
βββββββββββββββββββββ
Three invariants hold everywhere in the codebase, and most of the design falls out of them:
- The interpreter performs no I/O. It returns a
Trapdescribing what it needs. The host answers. This is why replay is exact β replacing the host with a journal reader is a no-op from the interpreter's perspective. - Every value is copyable and tagged. No host pointers in VM state, no
Rc, no interior mutability.ValueisCopyand 16 bytes; anything larger lives in the heap arena behind aHandle. - Verification is a precondition of execution, not a mode.
Imagecannot be constructed except throughverify::admit. The interpreter therefore contains no bounds checks onpc, no stack-depth checks, and no operand type dispatch failures β the verifier already proved they cannot happen.
cargo install cindervm # cinderc, cinder
go install ./cmd/cinderd # supervisor (optional)A minimal agent. .cdx is the textual form of the bytecode β a macro assembler,
not a language.
.isa cdx/4
.image "triage"
.budget tokens=8000 wall=45s tools=6
.const $sys "You triage bug reports. Reply with severity only."
.tool %rank "llm.complete" -> str
.tool %file "github.issue.label"
.fn main() -> i32
.maxstack 6
main:
ldc $sys
argv 0 ; the issue body, from the host
pack 2
calltool %rank ; traps; supervisor answers
await ; blocks this VM, not the host thread
dup
ldc "critical"
eq
brz .done ; not critical β nothing to do
checkpoint "pre-label" ; durable point before a side effect
ldc "P0"
calltool %file
await
drop
.done:
drop
ldi 0
ret$ cinderc triage.cdx -o triage.cdxb
compiled triage.cdxb 264 B 1 fn 14 insns maxstack 6
verified frames=14/14 types=ok stack=ok effects=ok 1.9 ms
$ cinder run triage.cdxb --arg "segfault on startup, every launch" --journal run.jl
[0000] calltool llm.complete β 41 tok
[0001] await β 3 tok 612 ms "critical"
[0002] checkpoint pre-label β 1.4 KB
[0003] calltool github.issue.label β β
[0004] await β β 208 ms ok
halt 0 wall 0.83 s tokens 44/8000 tools 2/6Then debug it without touching the network:
$ cinder replay run.jl --seek 0002 --inspect stack
stack [0] str "critical" (heap #3, 8 B)
frame main pc=0x1a depth=1/6
budget tokens 44 wall 0.61s tools 1replay is not a simulation. It is the same interpreter with the syscall broker
swapped for a journal cursor; a replay that diverges from its journal is a bug
and aborts with E_DIVERGE naming the instruction.
cdx/4. Fixed 4-byte encoding: [opcode:8][a:8][b:16], with a wide prefix
(0xFF) promoting b to 32 bits for large constant pools. Full reference:
docs/isa.md.
| Class | Opcodes | Notes |
|---|---|---|
| Stack | LDC LDI DUP DUPN DROP SWAP ROT |
Depth is a static property; see verifier. |
| Data | PACK UNPACK IDX LEN CAT FMT |
Heap-allocating; charged against the arena quota. |
| Arithmetic | ADD SUB MUL DIV MOD EQ LT NOT |
Wrapping i64 only. No floats β floats are not deterministic across hosts. |
| Control | BR BRZ BRNZ CALL RET TAIL SWITCH TRAP |
Targets are function-local; no computed jumps. |
| Effects | CALLTOOL AWAIT POLL CANCEL |
The only instructions that can suspend. |
| Concurrency | SPAWN JOIN SELECT FORK COMMIT ABORT |
FORK is copy-on-write over the heap arena. |
| Durability | CHECKPOINT YIELD_CTX RESUME |
Snapshot boundaries. Verified to occur at empty-pending points. |
| Metering | RESERVE RELEASE SPEND QUERYQ |
Two-phase: reserve before the call, spend on the answer. |
| Context | CTXPUSH CTXPOP CTXWIN CTXCOST |
Conversation context as an addressable ring, not a list you append to. |
Deliberate omissions, each of which would break a property above:
- No floating point.
x87/SSE rounding andfmacontraction differ across targets. Determinism outranks convenience; use scaled integers. - No indirect branches. The verifier's fixpoint needs a static CFG.
- No host pointers, no FFI opcode. Anything a host could inject would be unserializable and untrackable.
- No unbounded loops without metering.
BRto a lowerpcrequires a dominatingSPENDorRESERVE; enforced inverify.rsso a runaway agent burns budget rather than wall-clock.
Structurally a JVM-style verifier: abstract interpretation over the CFG, iterated to a fixpoint, with merge points requiring the frames to unify. It runs once at load and its result is cached in the image header alongside a hash of the code section, so a re-run of the same image skips it.
What it proves, per basic block, for every reachable pc:
- Stack depth is single-valued. Every path into a block agrees on depth.
Disagreement is
E_DEPTH_MERGE, reported with both predecessor blocks. This is what lets the interpreter index the stack without checking. - Operand types unify. The lattice is
β₯ β {i64, str, bytes, list, handle, pending<T>} β β€, withβ€illegal at any use site. Merges compute the join; a join landing onβ€is a type error at the merge, not at the eventual use β which is why the diagnostics point at the branch rather than at a random instruction 40 lines later. - No
pending<T>escapes. A value produced byCALLTOOLispending<T>and onlyAWAIT,POLL,CANCEL, andSELECTconsume it. Any other use, or reachingRET/CHECKPOINTwith a livepending, isE_PENDING_ESCAPE. This single rule is what makes snapshots safe: no snapshot can contain a half-issued effect whose completion nobody is waiting for. maxstackis honoured. The declared bound dominates the computed high-water mark. The interpreter allocates exactlymaxstackslots per frame and never grows.- Branch targets are in-range and land on instruction boundaries. Trivial given fixed-width encoding, but checked, because the encoding is not the only producer of images.
- Metering dominates back-edges. Every cycle in the CFG contains at least one metering instruction, proven with a dominator computation over the loop headers.
FORK/COMMIT/ABORTare balanced along all paths, and the fork depth at a merge agrees. Unbalanced isE_FORK_IMBALANCE.
Diagnostics carry source spans through the assembler, so a verify failure on
hand-written .cdx reads like a compiler error rather than an offset:
error[E_PENDING_ESCAPE]: pending value reaches `ret` unawaited
ββ triage.cdx:21:9
β
14β calltool %rank
β βββββββββββββββ pending<str> produced here
Β·
21β ret
β ^^^ still live at return; depth 1, slot 0
β
= a `pending` must be consumed by await/poll/cancel/select
= help: insert `await` before `ret`, or `cancel` to discard the effect
The conformance corpus contains 214 images that must be rejected, each
with the expected error code, plus 96 that must be accepted. cinder-fuzz
generates structurally-valid-but-semantically-broken bytecode by mutating the
accepted set; the invariant under test is that the interpreter never panics on
anything the verifier admits, and never runs anything it rejects.
A snapshot is the machine, flattened:
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
β magic "CDXC" ver flags image_hash[32] journal_seq β header, 56 B
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ€
β frames: [ pc, fn_id, base, depth, fork_depth ] Γ n β 20 B each
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ€
β operands: [ tag:u8, payload:u64, _pad ] Γ m β 16 B each
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ€
β heap arena: bump-allocated bytes, relocated on restore β variable
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ€
β context ring: window offsets + interned segment ids β variable
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ€
β budget ledger: reserved / spent / limits β 48 B
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ€
β blake3(all of the above) β 32 B
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
The design constraints that shaped it:
- Restore validates before it trusts. A snapshot is a foreign byte string.
cont::restorechecks the hash, the image binding, frame/operand bounds, and every heap handle's target extent β then reconstructs. A snapshot from a different image isE_IMAGE_MISMATCH, never a wild jump. - Handles are arena-relative, so relocation is arithmetic. No pointer patching, no identity map, no graph walk.
FORKis copy-on-write at page granularity over the arena, so speculative branches are cheap until they write. Refcounts live outside the arena so a snapshot of a forked machine is still a flat copy. Invariants are asserted indebug_assertionsbuilds after every arena mutation.- Snapshots are content-addressed and diffable. Consecutive checkpoints in a
long run share most of their arena, so
cinder snap diff a bis a chunk-level comparison and the object store dedups.
$ cinder snap inspect run.cdxc
image triage 6f2aβ¦c1 (matches)
frames 1 main pc=0x1a
operands 1/6 [0] str #3
arena 1184 B 3 live handles, 0 B slack
journal seq 2 last: tool.answer #1
budget 44/8000 tok 1/6 tools 0.61/45 sThe interpreter is a pure function:
step : (Image, State, Answer?) -> (State, Trap?)
Nothing else reaches it. Time, randomness, tool results, spawned-child results,
and even the iteration order of SELECT are answers delivered by the host and
recorded in the journal. NOW and RAND are instructions that trap.
The journal is append-only and hash-chained β record n commits to
blake3(prev_hash β payload) β so a truncated or edited journal is detectable
rather than silently divergent. Records are sealed before the answer reaches
the interpreter, which is the ordering that makes crash recovery correct: a crash
between "effect performed" and "answer recorded" is recoverable because the
record was written first and marked in-flight, and recovery reconciles by
querying the broker for that record's idempotency key.
ββββββ record 41 βββββ ββββββ record 42 βββββ ββββββ record 43 βββββ
β prev a19fβ¦ β β prev 7c02β¦ β β prev e5b1β¦ β
β kind tool.issue β β kind tool.answer β β kind now β
β key idem:9f3aβ¦ β β ref 41 β β value 1756... β
β hash 7c02β¦ β β hash e5b1β¦ β β hash 3d84β¦ β
ββββββββββββββββββββββ ββββββββββββββββββββββ ββββββββββββββββββββββ
This gives three things that are usually mutually exclusive:
| How | |
|---|---|
| Exact replay | Same image + same journal β identical state at every step. Enforced, not hoped for: --verify-replay re-hashes state at each record and compares. |
| Time travel | replay --seek N restores the nearest checkpoint β€ N and steps forward. Backward stepping is forward stepping from an earlier snapshot; there is no undo log. |
| Divergence as a first-class error | If the interpreter asks for something the journal does not have next, that is E_DIVERGE with the record index, the expected kind, and the requested kind. It means the image changed or the VM has a bug β the two things you actually want to know. |
$ cinder replay run.jl --verify-replay
replaying 5 records against triage.cdxb (6f2aβ¦c1)
β 5/5 states match recorded digests
β journal chain intact (head 3d84β¦)Written in Go, in cmd/cinderd and internal/. The
split is not decorative: the VM wants a single-threaded, allocation-frugal,
panic-free core, while the supervisor wants goroutines, context cancellation,
and an HTTP surface. They meet over a length-prefixed frame protocol on a pipe or
UDS (docs/protocol.md), so a compromised or crashing tool
cannot take a VM's address space with it.
ββββββββββββββββββββββββββββββββββββββββββ
HTTP / gRPC β cinderd β
ββββββββββββββββΊ β β
β ββββββββββββ admission + fair queue β
β β schedulerβ weighted by tenant β
β ββββββ¬ββββββ β
β β lease β
β ββββββΌββββββ ββββββββββββ β
β β broker ββββΊβ ledger β quotas β
β ββββββ¬ββββββ ββββββββββββ β
βββββββββΌβββββββββββββββββββββββββββββββββ
β frames (UDS)
ββββββββββββββΌβββββββββββββ¬βββββββββββββ
βΌ βΌ βΌ βΌ
vm #1 vm #2 vm #3 vm #4 (separate procs)
Responsibilities, in the order they matter:
- Scheduler. VMs are cooperatively descheduled at
AWAIT/YIELD_CTX. A suspended VM costs a snapshot, not a thread, so the concurrency ceiling is memory, not goroutines. Fair queueing is deficit round-robin over tenants with weights; a single tenant cannot starve others by spawning. - Syscall broker. Owns tool dispatch, retries with jittered backoff, idempotency keys, and per-tool circuit breakers. Every dispatch is journalled before it leaves and reconciled on return.
- Ledger. Two-phase budget.
RESERVEtakes an optimistic lease against the tenant's remaining allowance;SPENDsettles it with the real usage;RELEASEreturns unused reservation. Overspend is refused at reserve time, so a run cannot exceed its budget and then apologize. - Recovery. On startup, scans the snapshot store for runs whose lease expired, reconciles their in-flight journal records against the broker, and reschedules from the last checkpoint.
Note
cinderd binds 127.0.0.1:7749 with no authentication by default β it is
built for a trusted network boundary with the real gateway in front. Before
exposing it, read docs/deployment.md and
set CINDERD_AUTH. The /debug/vm endpoint exposes full machine state,
including tool arguments, and must not be reachable from outside the host.
cargo bench on the committed corpus; 12-core Zen 4, Linux 6.11, --release.
Numbers are p50 with p99 in parentheses. Reproduce with
cargo bench -- --save-baseline main β docs/benchmarks.md
covers the methodology and the outlier handling.
| Operation | Result | Notes |
|---|---|---|
| Dispatch, arithmetic-heavy loop | 41 M insn/s (38 M) | Computed-goto-shaped match; the bottleneck is the store to sp. |
| Dispatch, effect-heavy | 9.1 M insn/s | Trap construction dominates. |
| Verify, 4 KiB image | 1.9 ms (2.4 ms) | Fixpoint converges in β€3 passes on all corpus images. |
| Snapshot, 64 KiB arena | 112 Β΅s (140 Β΅s) | Two memcpys and a hash; hash is 70% of it. |
| Restore + validate | 138 Β΅s (171 Β΅s) | Validation is 60% β deliberately not optional. |
FORK, 1 MiB arena |
8 Β΅s | COW; independent of arena size until first write. |
| Journal append, fsync | 1.1 ms | Group-committed; 84 Β΅s at batch 16. |
| Suspended VM, resident | 2.3 KiB | vs. ~8 KiB for a parked goroutine, ~40 KiB for a Python task. |
The interpreter's inner loop is the one place in the codebase where clarity was traded for speed, and it is commented accordingly. Everything else is written to be read.
Requires Rust β₯ 1.78 (pinned in rust-toolchain.toml) and
Go β₯ 1.22. No C toolchain, no system libraries, no build scripts β the Rust crate
has zero dependencies outside core/alloc/std, including the hash, the
arena, and the CLI argument parsing.
git clone https://github.com/ashish/cindervm && cd cindervm
make # debug build of both halves
make release # LTO, single codegen unit, symbols stripped
make test # unit + corpus conformance + Go tests + cross-language e2e
make verify # clippy -D warnings, rustfmt, go vet, staticcheck
make bench # criterion, baseline-compared
make fuzz T=60 # 60s of bytecode fuzzing against the verifier/interpreter pairIndividually:
cargo build --release --workspace
cargo test --all-features
cargo clippy --all-targets -- -D warnings
go build ./cmd/...
go test ./... -raceThe Makefile is the source of truth for what CI runs; the
workflow calls the same targets so a green local
make verify && make test means a green CI. The matrix covers
{linux, macos, windows} Γ {stable, 1.78, nightly}, with nightly allowed to fail
and Miri run on the arena and continuation modules only (they are where aliasing
mistakes would hide, even under #![deny(unsafe_code)] β Miri also catches UB
in the standard library calls we make).
Cross-compiling for the supervisor's target
The VM binary is the only thing that needs to match the tool-execution host. Static musl builds are the intended deployment:
rustup target add x86_64-unknown-linux-musl
cargo build --release --target x86_64-unknown-linux-musl --bin cinder
CGO_ENABLED=0 GOOS=linux GOARCH=amd64 go build -trimpath -ldflags='-s -w' ./cmd/cinderdBoth artifacts are then self-contained; the container is FROM scratch plus the
two binaries. See docs/deployment.md.
Regenerating the ISA tables and docs
src/isa.rs is the single definition of the instruction set β the
opcode table, operand shapes, stack effects, and type rules all live in one
const array. The assembler's mnemonic table, the disassembler, the verifier's
transfer functions, and docs/isa.md are all derived from it:
cargo run --bin cinderc -- --emit-isa-md > docs/isa.md
cargo test isa::table_is_dense # every opcode 0..N accounted for, no gapsmake verify fails if the checked-in docs/isa.md differs from the generated
one, so the reference cannot drift from the implementation.
The Rust core is deliberately flat. Modules are large because the boundaries follow the machine's structure, not a file-size preference.
cindervm/
βββ src/
β βββ lib.rs crate root, invariant docs, #![deny(unsafe_code)]
β βββ isa.rs opcode table, encoding, stack effects, type rules
β βββ value.rs tagged 16-byte Value, arena handles, coercions
β βββ lex.rs .cdx tokenizer with span tracking
β βββ asm.rs parser, symbol resolution, fixups, encoder
β βββ image.rs .cdxb container: sections, header, sealing
β βββ verify.rs abstract interpreter, type lattice, CFG fixpoint
β βββ cfg.rs basic blocks, dominators, loop headers
β βββ interp.rs the dispatch loop and instruction semantics
β βββ frame.rs call frames, operand stack windows
β βββ heap.rs bump arena, COW pages, handle validation
β βββ cont.rs snapshot / restore, relocation, validation
β βββ journal.rs hash-chained record log, cursor, reconciliation
β βββ replay.rs journal-backed host, divergence detection
β βββ budget.rs two-phase reservation ledger
β βββ ctx.rs context ring, windowing, token accounting
β βββ trap.rs the interpreterβhost boundary type
β βββ wire.rs frame protocol codec
β βββ diag.rs spans, error codes, rendered diagnostics
β βββ disas.rs disassembler and the `cinder dis` output
β βββ bin/
β βββ cinderc.rs assembler CLI
β βββ cinder.rs run / replay / snap / dis
β βββ cinder_fuzz.rs mutation fuzzer
βββ cmd/cinderd/ supervisor entrypoint
βββ internal/
β βββ sched/ deficit round-robin, leases
β βββ broker/ tool dispatch, retries, circuit breakers
β βββ ledger/ tenant quotas
β βββ wire/ Go side of the frame protocol
βββ corpus/ 310 conformance images with expected outcomes
βββ examples/ runnable .cdx agents
βββ docs/ isa, protocol, determinism, deployment, benchmarks
βββ tests/ integration + cross-language end-to-end
Every module is documented at the top with what it guarantees and what it assumes the caller has already proven. docs/architecture.md is the long form.
0.x. The library API is not stable. Two things are:
- The
.cdxbcontainer is versioned and will be read by future minor versions. Images do not need recompilation. - The journal format is append-only and forward-compatible; a journal written
by
0.4replays on0.5.
The ISA itself is versioned separately (cdx/4). Adding opcodes bumps the minor;
changing the meaning of one bumps the ISA version and images declare which they
target. CHANGELOG.md tracks both.
Why not just use a durable execution framework?
They recover by re-executing and short-circuiting from a log, which requires your
code to be deterministic and punishes you subtly when it isn't. cindervm
restores state rather than re-deriving it, and makes non-determinism impossible
at the ISA level instead of asking you to be careful.
Is .cdx meant to be written by hand?
For tests and examples, yes. In practice you generate it β the assembler is a
library, and asm::Builder is the intended interface for a higher-level frontend.
Writing one is the obvious next project and deliberately out of scope here.
Why is the interpreter single-threaded?
Because SPAWN creates a VM, not a thread. Parallelism belongs to the
supervisor, which can place VMs across processes and machines. A multi-threaded
interpreter would make state non-serializable, which is the one thing this design
will not trade.
How does this handle streaming tool results?
POLL returns pending unchanged until the answer is complete; partial chunks
are journalled as tool.chunk records and accumulate in the arena. Replay
reproduces chunk boundaries exactly, which turns out to matter for reproducing
bugs in streaming parsers.
Zero dependencies β really? Really, for the core crate. blake3 is ~200 lines, the arena is ~400, arg parsing is ~150. The tradeoff is deliberate: this is a trust-boundary component, and every dependency is code you are also trusting. Dev-dependencies (criterion, proptest) are not so constrained.
Apache-2.0 OR MIT, at your option. See LICENSE-APACHE and LICENSE-MIT.
What happens if the host dies mid-run? The snapshot restores the machine state directly from the object store; effects issued before the snapshot are replayed from the journal, so nothing is re-executed. See docs/internal-contract.md.
Can two VMs share one journal? No. A journal belongs to exactly one run; forks get their own chain so E_DIVERGE stays a meaningful signal.
Why is unsafe forbidden? The tagged-value layout makes relocation arithmetic, not pointer patching. There is no code that needs unsafe today, and the lint keeps it that way.