Using Supabase as the backend for dafny-replay apps

The Supabase backend adapter gives dafny-replay apps managed authentication, database-level authorization through Row-Level Security, built-in realtime subscriptions, and serverless Edge Functions that run the compiled Dafny dispatch logic server-side in Deno. This is the default backend and the reference implementation for the multi-collaboration pattern.

Architecture

┌─────────────────────────────────────────────────────────┐
│  Supabase                                               │
│                                                         │
│  ┌──────────────┐  ┌──────────────┐  ┌───────────────┐  │
│  │  Auth        │  │  Database    │  │  Edge Function│  │
│  │  (OAuth)     │  │  + RLS       │  │  /dispatch    │  │
│  │              │  │              │  │               │  │
│  │  - Sign up   │  │  - projects  │  │  Runs Dafny   │  │
│  │  - Sign in   │  │  - members   │  │  dispatch     │  │
│  └──────────────┘  │              │  │  server-side  │  │
│                    │  RLS allows  │  └───────────────┘  │
│                    │  member read │                     │
│                    └──────────────┘                     │
└─────────────────────────────────────────────────────────┘
                     │                    │
       Realtime      │                    │  Dispatch
       subscription  │                    │  call
                     ▼                    ▼
┌─────────────────────────────────────────────────────────┐
│  React Client (useSyncExternalStore + EffectManager)    │
└─────────────────────────────────────────────────────────┘

Supabase handles the infrastructure; Dafny handles correctness. The Edge Function is the thin bridge that runs verified domain logic server-side.

Environment variables

Add these to your .env file (or .env.local for local development):

VITE_BACKEND=supabase
VITE_SUPABASE_URL=https://your-project-ref.supabase.co
VITE_SUPABASE_ANON_KEY=eyJ...

Find both values in your Supabase dashboard under Settings → Data API.

Backend implementation

The Supabase adapter creates a standard supabase-js client and maps the three generic sections of the Backend interface to Supabase calls:

// src/backend/supabase.ts
import { createClient } from '@supabase/supabase-js'

export function createSupabaseBackend(): Backend {
  const supabase = createClient(
    import.meta.env.VITE_SUPABASE_URL,
    import.meta.env.VITE_SUPABASE_ANON_KEY
  )

  return {
    auth: {
      getCurrentUser: async () => {
        const { data: { user } } = await supabase.auth.getUser()
        return user ? { id: user.id, email: user.email! } : null
      },
      signIn: async (email, password) => {
        const { error } = await supabase.auth.signInWithPassword({ email, password })
        if (error) throw error
      },
      signOut: async () => {
        await supabase.auth.signOut()
      },
      onAuthChange: (callback) => {
        const { data: { subscription } } = supabase.auth.onAuthStateChange(
          (_, session) => callback(session?.user ? { id: session.user.id, email: session.user.email! } : null)
        )
        return () => subscription.unsubscribe()
      },
      // ...
    },

    dispatch: {
      single: async (projectId, baseVersion, action) => {
        const { data } = await supabase.functions.invoke('dispatch', {
          body: { projectId, baseVersion, action }
        })
        return data
      }
    },

    realtime: {
      subscribe: (projectId, onUpdate) => {
        const channel = supabase
          .channel(`project:${projectId}`)
          .on('postgres_changes', {
            event: 'UPDATE',
            schema: 'public',
            table: 'projects',
            filter: `id=eq.${projectId}`
          }, (payload) => {
            onUpdate(payload.new.version, payload.new.state)
          })
          .subscribe()

        return () => supabase.removeChannel(channel)
      }
    }
  }
}

Dispatch via Edge Function

The dispatch.single call invokes a Supabase Edge Function that runs the actual compiled Dafny code in Deno. The function:

Authenticates the caller via the Authorization header.
Checks project membership with RLS-aware queries.
Loads the current state, version, and applied_log from PostgreSQL.
Calls the Dafny dispatch() function from the pre-built bundle.
Persists the new state with an optimistic-lock eq('version', project.version) check.
Returns { status, version, state } to the client.

// supabase/functions/dispatch/index.ts (simplified)
import { dispatch } from './dafny-bundle.ts'   // compiled Dafny

const result = dispatch(
  project.state,
  project.applied_log || [],
  baseVersion,
  action
)

if (result.status === 'rejected') {
  return new Response(JSON.stringify(result), { status: 200, ... })
}

// Optimistic lock: fails if another writer updated the row
const { error } = await supabaseAdmin
  .from('projects')
  .update({ state: result.state, version: project.version + 1, ... })
  .eq('id', projectId)
  .eq('version', project.version)   // conflict if version changed

if (error) {
  return new Response(JSON.stringify({ status: 'conflict' }), { status: 409, ... })
}

The dafny-bundle.ts file is generated by dafny2js --deno and is not hand-written. Run ./compile.sh from the repo root to regenerate it after modifying domain logic.

