# A reachable-state safety invariant

KL-FCS-008 · Model checking · version 1.0.0

## Problem

Check that every reachable state is in {0, 1, 2}.

## Context

Explore the states actually reachable from an initial condition, and evaluate safety on that closure.

## Definitions

- **Reachability**: The least set containing all initial states and closed under transitions.
- **Safety invariant**: A predicate true at every reachable state.
- **Unreachable state**: A declared state that no allowed execution from an initial state reaches.

## Checked result

Safety invariant holds: yes.

Breadth-first exploration reaches exactly 0, 1, and 2. State 3 exists in the model but is unreachable from the initial state.

## Checker reasoning

1. Initialize the frontier with every initial state.
2. Follow all transitions, deduplicating visited states.
3. Compare the supplied reachable-state certificate with the computed closure.
4. Check whether every reachable state lies in the declared safe set.

## Dataset construction

{
  "family": "model-checking",
  "task": "Check that every reachable state is in {0, 1, 2}.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Complete reachability · 3 states",
  "acceptance": [
    "Initialize the frontier with every initial state.",
    "Follow all transitions, deduplicating visited states.",
    "Compare the supplied reachable-state certificate with the computed closure.",
    "Check whether every reachable state lies in the declared safe set."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

```json
{
  "specification": {
    "initial": [
      0
    ],
    "transitions": {
      "0": [
        0,
        1
      ],
      "1": [
        2
      ],
      "2": [
        0
      ],
      "3": [
        3
      ]
    },
    "safe": [
      0,
      1,
      2
    ]
  },
  "claim": {
    "invariant_holds": true
  },
  "witness": {
    "reachable": [
      0,
      1,
      2
    ]
  }
}
```

## Complexity

Breadth-first exploration is O(V+E) for an explicit finite graph; implicit system state spaces can grow exponentially.

## Limits

Safety for this finite transition system only; no fairness, liveness, or real-device behavior claim.

## Common error and further work

Ignoring an enabled transition can make an unsafe system appear safe.

Add counterexample paths, temporal properties, and fairness-aware liveness checks.

## Verification

Complete reachability · 3 states. 3 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11.
No external dataset or model-generation experiment. Reuse-license selection
remains pending.

- [Conceptual reference](https://www.prismmodelchecker.org/doc/whatsinprism.php)