Use this file to discover all available pages before exploring further.
The Cloudflare backend adapter runs the complete dafny-replay stack on Cloudflare’s edge infrastructure: D1 (SQLite) for state, a Hono-based Worker for dispatch and auth, a Durable Object for per-entity WebSocket hubs, and custom JWT authentication. Compared to the Supabase backend, this option gives you lower cost at scale and full ownership of the infrastructure, at the cost of building and operating each layer yourself.
The shared cloudflare/ package (@dafny-replay/cloudflare) provides auth, realtime, and helper middleware. Each app worker imports from this package and adds only app-specific routes and dispatch logic.
The Worker’s dispatch endpoint loads state from D1, calls the compiled Dafny bundle, and writes back with an optimistic lock — the same logic as the Supabase Edge Function, but running in the Workers runtime:
// worker/src/dispatch.ts (simplified)import { dispatch } from './dafny-bundle'app.post('/dispatch', authMiddleware, async (c) => { const { projectId, baseVersion, action } = await c.req.json() const user = c.get('user') // Authorization: check membership in D1 const membership = await c.env.DB .prepare('SELECT role FROM project_members WHERE project_id = ? AND user_id = ?') .bind(projectId, user.id) .first() if (!membership) return c.json({ error: 'Not a member' }, 403) // Load current state const project = await c.env.DB .prepare('SELECT state, version, applied_log FROM projects WHERE id = ?') .bind(projectId) .first() // Run verified Dafny dispatch const result = dispatch(project.state, project.applied_log || [], baseVersion, action) if (result.status === 'rejected') return c.json(result) const newVersion = project.version + 1 // Optimistic lock: update only if version unchanged const { meta } = await c.env.DB .prepare('UPDATE projects SET state = ?, version = ? WHERE id = ? AND version = ?') .bind(JSON.stringify(result.state), newVersion, projectId, project.version) .run() if (meta.changes === 0) return c.json({ status: 'conflict' }, 409) // Broadcast to WebSocket clients via Durable Object await broadcastUpdate(c.env.REALTIME, projectId, newVersion, result.state) return c.json({ status: 'accepted', version: newVersion, state: result.state })})
Each entity gets its own Durable Object instance that acts as a WebSocket hub. When dispatch succeeds, the Worker calls broadcastUpdate() which forwards the new state to all connected WebSocket clients:
WebSocket connections pass the JWT in the query string (?token=JWT) because browsers cannot set Authorization headers on WebSocket handshake requests. The Worker validates membership before upgrading the connection. Avoid enabling full URL logging in production to prevent token exposure in log data.
D1 uses SQLite syntax. The schema mirrors the Supabase schema but without RLS — authorization is enforced in Worker code instead:
CREATE TABLE users ( id TEXT PRIMARY KEY, email TEXT UNIQUE NOT NULL, password TEXT NOT NULL, created_at TEXT DEFAULT (datetime('now')));CREATE TABLE projects ( id TEXT PRIMARY KEY, name TEXT NOT NULL, owner_id TEXT NOT NULL REFERENCES users(id), state TEXT NOT NULL DEFAULT '{}', version INTEGER NOT NULL DEFAULT 0, applied_log TEXT NOT NULL DEFAULT '[]', created_at TEXT DEFAULT (datetime('now')));CREATE TABLE project_members ( project_id TEXT NOT NULL REFERENCES projects(id) ON DELETE CASCADE, user_id TEXT NOT NULL REFERENCES users(id) ON DELETE CASCADE, role TEXT NOT NULL DEFAULT 'member', PRIMARY KEY (project_id, user_id));
The Dafny bundle for a Cloudflare Worker is generated with the --cloudflare flag:
# From the repo root./compile.sh your-app-cloud
This generates worker/src/dafny-bundle.ts using import BigNumber from 'bignumber.js' (npm, not esm.sh) and inlines the Dafny code directly (Workers block new Function() calls).
Do not edit dafny-bundle.ts by hand. Regenerate it by running ./compile.sh after modifying domain Dafny files.
D1 has no Row-Level Security. Authorization is enforced in layers by the Worker:
Layer
Responsibility
Enforced by
1. Authentication
Verify the caller’s identity
Worker (JWT validation)
2. Access control
Check project membership
Worker (D1 query)
3. State validity
Validate the action against current state
Dafny
4. Invariant preservation
Ensure state remains consistent after the action
Dafny
If an actor bypasses layer 2 and submits an action referencing a non-existent member, Dafny (layer 3) will reject it. Layers 1 and 2 remain the application’s responsibility.
Dafny-verified membership checks (moving layer 2 into Dafny) are listed as a TODO in the repository. The Dafny spec already includes members: set<UserId> in the model and a NotAMember error type.
