Formal Computer Science / Programs & systems

Kenton Labs / Programs & systems

Model checking

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

The vocabulary.

These definitions state the objects and properties used by the dataset. The complete instance specification remains the authority for each result.

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.

How the dataset works.

Three deterministic instances define this family. Each includes its input model, a checked result, evidence, and an acceptance procedure. Download the complete dataset JSON ↘ or the area’s readable source ↘.

Acceptance procedure

  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.

Cost and scope

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

A common failure

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

Worked records.

Three instances expose concrete claims and the artifacts that establish or refute them. Expand a record for the problem, checker reasoning, formal payload, and verification metadata.

KL-FCS-008
Model checkingA reachable-state safety invariantComplete reachability · 3 states

The problem

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

The 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.

Why the checker accepts it

  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.

Formal specification

{
  "initial": [
    0
  ],
  "transitions": {
    "0": [
      0,
      1
    ],
    "1": [
      2
    ],
    "2": [
      0
    ],
    "3": [
      3
    ]
  },
  "safe": [
    0,
    1,
    2
  ]
}

Claim and evidence

{
  "claim": {
    "invariant_holds": true
  },
  "witness": {
    "reachable": [
      0,
      1,
      2
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 3 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

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

A boundary to investigate

Ignoring an enabled transition can make an unsafe system appear safe. Add counterexample paths, temporal properties, and fairness-aware liveness checks.

Verification and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-020 ↘Related KL-FCS-021 ↘
KL-FCS-020
Model checkingA reachable unsafe stateComplete four-state reachability

The problem

Explore the complete transition graph from state 0.

The checked result

Safety invariant holds: no.

Every successor is included in the closure. The safe-set comparison identifies whether the property holds across all reachable executions.

Why the checker accepts it

  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.

Formal specification

{
  "initial": [
    0
  ],
  "transitions": {
    "0": [
      1
    ],
    "1": [
      2
    ],
    "2": [
      3
    ],
    "3": [
      0
    ]
  },
  "safe": [
    0,
    1,
    2
  ]
}

Claim and evidence

{
  "claim": {
    "invariant_holds": false
  },
  "witness": {
    "reachable": [
      0,
      1,
      2,
      3
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 4 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

This is a finite safety check; no liveness or fairness statement is included.

A boundary to investigate

Ignoring an enabled transition can make an unsafe system appear safe. Add counterexample paths, temporal properties, and fairness-aware liveness checks.

Verification and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-008 ↘Related KL-FCS-021 ↘
KL-FCS-021
Model checkingBranching safety closureComplete four-state reachability

The problem

Explore the complete transition graph from state 0.

The checked result

Safety invariant holds: yes.

Every successor is included in the closure. The safe-set comparison identifies whether the property holds across all reachable executions.

Why the checker accepts it

  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.

Formal specification

{
  "initial": [
    0
  ],
  "transitions": {
    "0": [
      1,
      2
    ],
    "1": [
      3
    ],
    "2": [
      3
    ],
    "3": [
      3
    ]
  },
  "safe": [
    0,
    1,
    2,
    3
  ]
}

Claim and evidence

{
  "claim": {
    "invariant_holds": true
  },
  "witness": {
    "reachable": [
      0,
      1,
      2,
      3
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 4 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

This is a finite safety check; no liveness or fairness statement is included.

A boundary to investigate

Ignoring an enabled transition can make an unsafe system appear safe. Add counterexample paths, temporal properties, and fairness-aware liveness checks.

Verification and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-008 ↘Related KL-FCS-020 ↘

Go further.

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

Questions to investigate

  1. Ignoring an enabled transition can make an unsafe system appear safe.
  2. Which assumption in the specification can be changed to make the current evidence insufficient?
  3. Add counterexample paths, temporal properties, and fairness-aware liveness checks.

Conceptual references

These sources explain the surrounding theory. The linked material was not imported as a dataset, and these records do not claim checking by the source’s software.

Primary conceptual reference ↗

Related areas

Compiler optimizationAbstract interpretationProgram verificationDistributed protocols