Find the bugs that crashes, retries and concurrency cause before production does, and prove the business logic underneath for every input.
Runs your real Worker inside workerd through your own Vitest and the Cloudflare Vitest plugin. D1, Queues, Durable Objects with alarms and R2 are the real local bindings, wrapped rather than mocked.
Supported bindings
Crashes before and after each effect, lost replies, clean errors, redeliveries and cut-off background work, injected at every binding call and outbound fetch.
The fault model
Concurrent invocations interleave at their I/O, under a seeded scheduler or over every schedule within the bounds, with partial-order reduction.
Exploration
A violation comes back replayed and shrunk, with its full effect trace, and as a Vitest regression test that fails until the bug is fixed.
See one
Properties of your pure core are written with forall in TypeScript, checked on the inputs the simulation produced, then on generated inputs.
Writing specs
First-party engines prove properties for every input in Lean 4 or with Z3. When they disagree the verdict is CONFLICT, and nothing sampled is ever called verified.
The provers
This queue consumer records each payment in D1 and acknowledges the message. It passes every unit test you would think to write.
export default {
async queue(batch: MessageBatch<Payment>, env: Env): Promise<void> {
for (const message of batch.messages) {
const { orderId, amountCents } = message.body;
await env.DB.prepare("INSERT INTO payments (order_id, amount_cents) VALUES (?1, ?2)")
.bind(orderId, amountCents)
.run();
message.ack();
}
},
} satisfies ExportedHandler<Env, Payment>;A scenario beside it says what must hold: every payment recorded, none recorded twice. eutaxy check runs the Worker inside workerd, injects faults at every effect, redelivers messages the way Cloudflare Queues does, and finds the run that breaks it:
VIOLATED payments (seed payments)
Invariant payment-recorded-once is violated: D1:DB run happened twice for key "o-2" (seq 1 and 4)
Schedule (run seed 2537518072), events kept: msg-2
ambiguous at msg-2#1 effect #0 (D1:DB run)
Shrunk: 1 event(s) and 0 fault(s) removed in 3 run(s)The insert committed but its answer was lost, the handler threw, the queue redelivered the message, and the order was recorded twice. The same seed replays the same run on every machine, and the regression test Eutaxy writes fails until the insert is idempotent.
pnpm add -D eutaxy vitest @cloudflare/vitest-plugin typescript@7.1.0-betaEutaxy needs Node 24 and TypeScript 7.1 (inside Vitest, eutaxy/cloudflare loads without the compiler). It has no runtime dependencies; the prover toolchains (Lean 4, Z3) are optional. Continue with Getting started.