Part 7: Testing Causl Code

A causl graph is a state machine, and the questions that matter about a state machine are universal ones: for every commit sequence, does this invariant hold? This part of the tutorial covers the testing toolkit causl ships with — example-based unit tests with vitest, property-based fuzzing with fast-check, the tieredPropertyTrials helper for routing fuzz budgets through CI tiers, the @causl/checker static linter, and the 4-way classifier that races verdicts across the differential corpus.

By the end of this part you will be able to write tests that distinguish "passes because the bug isn't there" from "passes because we never tried hard enough" — the distinction that causl's testing contract was built around.

Why property tests, not just examples

Example-based tests confirm that a specific input produces a specific output. They are precise, fast, and easy to read. They are also weak at exposing the kind of bug causl is designed to prevent: race orderings, commit interleavings, and DAG-shape edge cases that only appear when the graph looks slightly off from anything a human would write by hand.

Property tests fix this by generating thousands of random graphs and commit sequences and asserting that a universal invariant — atomicity, glitch-freedom, determinism — holds across all of them. When a property fails, fast-check shrinks the failing input to a minimal counterexample and logs the seed so the failure replays deterministically. The counterexample is committed back to the repo as a regression fixture, and the property keeps running on every PR.

Detailed explanation: SPEC §15.2 floor. Causl's testing contract mandates a 1000-trial floor per property, per CI run. Under-trialling a property silently weakens the race-detection layer it is meant to be. The propertyTrials() helper rejects numRuns values below 1000 unless the caller opts in via unsafeTrials with a documented rationale, and the causl/no-unsafe-trials lint rule rejects that escape hatch without a justification comment.

1. Write an example test with vitest

Start with a concrete, readable test. Causl integrates with vitest like any other TypeScript library — there is no special test runner.

// graph.test.ts
import { describe, it, expect } from 'vitest'
import { createCausl, input, derived } from '@causl/core'

describe('counter graph', () => {
  it('derives doubled from count', () => {
    const graph = createCausl()
    const count = input(graph, 0)
    const doubled = derived(graph, g => g.read(count) * 2)

    graph.commit(() => {
      graph.set(count, 5)
    })

    expect(graph.read(doubled)).toBe(10)
  })
})

The pattern: build a graph in the test body, run one or more commits, read the derived value, assert. The commit() boundary is the unit of atomicity — every mutation inside one fires Phase A–H as a single transaction, so you can assert on the post-commit state without worrying about partial recomputes.

2. Add a property test with fast-check

Now generalise. Instead of asserting that 5 doubles to 10, assert that every input value n doubles to 2n. That is one trial; the property runs it a thousand times against random ns.

import { describe, it, expect } from 'vitest'
import fc from 'fast-check'
import { createCausl, input, derived } from '@causl/core'
import { propertyTrials } from '@causl/core/testing'

describe('doubled is a function of count', () => {
  it('holds for any integer', () => {
    fc.assert(
      fc.property(fc.integer(), (n) => {
        const graph = createCausl()
        const count = input(graph, 0)
        const doubled = derived(graph, g => g.read(count) * 2)
        graph.commit(() => graph.set(count, n))
        expect(graph.read(doubled)).toBe(n * 2)
      }),
      propertyTrials('counter-doubled'),
    )
  })
})

Three things to notice. The arbitrary (fc.integer()) defines the input space. The body is the property: this expectation must hold for every value. And the third argument to fc.assert() is the configuration — that is where propertyTrials() comes in.

What `propertyTrials()` does

propertyTrials(label, options?) returns a fast-check Parameters object with the trial floor enforced, the seed wired from the CAUSL_FUZZ_SEED environment variable when set (otherwise a random seed logged on every run), and the label embedded so a failure message identifies which property fired. Without the label, a CI failure in a file with twelve properties is a spelunking exercise.

3. Tier the fuzz budget with `tieredPropertyTrials`

The 1000-trial floor is right for every-PR feedback. It is wrong for the nightly build, which has hours of budget to spend, and it is also wrong for releases, where you want the most coverage you can afford before stamping a version. Causl's CI runs three tiers, and tieredPropertyTrials() is the helper that routes a single property through all three.

import { tieredPropertyTrials } from '@causl/core/testing'

it('any commit sequence preserves the invariant', () => {
  fc.assert(
    fc.property(commitSequenceArb, (commits) => {
      const graph = createCausl()
      // ... build graph, apply commits, assert invariant
    }),
    tieredPropertyTrials('commit-invariant'),
  )
})

The helper resolves the active tier from CAUSL_FUZZ_TIER and selects the matching trial count:

Tier	Env var value	`numRuns`	When it runs
default	`default` / unset	1000	local dev, PR fast path
pr	`pr`	5,000	required PR gate
nightly	`nightly`	100,000	cron job, 02:30 UTC
cargo-fuzz	`cargo-fuzz`	1000 (skip)	Rust corpus tier — TS path falls through

