modality-ts

Model-checking-based testing tool for React state-transition bugs.

Read the docs »

modality-ts extracts a finite transition model from React + TypeScript code, checks developer-defined properties against every reachable state within stated bounds, and turns counterexamples into replayable tests.

It is for the bugs that hide between example-based tests: double submits, stale async completions, impossible checkout states, auth/router bypasses, and "this can never happen" state combinations that only appear after an awkward event interleaving.

Installation

npm install -D modality-ts
# or
pnpm add -D modality-ts
# or
yarn add -D modality-ts

Usage

1. Create an empty props file

Create an empty *.props.ts file beside the components you want to model:

src/App.tsx
src/App.props.ts

2. Run generation

Run generation before writing properties:

npx modality init
npx modality generate

This writes sibling modules such as src/App.modals.ts, which contain typed handles for the component's state and transitions.

3. Write properties

Write properties in the props file, importing component handles from sibling modules such as ./App.modals.

// src/App.props.ts
import {
  always,
  alwaysStep,
  and,
  eq,
  leadsToWithin,
  not,
  or,
  reachable,
  reachableFrom,
  stepEnqueued,
} from "modality-ts/properties";
import { App } from "./App.modals";

// always for state invariants
always(
  "guestCannotReachSuccess",
  not(and(eq(App.auth, "guest"), eq(App.step, "success"))),
);

// alwaysStep for action rules
alwaysStep("emptyDraftCannotSubmit", {
  negate: true,
  step: stepEnqueued("api.createTodo"),
  pre: eq(App.draft, "empty"),
});

// reachable for sanity checks
reachable("successIsReachable", eq(App.step, "success"));

// reachableFrom for conditional reachability
reachableFrom(
  "reviewStaysReachable",
  eq(App.payment, "valid"),
  eq(App.step, "review"),
);

// leadsToWithin for bounded response
leadsToWithin(
  "submitResolves",
  stepEnqueued("api.placeOrder"),
  or(eq(App.order, "success"), eq(App.order, "error")),
  { budget: { environment: 3 } },
);

4. Extract and check

Run extraction and check:

# extract the model from the source code
npx modality extract

# check the model for properties
npx modality check

This will produce a report like this:

 ✓ src/App.props.ts 0.13s
  (2 tests, 2 passed, 0 failed, 0 errors, states 1, edges 0, depth 1, slices 2, vars 2, transitions 0, skipped 0)
  ✓ guestCannotReachSuccess reachable
    trace: (initial)
  ✓ emptyDraftCannotSubmit verified-within-bounds
    trace: (initial)
  ✓ guestCannotReachSuccess verified-within-bounds
    trace: (initial)
  ✓ reviewStaysReachable verified-within-bounds
    trace: (initial)
  ✓ submitResolves verified-within-bounds
    trace: (initial)

 Test Files  0 failed | 1 passed (5)
      Tests  5 passed, 0 failed, 0 warnings, (5)
   Start at  <timestamp>
   Duration  <duration>

Limitation

modality-ts verifies the model it can extract, not arbitrary browser behavior. It works best for React apps where important behavior is represented as bounded, deterministic state transitions in TypeScript.

Good fits include:

• Components with local useState transitions.
• Apps that use supported state/data sources such as Jotai, SWR, and router state.
• Flows with finite domains, bounded collections, and named side effects.
• Business rules that can be expressed as safety properties over reachable states.

Current weak fits include:

• Apps whose correctness depends mainly on DOM layout, CSS, animation timing, canvas rendering, or browser quirks.
• Unbounded or highly numeric behavior without explicit finite bounds.
• External services that are not modeled as effects or bounded data.
• Concurrency, timers, and network races that are not represented in the extracted model.
• Code patterns outside the supported React + TypeScript extraction subset.

For those cases, use modality-ts alongside regular unit, integration, and end-to-end tests.

License

MIT