RaceProof — deterministic concurrency testing for TypeScript
Explore the timelines your tests never run.
RaceProof is a local-first developer tool for finding race conditions before they reach production. Instead of validating one expected event order, it explores a bounded state space of deterministic event schedules: retries, timeouts, duplicate delivery, delayed completion, stale reads, and out-of-order messages.
When a safety invariant fails, RaceProof returns the exact event sequence, minimizes it into a valid reproducible counterexample, lets developers replay it step by step, shows immutable state diffs, and exports a ready-to-run Vitest regression test.
The problem
Ordinary tests usually exercise one happy-path timeline. Real distributed systems do not: an original request and a retry may both complete, two customers may act on stale inventory, and an edit can arrive before the message it modifies. These bugs are difficult to reproduce because the failure depends on timing and ordering rather than a single incorrect function.
What RaceProof does
Explores bounded reachable states with BFS, DFS, and seeded randomized traversal. Uses canonical JSON state serialization to skip duplicate states deterministically. Validates immutable transitions, guards, JSON compatibility, duplicate IDs, invalid bounds, and replay divergence. Produces a counterexample with invariant details, actors, labels, before/after state snapshots, and structured diffs. Applies guard-aware delta debugging so a minimized trace remains executable and violates the same invariant. Runs exploration in a Web Worker to keep the browser interface responsive, with progress, cancellation, timeout, and worker-failure handling. Exports portable run-result JSON and self-contained Vitest regression tests. Includes a CLI for judges and CI systems.
Built-in demonstrations
RaceProof ships three polished Buggy/Fixed model pairs:
Duplicate Payment — an original request and retry can charge an order twice; the fixed model adds idempotency. Inventory Overselling — two customers confirm the final item using stale reads; the fixed model performs atomic reservation. Out-of-Order Chat Events — an edit delivered before creation is lost; the fixed model buffers and reconciles the edit.
Every buggy model reliably produces its intended violation within small bounds. Every fixed model reports “No violation found within selected bounds”—never an unbounded correctness claim.
Product experience
The responsive web workbench provides example selection, bounded exploration controls, live engine metrics, a violation or bounded-success summary, an interactive replay timeline, JSON state inspector, highlighted state diffs, invariant status, clipboard/download actions, and generated test output. It remains usable on desktop and mobile and supports visible focus, semantic controls, keyboard replay, and reduced motion.
How it was built
RaceProof is a TypeScript npm-workspace monorepo with a small pure core domain package, an explorer/replay package, bundled trusted examples, a test generator, a CLI, and a static React/Vite application. The browser UI runs only bundled models: it never evaluates pasted JavaScript, needs no credentials, calls no remote service, and stores no user data.
Verification
The project includes strict TypeScript checks, ESLint, unit tests, property-based tests with fast-check, integration tests, Playwright desktop/mobile journeys, accessibility smoke coverage, coverage reporting, a production build, benchmarks, and CLI verification. The main check runs lint, type checking, tests, and production build.
How Codex and GPT-5.6 were used
GPT-5.6 and Codex accelerated the build through implementation, testing, documentation, performance review, and final verification. Human architectural decisions defined the trust boundary, deterministic model, bounded-verification language, and product scope. RaceProof itself contains no AI functionality at runtime: it makes no OpenAI API calls, requires no API key, includes no chatbot, and has no model dependency.
Why it matters
RaceProof makes concurrency failures concrete. Developers can move from “this only happens sometimes” to a deterministic schedule, a minimized reproduction, and a permanent regression test—all locally and without depending on production telemetry.
What's next
Future work could add visual schedule comparison, richer trace import/export workflows, and integrations with application test suites while preserving the core rule: exploration stays deterministic, local, and explicit.
Silent visual demo (30 seconds)
Built With
- codex
- fast-check
- gpt-5.6
- node.js
- playwright
- react
- typescript
- vite
- vitest
- web-workers