Realtime subscription via postgres_changes

realtime.subscribe opens a Supabase channel filtered to a single project row. When the Edge Function persists a new state, Supabase’s logical replication triggers an event that the client receives:

const channel = supabase
  .channel(`project:${projectId}`)
  .on('postgres_changes', {
    event: 'UPDATE',
    schema: 'public',
    table: 'projects',
    filter: `id=eq.${projectId}`
  }, (payload) => {
    onUpdate(payload.new.version, payload.new.state)
  })
  .subscribe()

Supabase Realtime respects RLS: clients only receive events for rows their authenticated user can read. No extra membership check is needed in the subscription handler.

Database schema

The pattern uses two core tables — one for entity state and one for membership:

CREATE TABLE projects (
  id          UUID PRIMARY KEY DEFAULT gen_random_uuid(),
  name        TEXT NOT NULL,
  owner_id    UUID NOT NULL REFERENCES auth.users(id),
  state       JSONB NOT NULL DEFAULT '{}',
  version     INT  NOT NULL DEFAULT 0,
  applied_log JSONB NOT NULL DEFAULT '[]',
  created_at  TIMESTAMPTZ DEFAULT now(),
  updated_at  TIMESTAMPTZ DEFAULT now()
);

CREATE TABLE project_members (
  project_id UUID NOT NULL REFERENCES projects(id) ON DELETE CASCADE,
  user_id    UUID NOT NULL REFERENCES auth.users(id) ON DELETE CASCADE,
  role       TEXT NOT NULL DEFAULT 'member',
  PRIMARY KEY (project_id, user_id)
);

Row-Level Security ensures members can read projects but all writes go through the Edge Function (which uses the service role key):

ALTER TABLE projects ENABLE ROW LEVEL SECURITY;

CREATE POLICY "members can read projects"
  ON projects FOR SELECT
  USING (is_project_member(id));

Use SECURITY DEFINER helper functions (like is_project_member) when RLS policies reference each other, to avoid infinite recursion. See SUPABASE.md in the repository for the full schema and RLS setup.

Cross-tab auth sync

Supabase broadcasts auth state changes across browser tabs automatically. However, data-fetching hooks that run only on mount will not re-fetch if the user changes in another tab. Pass userId as a dependency to any fetch effect:

// Re-fetches when the user changes across tabs
useEffect(() => {
  if (!userId) return
  fetchProjects(userId)
}, [userId])

Deploying

Deploy the Edge Function with the Supabase CLI:

# Login and link your project
supabase login
supabase link

# Deploy the dispatch function
supabase functions deploy dispatch

Set the frontend environment variables with your project URL and anon key, then deploy the static build to any host (Netlify, Cloudflare Pages, etc.):

npm run build
# Upload dist/ to your chosen static host

The Supabase backend is described in detail in SUPABASE.md and DEPLOY_SUPABASE.md in the repository. Those files cover the full schema, RLS policies, offline hook API, and the trust boundary between Supabase and Dafny.

Trade-offs

The Supabase backend is the batteries-included option.

Advantage	Detail
Managed auth	OAuth, magic links, and session management out of the box
Database-level authorization	RLS enforces access control even if application code has bugs
Built-in realtime	No separate WebSocket infrastructure to operate
Simple deployment	One CLI command deploys the Edge Function

Trade-off	Detail
Higher cost at scale	Supabase pricing is per-project; realtime connections count toward quotas
Deno runtime	Edge Functions run in Deno, which affects how the Dafny bundle is generated (`--deno` flag)
Vendor lock-in	Moving away from Supabase requires replacing auth, RLS, and realtime — the backend abstraction makes this tractable

Backend overview

Understand the Backend interface and what stays the same across providers.

Cloudflare backend

Compare with the Cloudflare Workers option: D1, Durable Objects, and custom JWT.

Introduction

Kernels

Building with dafny-replay

Example Apps

Backend Integration

Reference

Using Supabase as the backend for dafny-replay apps

Architecture

Environment variables

Backend implementation

Dispatch via Edge Function

Realtime subscription via postgres_changes

Database schema

Cross-tab auth sync

Deploying

Trade-offs

Backend overview

Cloudflare backend

Build docs developers (and LLMs) love

Introduction

Kernels

Building with dafny-replay

Example Apps

Backend Integration

Reference

Documentation Index

​Architecture

​Environment variables

​Backend implementation

​Dispatch via Edge Function

​Realtime subscription via postgres_changes

​Database schema

​Cross-tab auth sync

​Deploying

​Trade-offs

Backend overview

Cloudflare backend

Build docs developers (and LLMs) love

Architecture

Environment variables

Backend implementation

Dispatch via Edge Function

Realtime subscription via postgres_changes

Database schema

Cross-tab auth sync

Deploying

Trade-offs