The numeric override CAUSL_FUZZ_TRIALS=N takes precedence when the named tier is unset; both lose to an explicit numRuns passed at the call site. The cargo-fuzz label is a marker for the Rust fuzz harness and does not boost the TypeScript property count — the heavy corpus-driven work lives in the Rust crate.

Prefer tieredPropertyTrials over hard-coded numRuns: 1000. A call site that pins propertyTrials('x', { numRuns: 1000 }) silently bypasses the tier system — CAUSL_FUZZ_TIER=nightly still produces 1000 trials, defeating the nightly's purpose. Always pass tiered properties through tieredPropertyTrials.

4. Lint statically with `@causl/checker`

Properties find bugs that can happen. The static linter finds bugs that must happen on every run — schema violations, cycles, unknown dependencies, use-after-dispose, cross-graph reads. It is much faster than property fuzzing because it never executes a commit; it analyses the CauslModel IR exported from your graph and walks twelve one-shot passes.

import { runChecker } from '@causl/checker'
import { createCausl, input, derived } from '@causl/core'

const graph = createCausl()
const a = input(graph, 0)
const b = derived(graph, g => g.read(a) + 1)

const model = graph.exportModel()
const report = await runChecker(model, { maxNodes: 100, maxCommits: 500 })

if (report.violations.length > 0) {
  for (const v of report.violations) {
    console.error(`[${v.ruleId}] ${v.node}: ${v.message}`)
  }
  process.exit(1)
}

Or as a CLI step in CI:

$ pnpm causl-check < model.json
$ pnpm causl-check --input model.json --max-nodes 100

The --replay <report-path> flag is the verdict-determinism gate: it loads a saved JSON report and re-runs the checker against the same model, exiting with code 3 if the verdict diverges. The --suppress <rule-id>=<reason> flag is the only sanctioned way to silence a diagnostic, and every suppression requires a non-empty justification.

5. Read the 4-way race-detection classifier

Causl's race detection runs in three tiers (the static linter for PRs, the bounded enumerator at K=10/D=5 for main, and the K=20/D=8 enumerator plus an Apalache differential at night). The differential is the bit you should understand even if you never run it yourself: every TLA+ model in the corpus is checked by both Apalache and the Rust enumerator, and their verdicts are compared cell-by-cell. The classifier has four buckets:

Status	Apalache	Enumerator	Meaning
`triple_agree`	Match	Match	Both backends concur. The expected case; ship.
`apalache_only_agrees`	Match	Divergence	Apalache confirms the spec; the Rust enumerator does not. Defect in the enumerator or its action lattice.
`enumerator_only_agrees`	Divergence	Match	Enumerator confirms; Apalache disagrees. Defect in the TLA+ model or the verdict-mapping layer.
`none_agree`	Divergence	Divergence	Both backends disagree with the expected verdict. The race is real and the corpus needs review.

A fifth bucket, unknown, is reported when either backend produced no verdict (Apalache fetch failure, enumerator bound-exceeded). The Tier 3 job downgrades unknown from Apalache to a warning rather than a hard failure — Apalache's Releases API is occasionally rate-limited — but a Rust-side unknown still fails closed.

What this gives an adopter. When the differential disagrees, the classifier tells you which side to look at first. A none_agree cell points at the model or the property; an apalache_only_agrees cell points at the enumerator. Without the 4-way split, every divergence is "some backend is wrong somewhere" and the bisect is manual.

6. Recording a counterexample as a regression fixture

When fast-check shrinks a failure to a minimal counterexample, copy it back into the test file as an example-based test. The next CI run regression-tests the bug explicitly even if the random seed never visits that input again.

import { describe, it, expect } from 'vitest'
import { createCausl, input, derived } from '@causl/core'

// Regression: fast-check shrunk to this on seed=1709234182, label=counter-doubled.
// Phase D recompute order skipped doubled when count flipped 0 -> 0 (no-op write).
it('handles no-op writes (regression)', () => {
  const graph = createCausl()
  const count = input(graph, 0)
  const doubled = derived(graph, g => g.read(count) * 2)
  graph.commit(() => graph.set(count, 0))
  expect(graph.read(doubled)).toBe(0)
})

Comment the seed and the label. Six months from now, the bug recurs and the reviewer wants to know which property generated this exact input. The comment is the trail.

What we covered

Example tests with vitest are the readable surface; property tests with fast-check are the coverage surface.
propertyTrials() enforces the 1000-trial SPEC §15.2 floor and labels each property for legible failures.
tieredPropertyTrials() routes the fuzz budget through CAUSL_FUZZ_TIER: 1000 (default), 5,000 (pr), 100,000 (nightly).
@causl/checker is the static-IR linter — twelve one-shot passes, no commit execution, runs in seconds.
The 4-way race-detection classifier — triple_agree, apalache_only_agrees, enumerator_only_agrees, none_agree — tells you which side to bisect when a differential disagrees.

Next steps

Part 8 covers devtools and time-travel debugging — recording commit history, scrubbing through it, and using @causl/devtools-bridge to wire the graph to a browser inspector. The contracts your tests assert are the same contracts the devtools surface visually.