Formal Computer Science

KL-FCS-001
AlgorithmsInsertion sort over a finite domainExhaustive bounded validation · 364 inputs

The problem

Sort every list of length 0–5 over {−1, 0, 1}, preserving every occurrence.

The checked result

Correct over the stated input domain: yes.

The candidate shifts larger values to the right before inserting the next value. A separate checker compares every declared input with Python’s reference ordering. Duplicates and the empty list are included.

Why the checker accepts it

Enumerate every list in the declared alphabet and length bound.
Run the candidate insertion-sort implementation without modifying the source input.
Compare each result with the reference ordering, including repeated elements.
Reject immediately with an input witness if ordering or multiplicity differs.

Formal specification

{
  "alphabet": [
    -1,
    0,
    1
  ],
  "max_length": 5
}

Claim and evidence

{
  "claim": {
    "correct_on_declared_domain": true
  },
  "witness": {
    "function": "insertion_sort"
  }
}

Dataset construction

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

Complexity and limits

For alphabet size k and maximum length n, this family checks Σ kⁱ inputs for i=0…n. Insertion sort performs O(n²) comparisons in its worst case.

This is not a general proof for arbitrary lists, a stability proof, or a complexity result.

A boundary to investigate

Sortedness alone does not prove that an output preserves the input multiset. Add stability certificates for tagged records or an unbounded inductive invariant.

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-012 ↘Related KL-FCS-013 ↘

KL-FCS-002
AutomataTwo automata, one parity languageComplete reachable product · 3 state pairs

The problem

Decide whether two complete deterministic automata accept the same binary strings.

The checked result

Equivalent: yes.

Starting from the initial pair, the checker explores every reachable pair of states and requires matching acceptance. No mismatch is reachable, so equivalence holds for every finite binary word. Both accept an even number of ones.

Why the checker accepts it

Start from the pair of initial states.
Explore every symbol transition until no new pair is reachable.
Compare acceptance in every reachable pair.
For inequivalence, replay a distinguishing input from both initial states.

Formal specification

{
  "alphabet": [
    "0",
    "1"
  ],
  "left": {
    "start": "E",
    "accepting": [
      "E"
    ],
    "transitions": {
      "E": {
        "0": "E",
        "1": "O"
      },
      "O": {
        "0": "O",
        "1": "E"
      }
    }
  }
}

Claim and evidence

{
  "claim": {
    "equivalent": true
  },
  "witness": {
    "right": {
      "start": "A",
      "accepting": [
        "A",
        "B"
      ],
      "transitions": {
        "A": {
          "0": "B",
          "1": "C"
        },
        "B": {
          "0": "A",
          "1": "C"
        },
        "C": {
          "0": "C",
          "1": "A"
        }
      }
    }
  }
}

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

At most |Q₁|·|Q₂| product states are visited, with one outgoing edge per alphabet symbol.

Applies only to these two specified complete deterministic automata; no claim of automaton minimality.

A boundary to investigate

Bounded string testing is weaker than complete DFA product exploration. Extend the checker to emit shortest distinguishing words and state-minimization partitions.

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-014 ↘Related KL-FCS-015 ↘

KL-FCS-003
Programming-language semanticsReplay an arithmetic reductionExact reduction replay · 2 steps

The problem

Evaluate (2 × 3) + 4 using left-to-right small-step reduction on integer literals, addition, and multiplication.

The checked result

Normal form: 10.

Every adjacent term must follow the declared reduction rule. The final term is the literal 10 and cannot reduce further.

Why the checker accepts it

Check that the trace begins with the declared syntax tree.
Reduce the left non-literal operand before the right operand.
Apply arithmetic only when both operands are integer literals.
Check each adjacent trace pair and require a terminal integer.

Formal specification

{
  "term": [
    "add",
    [
      "mul",
      2,
      3
    ],
    4
  ],
  "rules": "Reduce the left non-literal operand first, then the right; combine two integer literals."
}

Claim and evidence

{
  "claim": {
    "normal_form": 10
  },
  "witness": {
    "trace": [
      [
        "add",
        [
          "mul",
          2,
          3
        ],
        4
      ],
      [
        "add",
        6,
        4
      ],
      10
    ]
  }
}

Dataset construction

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

Complexity and limits

Replay costs one reduction per arithmetic node, plus traversal to find the next reducible node.

One ground term in a deliberately small language; no general termination or confluence theorem.

A boundary to investigate

A final number alone does not certify the declared evaluation sequence. Introduce variables, environments, conditionals, and explicit stuck-state outcomes.

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-016 ↘Related KL-FCS-017 ↘

KL-FCS-004
Type systemsType a Boolean identity applicationExact type reconstruction · 1 judgment

The problem

Reconstruct the type of (λx:Bool. x) true in the simply typed lambda fragment.

The checked result

Reconstructed type: Bool.

The abstraction has type Bool → Bool. Its argument has type Bool, so application produces Bool. The checker reconstructs these types from syntax and an initially empty context.

Why the checker accepts it

Walk the term recursively from an empty context.
Extend the context when entering an annotated lambda.
Construct arrow types for abstractions.
At each application, check the argument type and return the codomain.

Formal specification

{
  "term": [
    "app",
    [
      "lam",
      "x",
      "Bool",
      [
        "var",
        "x"
      ]
    ],
    [
      "bool",
      true
    ]
  ],
  "rules": "Boolean literals have Bool; variables use the context; abstractions form arrows; applications require an exact domain match."
}

Claim and evidence

{
  "claim": {
    "type": "Bool"
  },
  "witness": {
    "method": "syntax-directed reconstruction"
  }
}

Dataset construction

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

Complexity and limits

The syntax-directed checker visits each term node; context lookup and type comparison add implementation-dependent cost.

A single typing judgment; no proof of type soundness, normalization, or full language implementation.

A boundary to investigate

Being well typed is not, by itself, a proof of preservation or progress. Add independently checked derivation trees and a broader type grammar.

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-018 ↘Related KL-FCS-019 ↘

KL-FCS-005
SAT / SMTA satisfiable CNF with a witnessComplete Boolean enumeration · 4 assignments

The problem

Decide (a ∨ b) ∧ (¬a ∨ b) ∧ (a ∨ ¬b). Signed literals use DIMACS-style variable numbers.

The checked result

Satisfiable: yes.

The supplied model a=true, b=true satisfies all three clauses. Enumeration checks the verdict over every assignment.

Why the checker accepts it

Interpret each literal using its variable number and sign.
Enumerate the entire declared Boolean or bit-vector domain.
Check the supplied model against every constraint.
For unsatisfiability, require complete coverage with no satisfying assignment.

Formal specification

{
  "variables": 2,
  "clauses": [
    [
      1,
      2
    ],
    [
      -1,
      2
    ],
    [
      1,
      -2
    ]
  ]
}

Claim and evidence

{
  "claim": {
    "satisfiable": true
  },
  "witness": {
    "assignment": [
      true,
      true
    ]
  }
}

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

Boolean enumeration examines 2ⁿ assignments. A width-w unary bit-vector instance examines 2ʷ values.

A tiny propositional instance; no solver performance claim or general SAT algorithm benchmark.

A boundary to investigate

A solver’s unverified UNSAT verdict is not a certificate. Fixed-width overflow is part of the theory. Add checked UNSAT proof formats and solver-backed artifacts with pinned versions.

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-006 ↘Related KL-FCS-007 ↘

KL-FCS-006
SAT / SMTAn unsatisfiable CNFComplete Boolean enumeration · 2 assignments

The problem

Decide a ∧ ¬a.

The checked result

Satisfiable: no.

When a is false, the first clause fails. When a is true, the second clause fails. Enumeration covers the entire domain.

Why the checker accepts it

Interpret each literal using its variable number and sign.
Enumerate the entire declared Boolean or bit-vector domain.
Check the supplied model against every constraint.
For unsatisfiability, require complete coverage with no satisfying assignment.

Formal specification

{
  "variables": 1,
  "clauses": [
    [
      1
    ],
    [
      -1
    ]
  ]
}

Claim and evidence

{
  "claim": {
    "satisfiable": false
  },
  "witness": {
    "method": "exhaustive enumeration"
  }
}

Dataset construction

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

Complexity and limits

Boolean enumeration examines 2ⁿ assignments. A width-w unary bit-vector instance examines 2ʷ values.

Exhaustive enumeration is the certificate method here. This is not a DRAT/LRAT proof or a scalable UNSAT benchmark.

A boundary to investigate

A solver’s unverified UNSAT verdict is not a certificate. Fixed-width overflow is part of the theory. Add checked UNSAT proof formats and solver-backed artifacts with pinned versions.

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-005 ↘Related KL-FCS-007 ↘

KL-FCS-007
SAT / SMTA four-bit wraparound modelComplete bit-vector enumeration · 16 values

The problem

Solve x + 1 = 0 in unsigned four-bit bit-vector arithmetic.

The checked result

Solutions: [15].

The value 15 wraps to 0 after adding 1. All other four-bit values fail the equality.

Why the checker accepts it

Interpret each literal using its variable number and sign.
Enumerate the entire declared Boolean or bit-vector domain.
Check the supplied model against every constraint.
For unsatisfiability, require complete coverage with no satisfying assignment.

Formal specification

{
  "width": 4,
  "addend": 1,
  "rhs": 0,
  "theory": "Unsigned four-bit values; addition modulo 16."
}

Claim and evidence

{
  "claim": {
    "solutions": [
      15
    ]
  },
  "witness": {
    "x": 15
  }
}

Dataset construction

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

Complexity and limits

Boolean enumeration examines 2ⁿ assignments. A width-w unary bit-vector instance examines 2ʷ values.

A fixed bit-vector theory example checked by enumeration, not an SMT-solver run or a statement about unbounded integers.

A boundary to investigate

A solver’s unverified UNSAT verdict is not a certificate. Fixed-width overflow is part of the theory. Add checked UNSAT proof formats and solver-backed artifacts with pinned versions.

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-005 ↘Related KL-FCS-006 ↘

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

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.

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-009
Circuit minimizationXOR with a minimum NAND countWitness truth table + complete smaller-circuit search

The problem

Find the fewest two-input NAND gates for XOR(a,b), with acyclic wiring, reusable signals, unrestricted fan-out, no constants, and one gate-output signal.

The checked result

Minimum gates: 4.

The four-gate witness yields the XOR truth table. The checker enumerates every topologically ordered circuit with fewer than four gates, identifying symmetric NAND inputs, and finds none that implements XOR.

Why the checker accepts it

Evaluate the witness circuit in topological signal order.
Compare its complete truth table with the target function.
Enumerate all smaller acyclic circuits, identifying symmetric NAND inputs.
Reject minimality if any smaller circuit implements the target.

Formal specification

{
  "truth_table": 6,
  "row_order": "00, 01, 10, 11; row i is bit i",
  "gate_basis": "two-input NAND; repeated inputs permitted; no constants"
}

Claim and evidence

{
  "claim": {
    "minimum_gates": 4
  },
  "witness": {
    "gates": [
      [
        0,
        1
      ],
      [
        0,
        2
      ],
      [
        1,
        2
      ],
      [
        3,
        4
      ]
    ]
  }
}

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

The circuit search grows rapidly with gate count. This family keeps two inputs and at most four witness gates.

Minimality is relative to this precise gate basis and wiring model. It says nothing about transistor count, delay, power, or other gate libraries.

A boundary to investigate

Gate-count minimality does not imply minimum delay, energy, area, or transistor count. Add independently checked lower bounds and additional gate libraries.

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-022 ↘Related KL-FCS-023 ↘

KL-FCS-010
SchedulingAn optimal two-machine scheduleComplete assignment enumeration · 8 schedules

The problem

Schedule independent, non-preemptive jobs with durations [2, 2, 1] on two identical machines, all available at time zero, to minimize makespan.

The checked result

Minimum makespan: 3.

Assign the first and third jobs to machine 0 and the second to machine 1. Loads are 3 and 2. Enumeration of every assignment establishes the optimum; job order does not affect loads in this model.

Why the checker accepts it

Enumerate every job-to-machine assignment.
Sum the durations assigned to each machine.
Evaluate makespan as the maximum load.
Check that the witness achieves the minimum across all assignments.

Formal specification

{
  "durations": [
    2,
    2,
    1
  ],
  "machines": 2,
  "constraints": "No precedence, setup time, release delay, or preemption; each machine runs its assigned jobs sequentially."
}

Claim and evidence

{
  "claim": {
    "minimum_makespan": 3
  },
  "witness": {
    "assignment": [
      0,
      1,
      0
    ]
  }
}

Dataset construction

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

Complexity and limits

m machines and n jobs produce mⁿ assignments. In this model, job order within a machine does not change the load.

Only this job set and scheduling model; additional constraints require a new specification and checker.

A boundary to investigate

A balanced-looking schedule need not be optimal; release dates and precedence change the problem. Add precedence-constrained schedules and dual or lower-bound certificates.

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-024 ↘Related KL-FCS-025 ↘

KL-FCS-011
Compiler optimizationStrength reduction under modular arithmeticComplete bit-vector equivalence · 16 inputs

The problem

Check the rewrite x × 2 → x + x for every unsigned four-bit x.

The checked result

Equivalent: yes.

For each possible input, the original and replacement expressions yield the same four-bit result, including values that wrap.

Why the checker accepts it

Enumerate every value at the chosen bit width.
Evaluate the source expression modulo 2ʷ.
Evaluate the replacement under the same semantics.
Compare outputs, including wraparound inputs.

Formal specification

{
  "width": 4,
  "source": "x * 2",
  "semantics": "Pure expressions on four-bit values, with both operators modulo 16 and no observable side effects."
}

Claim and evidence

{
  "claim": {
    "equivalent": true
  },
  "witness": {
    "replacement": "x + x"
  }
}

Dataset construction

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

Complexity and limits

Unary width-w equivalence by enumeration checks 2ʷ inputs. This is practical for small widths, not a general large-program optimizer.

This example does not establish a rewrite for language undefined behavior, side effects, overflow flags, other widths, or floating-point arithmetic. No speedup is claimed.

A boundary to investigate

Correctness is not a speedup claim; duplicating an expression with side effects can be invalid. Add expression DAGs, observable-state semantics, and checked equivalence certificates.

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-026 ↘Related KL-FCS-027 ↘

KL-FCS-012
AlgorithmsLonger binary listsComplete bounded enumeration · 511 inputs

The problem

Sort every list of length at most 8 over [0, 1].

The checked result

Correct over the stated input domain: yes.

The alphabet and bound jointly define the dataset. Every list is compared with a reference result; the declared domain includes duplicates, reversed lists, and empty input.

Why the checker accepts it

Enumerate every list in the declared alphabet and length bound.
Run the candidate insertion-sort implementation without modifying the source input.
Compare each result with the reference ordering, including repeated elements.
Reject immediately with an input witness if ordering or multiplicity differs.

Formal specification

{
  "alphabet": [
    0,
    1
  ],
  "max_length": 8
}

Claim and evidence

{
  "claim": {
    "correct_on_declared_domain": true
  },
  "witness": {
    "function": "insertion_sort"
  }
}

Dataset construction

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

Complexity and limits

For alphabet size k and maximum length n, this family checks Σ kⁱ inputs for i=0…n. Insertion sort performs O(n²) comparisons in its worst case.

This finite acceptance result does not establish an unrestricted algorithm theorem.

A boundary to investigate

Sortedness alone does not prove that an output preserves the input multiset. Add stability certificates for tagged records or an unbounded inductive invariant.

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-001 ↘Related KL-FCS-013 ↘

KL-FCS-013
AlgorithmsFive-symbol sorting domainComplete bounded enumeration · 781 inputs

The problem

Sort every list of length at most 4 over [-2, -1, 0, 1, 2].

The checked result

Correct over the stated input domain: yes.

The alphabet and bound jointly define the dataset. Every list is compared with a reference result; the declared domain includes duplicates, reversed lists, and empty input.

Why the checker accepts it

Enumerate every list in the declared alphabet and length bound.
Run the candidate insertion-sort implementation without modifying the source input.
Compare each result with the reference ordering, including repeated elements.
Reject immediately with an input witness if ordering or multiplicity differs.

Formal specification

{
  "alphabet": [
    -2,
    -1,
    0,
    1,
    2
  ],
  "max_length": 4
}

Claim and evidence

{
  "claim": {
    "correct_on_declared_domain": true
  },
  "witness": {
    "function": "insertion_sort"
  }
}

Dataset construction

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

Complexity and limits

For alphabet size k and maximum length n, this family checks Σ kⁱ inputs for i=0…n. Insertion sort performs O(n²) comparisons in its worst case.

This finite acceptance result does not establish an unrestricted algorithm theorem.

A boundary to investigate

Sortedness alone does not prove that an output preserves the input multiset. Add stability certificates for tagged records or an unbounded inductive invariant.

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-001 ↘Related KL-FCS-012 ↘

KL-FCS-014
AutomataParity language under renamingComplete product reachability

The problem

Compare two isomorphic parity automata.

The checked result

Equivalent: yes.

Renaming states preserves transitions and acceptance. The checker establishes equivalence over every finite binary word.

Why the checker accepts it

Start from the pair of initial states.
Explore every symbol transition until no new pair is reachable.
Compare acceptance in every reachable pair.
For inequivalence, replay a distinguishing input from both initial states.

Formal specification

{
  "alphabet": [
    "0",
    "1"
  ],
  "left": {
    "start": "E",
    "accepting": [
      "E"
    ],
    "transitions": {
      "E": {
        "0": "E",
        "1": "O"
      },
      "O": {
        "0": "O",
        "1": "E"
      }
    }
  }
}

Claim and evidence

{
  "claim": {
    "equivalent": true
  },
  "witness": {
    "right": {
      "start": "S",
      "accepting": [
        "S"
      ],
      "transitions": {
        "S": {
          "0": "S",
          "1": "T"
        },
        "T": {
          "0": "T",
          "1": "S"
        }
      }
    }
  }
}

Dataset construction

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

Complexity and limits

At most |Q₁|·|Q₂| product states are visited, with one outgoing edge per alphabet symbol.

This certificate concerns the declared deterministic machines only.

A boundary to investigate

Bounded string testing is weaker than complete DFA product exploration. Extend the checker to emit shortest distinguishing words and state-minimization partitions.

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-002 ↘Related KL-FCS-015 ↘

KL-FCS-015
AutomataA one-symbol counterexampleComplete product + distinguishing-word replay

The problem

Compare even-parity acceptance with the same transitions but odd-parity acceptance.

The checked result

Equivalent: no.

Reading 1 moves both machines to O. The first rejects and the second accepts. The witness refutes equivalence immediately.

Why the checker accepts it

Start from the pair of initial states.
Explore every symbol transition until no new pair is reachable.
Compare acceptance in every reachable pair.
For inequivalence, replay a distinguishing input from both initial states.

Formal specification

{
  "alphabet": [
    "0",
    "1"
  ],
  "left": {
    "start": "E",
    "accepting": [
      "E"
    ],
    "transitions": {
      "E": {
        "0": "E",
        "1": "O"
      },
      "O": {
        "0": "O",
        "1": "E"
      }
    }
  }
}

Claim and evidence

{
  "claim": {
    "equivalent": false
  },
  "witness": {
    "right": {
      "start": "E",
      "accepting": [
        "O"
      ],
      "transitions": {
        "E": {
          "0": "E",
          "1": "O"
        },
        "O": {
          "0": "O",
          "1": "E"
        }
      }
    },
    "distinguishing_word": "1"
  }
}

Dataset construction

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

Complexity and limits

At most |Q₁|·|Q₂| product states are visited, with one outgoing edge per alphabet symbol.

A counterexample is sufficient for inequivalence; it does not characterize all differing inputs.

A boundary to investigate

Bounded string testing is weaker than complete DFA product exploration. Extend the checker to emit shortest distinguishing words and state-minimization partitions.

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-002 ↘Related KL-FCS-014 ↘

KL-FCS-016
Programming-language semanticsEvaluation order in a nested productExact reduction replay · 3 steps

The problem

Replay left-to-right integer arithmetic with add and mul nodes.

The checked result

Normal form: 21.

The trace records intermediate terms, so the result’s derivation and the evaluation order are both inspectable.

Why the checker accepts it

Check that the trace begins with the declared syntax tree.
Reduce the left non-literal operand before the right operand.
Apply arithmetic only when both operands are integer literals.
Check each adjacent trace pair and require a terminal integer.

Formal specification

{
  "term": [
    "mul",
    [
      "add",
      1,
      2
    ],
    [
      "add",
      3,
      4
    ]
  ],
  "rules": "Left non-literal operand first, then right; integer arithmetic without overflow."
}

Claim and evidence

{
  "claim": {
    "normal_form": 21
  },
  "witness": {
    "trace": [
      [
        "mul",
        [
          "add",
          1,
          2
        ],
        [
          "add",
          3,
          4
        ]
      ],
      [
        "mul",
        3,
        [
          "add",
          3,
          4
        ]
      ],
      [
        "mul",
        3,
        7
      ],
      21
    ]
  }
}

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

Replay costs one reduction per arithmetic node, plus traversal to find the next reducible node.

This language uses mathematical integers and no side effects; machine overflow requires different semantics.

A boundary to investigate

A final number alone does not certify the declared evaluation sequence. Introduce variables, environments, conditionals, and explicit stuck-state outcomes.

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-003 ↘Related KL-FCS-017 ↘

KL-FCS-017
Programming-language semanticsSigned integer reductionExact reduction replay · 3 steps

The problem

Replay left-to-right integer arithmetic with add and mul nodes.

The checked result

Normal form: 14.

The trace records intermediate terms, so the result’s derivation and the evaluation order are both inspectable.

Why the checker accepts it

Check that the trace begins with the declared syntax tree.
Reduce the left non-literal operand before the right operand.
Apply arithmetic only when both operands are integer literals.
Check each adjacent trace pair and require a terminal integer.

Formal specification

{
  "term": [
    "add",
    [
      "mul",
      -2,
      3
    ],
    [
      "mul",
      4,
      5
    ]
  ],
  "rules": "Left non-literal operand first, then right; integer arithmetic without overflow."
}

Claim and evidence

{
  "claim": {
    "normal_form": 14
  },
  "witness": {
    "trace": [
      [
        "add",
        [
          "mul",
          -2,
          3
        ],
        [
          "mul",
          4,
          5
        ]
      ],
      [
        "add",
        -6,
        [
          "mul",
          4,
          5
        ]
      ],
      [
        "add",
        -6,
        20
      ],
      14
    ]
  }
}

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

Replay costs one reduction per arithmetic node, plus traversal to find the next reducible node.

This language uses mathematical integers and no side effects; machine overflow requires different semantics.

A boundary to investigate

A final number alone does not certify the declared evaluation sequence. Introduce variables, environments, conditionals, and explicit stuck-state outcomes.

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-003 ↘Related KL-FCS-016 ↘

KL-FCS-018
Type systemsThe Boolean identity functionExact syntax-directed typing judgment

The problem

Reconstruct the type under Boolean binders and lexical scope.

The checked result

Reconstructed type: ["arrow", "Bool", "Bool"].

The binder extends the context for its body. The inner lambda preserves access to outer bindings, and the resulting type records each input separately.

Why the checker accepts it

Walk the term recursively from an empty context.
Extend the context when entering an annotated lambda.
Construct arrow types for abstractions.
At each application, check the argument type and return the codomain.

Formal specification

{
  "term": [
    "lam",
    "x",
    "Bool",
    [
      "var",
      "x"
    ]
  ],
  "rules": "Boolean literals, contextual variables, annotated lambdas, and exact-domain applications."
}

Claim and evidence

{
  "claim": {
    "type": [
      "arrow",
      "Bool",
      "Bool"
    ]
  },
  "witness": {
    "method": "syntax-directed reconstruction"
  }
}

Dataset construction

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

Complexity and limits

The syntax-directed checker visits each term node; context lookup and type comparison add implementation-dependent cost.

Only the declared lambda fragment is checked; no inference of polymorphic or dependent types occurs.

A boundary to investigate

Being well typed is not, by itself, a proof of preservation or progress. Add independently checked derivation trees and a broader type grammar.

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-004 ↘Related KL-FCS-019 ↘

KL-FCS-019
Type systemsA curried constant functionExact syntax-directed typing judgment

The problem

Reconstruct the type under Boolean binders and lexical scope.

The checked result

Reconstructed type: ["arrow", "Bool", ["arrow", "Bool", "Bool"]].

The binder extends the context for its body. The inner lambda preserves access to outer bindings, and the resulting type records each input separately.

Why the checker accepts it

Walk the term recursively from an empty context.
Extend the context when entering an annotated lambda.
Construct arrow types for abstractions.
At each application, check the argument type and return the codomain.

Formal specification

{
  "term": [
    "lam",
    "x",
    "Bool",
    [
      "lam",
      "y",
      "Bool",
      [
        "var",
        "x"
      ]
    ]
  ],
  "rules": "Boolean literals, contextual variables, annotated lambdas, and exact-domain applications."
}

Claim and evidence

{
  "claim": {
    "type": [
      "arrow",
      "Bool",
      [
        "arrow",
        "Bool",
        "Bool"
      ]
    ]
  },
  "witness": {
    "method": "syntax-directed reconstruction"
  }
}

Dataset construction

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

Complexity and limits

The syntax-directed checker visits each term node; context lookup and type comparison add implementation-dependent cost.

Only the declared lambda fragment is checked; no inference of polymorphic or dependent types occurs.

A boundary to investigate

Being well typed is not, by itself, a proof of preservation or progress. Add independently checked derivation trees and a broader type grammar.

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-004 ↘Related KL-FCS-018 ↘

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

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.

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

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.

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 ↘

KL-FCS-022
Circuit minimizationNegation from a repeated NAND inputComplete truth table + zero-gate lower bound

The problem

Minimize the gate count for the declared two-input truth-table signature.

The checked result

Minimum gates: 1.

A single NAND gate supplies the target. Neither available input wire has the same signature, so no zero-gate implementation exists.

Why the checker accepts it

Evaluate the witness circuit in topological signal order.
Compare its complete truth table with the target function.
Enumerate all smaller acyclic circuits, identifying symmetric NAND inputs.
Reject minimality if any smaller circuit implements the target.

Formal specification

{
  "truth_table": 3,
  "row_order": "00, 01, 10, 11; row i is bit i",
  "gate_basis": "two-input NAND; repeated inputs allowed; no constants"
}

Claim and evidence

{
  "claim": {
    "minimum_gates": 1
  },
  "witness": {
    "gates": [
      [
        0,
        0
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

The circuit search grows rapidly with gate count. This family keeps two inputs and at most four witness gates.

The lower bound applies only to the specified two-input NAND basis.

A boundary to investigate

Gate-count minimality does not imply minimum delay, energy, area, or transistor count. Add independently checked lower bounds and additional gate libraries.

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-009 ↘Related KL-FCS-023 ↘

KL-FCS-023
Circuit minimizationThe NAND primitive is minimalComplete truth table + zero-gate lower bound

The problem

Minimize the gate count for the declared two-input truth-table signature.

The checked result

Minimum gates: 1.

A single NAND gate supplies the target. Neither available input wire has the same signature, so no zero-gate implementation exists.

Why the checker accepts it

Evaluate the witness circuit in topological signal order.
Compare its complete truth table with the target function.
Enumerate all smaller acyclic circuits, identifying symmetric NAND inputs.
Reject minimality if any smaller circuit implements the target.

Formal specification

{
  "truth_table": 7,
  "row_order": "00, 01, 10, 11; row i is bit i",
  "gate_basis": "two-input NAND; repeated inputs allowed; no constants"
}

Claim and evidence

{
  "claim": {
    "minimum_gates": 1
  },
  "witness": {
    "gates": [
      [
        0,
        1
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

The circuit search grows rapidly with gate count. This family keeps two inputs and at most four witness gates.

The lower bound applies only to the specified two-input NAND basis.

A boundary to investigate

Gate-count minimality does not imply minimum delay, energy, area, or transistor count. Add independently checked lower bounds and additional gate libraries.

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-009 ↘Related KL-FCS-022 ↘

KL-FCS-024
SchedulingA perfectly balanced four-job scheduleComplete assignment space · 16 schedules

The problem

Minimize makespan for independent jobs on identical machines.

The checked result

Minimum makespan: 4.

The witness lists one machine per job. Feasibility follows from sequential execution on each machine, and enumeration establishes the minimum load ceiling.

Why the checker accepts it

Enumerate every job-to-machine assignment.
Sum the durations assigned to each machine.
Evaluate makespan as the maximum load.
Check that the witness achieves the minimum across all assignments.

Formal specification

{
  "durations": [
    3,
    2,
    2,
    1
  ],
  "machines": 2,
  "constraints": "Non-preemptive; all available at time zero; no precedence or setup times."
}

Claim and evidence

{
  "claim": {
    "minimum_makespan": 4
  },
  "witness": {
    "assignment": [
      0,
      1,
      1,
      0
    ]
  }
}

Dataset construction

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

Complexity and limits

m machines and n jobs produce mⁿ assignments. In this model, job order within a machine does not change the load.

The model excludes release delays, precedence, heterogeneous machines, and setup costs.

A boundary to investigate

A balanced-looking schedule need not be optimal; release dates and precedence change the problem. Add precedence-constrained schedules and dual or lower-bound certificates.

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-010 ↘Related KL-FCS-025 ↘

KL-FCS-025
SchedulingThree machines and five jobsComplete assignment space · 243 schedules

The problem

Minimize makespan for independent jobs on identical machines.

The checked result

Minimum makespan: 4.

The witness lists one machine per job. Feasibility follows from sequential execution on each machine, and enumeration establishes the minimum load ceiling.

Why the checker accepts it

Enumerate every job-to-machine assignment.
Sum the durations assigned to each machine.
Evaluate makespan as the maximum load.
Check that the witness achieves the minimum across all assignments.

Formal specification

{
  "durations": [
    4,
    3,
    2,
    2,
    1
  ],
  "machines": 3,
  "constraints": "Non-preemptive; all available at time zero; no precedence or setup times."
}

Claim and evidence

{
  "claim": {
    "minimum_makespan": 4
  },
  "witness": {
    "assignment": [
      0,
      1,
      2,
      2,
      1
    ]
  }
}

Dataset construction

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

Complexity and limits

m machines and n jobs produce mⁿ assignments. In this model, job order within a machine does not change the load.

The model excludes release delays, precedence, heterogeneous machines, and setup costs.

A boundary to investigate

A balanced-looking schedule need not be optimal; release dates and precedence change the problem. Add precedence-constrained schedules and dual or lower-bound certificates.

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-010 ↘Related KL-FCS-024 ↘

KL-FCS-026
Compiler optimizationEliminate an eight-bit neutral additionComplete equivalence · 256 inputs

The problem

Check a pure unsigned modular rewrite at every input.

The checked result

Equivalent: yes.

The checker evaluates both expressions at every representable value. Overflow wraps identically in the two expressions.

Why the checker accepts it

Enumerate every value at the chosen bit width.
Evaluate the source expression modulo 2ʷ.
Evaluate the replacement under the same semantics.
Compare outputs, including wraparound inputs.

Formal specification

{
  "width": 8,
  "source": "x + 0",
  "semantics": "Pure unsigned 8-bit arithmetic modulo 256, with no side effects."
}

Claim and evidence

{
  "claim": {
    "equivalent": true
  },
  "witness": {
    "replacement": "x"
  }
}

Dataset construction

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

Complexity and limits

Unary width-w equivalence by enumeration checks 2ʷ inputs. This is practical for small widths, not a general large-program optimizer.

The result does not transfer automatically to signed-overflow undefined behavior or effectful expressions.

A boundary to investigate

Correctness is not a speedup claim; duplicating an expression with side effects can be invalid. Add expression DAGs, observable-state semantics, and checked equivalence certificates.

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-011 ↘Related KL-FCS-027 ↘

KL-FCS-027
Compiler optimizationTriple a six-bit value by additionComplete equivalence · 64 inputs

The problem

Check a pure unsigned modular rewrite at every input.

The checked result

Equivalent: yes.

The checker evaluates both expressions at every representable value. Overflow wraps identically in the two expressions.

Why the checker accepts it

Enumerate every value at the chosen bit width.
Evaluate the source expression modulo 2ʷ.
Evaluate the replacement under the same semantics.
Compare outputs, including wraparound inputs.

Formal specification

{
  "width": 6,
  "source": "x * 3",
  "semantics": "Pure unsigned 6-bit arithmetic modulo 64, with no side effects."
}

Claim and evidence

{
  "claim": {
    "equivalent": true
  },
  "witness": {
    "replacement": "(x + x) + x"
  }
}

Dataset construction

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

Complexity and limits

Unary width-w equivalence by enumeration checks 2ʷ inputs. This is practical for small widths, not a general large-program optimizer.

The result does not transfer automatically to signed-overflow undefined behavior or effectful expressions.

A boundary to investigate

Correctness is not a speedup claim; duplicating an expression with side effects can be invalid. Add expression DAGs, observable-state semantics, and checked equivalence certificates.

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-011 ↘Related KL-FCS-026 ↘

KL-FCS-028
Graph algorithmsA shortest path through an intermediate nodeComplete simple-path enumeration

The problem

Find the minimum weighted directed path from vertex 0 to vertex 3.

The checked result

Minimum distance: 5.

The supplied sequence is a valid path. Every alternative simple path is scored, so equal-cost optima are accepted and longer alternatives are ruled out.

Why the checker accepts it

Enumerate every simple source-to-target path in the small graph.
Compute the total weight of each path.
Find the minimum and accept any witness attaining it.
Check the witness edge sequence and objective.

Formal specification

{
  "vertices": 4,
  "edges": [
    [
      0,
      1,
      2
    ],
    [
      0,
      2,
      5
    ],
    [
      1,
      2,
      1
    ],
    [
      1,
      3,
      6
    ],
    [
      2,
      3,
      2
    ]
  ],
  "start": 0,
  "target": 3
}

Claim and evidence

{
  "claim": {
    "minimum_distance": 5
  },
  "witness": {
    "path": [
      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 3 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

Simple-path enumeration can be exponential; nonnegative weights ensure a shortest path can be chosen simple.

Weights are nonnegative. Negative cycles and unreachable targets require distinct result types.

A boundary to investigate

A locally cheapest outgoing edge need not belong to a globally shortest path. Replace enumeration with distance-label certificates and add max-flow/min-cut records.

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-029 ↘Related KL-FCS-030 ↘

KL-FCS-029
Graph algorithmsTwo equally short pathsComplete simple-path enumeration

The problem

Find the minimum weighted directed path from vertex 0 to vertex 3.

The checked result

Minimum distance: 3.

The supplied sequence is a valid path. Every alternative simple path is scored, so equal-cost optima are accepted and longer alternatives are ruled out.

Why the checker accepts it

Enumerate every simple source-to-target path in the small graph.
Compute the total weight of each path.
Find the minimum and accept any witness attaining it.
Check the witness edge sequence and objective.

Formal specification

{
  "vertices": 4,
  "edges": [
    [
      0,
      1,
      1
    ],
    [
      0,
      2,
      1
    ],
    [
      1,
      3,
      2
    ],
    [
      2,
      3,
      2
    ]
  ],
  "start": 0,
  "target": 3
}

Claim and evidence

{
  "claim": {
    "minimum_distance": 3
  },
  "witness": {
    "path": [
      0,
      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 2 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

Simple-path enumeration can be exponential; nonnegative weights ensure a shortest path can be chosen simple.

Weights are nonnegative. Negative cycles and unreachable targets require distinct result types.

A boundary to investigate

A locally cheapest outgoing edge need not belong to a globally shortest path. Replace enumeration with distance-label certificates and add max-flow/min-cut records.

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-028 ↘Related KL-FCS-030 ↘

KL-FCS-030
Graph algorithmsZero-weight edges without negative cyclesComplete simple-path enumeration

The problem

Find the minimum weighted directed path from vertex 0 to vertex 3.

The checked result

Minimum distance: 1.

The supplied sequence is a valid path. Every alternative simple path is scored, so equal-cost optima are accepted and longer alternatives are ruled out.

Why the checker accepts it

Enumerate every simple source-to-target path in the small graph.
Compute the total weight of each path.
Find the minimum and accept any witness attaining it.
Check the witness edge sequence and objective.

Formal specification

{
  "vertices": 4,
  "edges": [
    [
      0,
      1,
      0
    ],
    [
      1,
      2,
      0
    ],
    [
      0,
      2,
      4
    ],
    [
      2,
      3,
      1
    ],
    [
      1,
      3,
      3
    ]
  ],
  "start": 0,
  "target": 3
}

Claim and evidence

{
  "claim": {
    "minimum_distance": 1
  },
  "witness": {
    "path": [
      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 3 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

Simple-path enumeration can be exponential; nonnegative weights ensure a shortest path can be chosen simple.

Weights are nonnegative. Negative cycles and unreachable targets require distinct result types.

A boundary to investigate

A locally cheapest outgoing edge need not belong to a globally shortest path. Replace enumeration with distance-label certificates and add max-flow/min-cut records.

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-028 ↘Related KL-FCS-029 ↘

KL-FCS-031
Formal languagesBalanced words through length 4Complete bounded membership · 31 candidates

The problem

List every balanced parenthesis word of length at most 4, including the empty word.

The checked result

Accepted words: 4.

A prefix can invalidate a word before its final symbol. The accepted list includes different nesting structures and concatenations, not only fully nested strings.

Why the checker accepts it

Generate every parenthesis string up to the stated length.
Scan each prefix and reject any negative balance.
Accept only strings with terminal balance zero.
Compare the complete accepted-word list and its cardinality.

Formal specification

{
  "max_length": 4,
  "alphabet": [
    "(",
    ")"
  ],
  "language": "Every prefix has nonnegative balance and the terminal balance is zero."
}

Claim and evidence

{
  "claim": {
    "accepted_count": 4
  },
  "witness": {
    "words": [
      "",
      "()",
      "(())",
      "()()"
    ]
  }
}

Dataset construction

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

Complexity and limits

A length bound n produces 2ⁿ⁺¹−1 candidate words; each membership scan takes O(n).

This enumerates a bounded language slice; it is not a grammar-equivalence theorem.

A boundary to investigate

Equal numbers of opening and closing symbols do not guarantee proper nesting. Add context-free grammar membership, CYK charts, and parse-tree certificates.

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-032 ↘Related KL-FCS-033 ↘

KL-FCS-032
Formal languagesBalanced words through length 6Complete bounded membership · 127 candidates

The problem

List every balanced parenthesis word of length at most 6, including the empty word.

The checked result

Accepted words: 9.

A prefix can invalidate a word before its final symbol. The accepted list includes different nesting structures and concatenations, not only fully nested strings.

Why the checker accepts it

Generate every parenthesis string up to the stated length.
Scan each prefix and reject any negative balance.
Accept only strings with terminal balance zero.
Compare the complete accepted-word list and its cardinality.

Formal specification

{
  "max_length": 6,
  "alphabet": [
    "(",
    ")"
  ],
  "language": "Every prefix has nonnegative balance and the terminal balance is zero."
}

Claim and evidence

{
  "claim": {
    "accepted_count": 9
  },
  "witness": {
    "words": [
      "",
      "()",
      "(())",
      "()()",
      "((()))",
      "(()())",
      "(())()",
      "()(())",
      "()()()"
    ]
  }
}

Dataset construction

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

Complexity and limits

A length bound n produces 2ⁿ⁺¹−1 candidate words; each membership scan takes O(n).

This enumerates a bounded language slice; it is not a grammar-equivalence theorem.

A boundary to investigate

Equal numbers of opening and closing symbols do not guarantee proper nesting. Add context-free grammar membership, CYK charts, and parse-tree certificates.

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-031 ↘Related KL-FCS-033 ↘

KL-FCS-033
Formal languagesBalanced words through length 8Complete bounded membership · 511 candidates

The problem

List every balanced parenthesis word of length at most 8, including the empty word.

The checked result

Accepted words: 23.

A prefix can invalidate a word before its final symbol. The accepted list includes different nesting structures and concatenations, not only fully nested strings.

Why the checker accepts it

Generate every parenthesis string up to the stated length.
Scan each prefix and reject any negative balance.
Accept only strings with terminal balance zero.
Compare the complete accepted-word list and its cardinality.

Formal specification

{
  "max_length": 8,
  "alphabet": [
    "(",
    ")"
  ],
  "language": "Every prefix has nonnegative balance and the terminal balance is zero."
}

Claim and evidence

{
  "claim": {
    "accepted_count": 23
  },
  "witness": {
    "words": [
      "",
      "()",
      "(())",
      "()()",
      "((()))",
      "(()())",
      "(())()",
      "()(())",
      "()()()",
      "(((())))",
      "((()()))",
      "((())())",
      "((()))()",
      "(()(()))",
      "(()()())",
      "(()())()",
      "(())(())",
      "(())()()",
      "()((()))",
      "()(()())",
      "()(())()",
      "()()(())",
      "()()()()"
    ]
  }
}

Dataset construction

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

Complexity and limits

A length bound n produces 2ⁿ⁺¹−1 candidate words; each membership scan takes O(n).

This enumerates a bounded language slice; it is not a grammar-equivalence theorem.

A boundary to investigate

Equal numbers of opening and closing symbols do not guarantee proper nesting. Add context-free grammar membership, CYK charts, and parse-tree certificates.

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-031 ↘Related KL-FCS-032 ↘

KL-FCS-034
Term rewritingAll reduction orders through length 4All reduction paths over 31 bounded inputs

The problem

Establish a unique sorted normal form for every bounded binary word.

The checked result

Unique normal forms on the domain: yes.

The checker explores every enabled rewrite, not just the trace shown. Each result preserves the symbol multiset and reaches a block of zeros followed by ones.

Why the checker accepts it

Enumerate every binary word through the declared length.
Explore all possible one-step adjacent rewrites.
Collect terminal words, memoizing the reduction graph.
Require one normal form per input and replay the supplied concrete trace.

Formal specification

{
  "max_length": 4,
  "rule": [
    "10",
    "01"
  ],
  "sample_word": "1100"
}

Claim and evidence

{
  "claim": {
    "unique_normal_forms": true
  },
  "witness": {
    "trace": [
      "1100",
      "1010",
      "0110",
      "0101",
      "0011"
    ]
  }
}

Dataset construction

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

Complexity and limits

Each rewrite decreases the number of inverted 1-before-0 pairs. Exhaustive graph exploration is restricted to the stated length.

The mechanical confluence result is restricted to the declared finite word family.

A boundary to investigate

Two chosen reduction strategies agreeing does not establish that all strategies agree. Publish a general inversion-measure termination argument and a separately checked confluence proof.

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-035 ↘Related KL-FCS-036 ↘

KL-FCS-035
Term rewritingAll reduction orders through length 6All reduction paths over 127 bounded inputs

The problem

Establish a unique sorted normal form for every bounded binary word.

The checked result

Unique normal forms on the domain: yes.

The checker explores every enabled rewrite, not just the trace shown. Each result preserves the symbol multiset and reaches a block of zeros followed by ones.

Why the checker accepts it

Enumerate every binary word through the declared length.
Explore all possible one-step adjacent rewrites.
Collect terminal words, memoizing the reduction graph.
Require one normal form per input and replay the supplied concrete trace.

Formal specification

{
  "max_length": 6,
  "rule": [
    "10",
    "01"
  ],
  "sample_word": "101010"
}

Claim and evidence

{
  "claim": {
    "unique_normal_forms": true
  },
  "witness": {
    "trace": [
      "101010",
      "011010",
      "010110",
      "001110",
      "001101",
      "001011",
      "000111"
    ]
  }
}

Dataset construction

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

Complexity and limits

Each rewrite decreases the number of inverted 1-before-0 pairs. Exhaustive graph exploration is restricted to the stated length.

The mechanical confluence result is restricted to the declared finite word family.

A boundary to investigate

Two chosen reduction strategies agreeing does not establish that all strategies agree. Publish a general inversion-measure termination argument and a separately checked confluence proof.

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-034 ↘Related KL-FCS-036 ↘

KL-FCS-036
Term rewritingAll reduction orders through length 8All reduction paths over 511 bounded inputs

The problem

Establish a unique sorted normal form for every bounded binary word.

The checked result

Unique normal forms on the domain: yes.

The checker explores every enabled rewrite, not just the trace shown. Each result preserves the symbol multiset and reaches a block of zeros followed by ones.

Why the checker accepts it

Enumerate every binary word through the declared length.
Explore all possible one-step adjacent rewrites.
Collect terminal words, memoizing the reduction graph.
Require one normal form per input and replay the supplied concrete trace.

Formal specification

{
  "max_length": 8,
  "rule": [
    "10",
    "01"
  ],
  "sample_word": "11110000"
}

Claim and evidence

{
  "claim": {
    "unique_normal_forms": true
  },
  "witness": {
    "trace": [
      "11110000",
      "11101000",
      "11011000",
      "10111000",
      "01111000",
      "01110100",
      "01101100",
      "01011100",
      "00111100",
      "00111010",
      "00110110",
      "00101110",
      "00011110",
      "00011101",
      "00011011",
      "00010111",
      "00001111"
    ]
  }
}

Dataset construction

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

Complexity and limits

Each rewrite decreases the number of inverted 1-before-0 pairs. Exhaustive graph exploration is restricted to the stated length.

The mechanical confluence result is restricted to the declared finite word family.

A boundary to investigate

Two chosen reduction strategies agreeing does not establish that all strategies agree. Publish a general inversion-measure termination argument and a separately checked confluence proof.

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-034 ↘Related KL-FCS-035 ↘

KL-FCS-037
Abstract interpretationA positive affine transferComplete concrete inputs + interval transfer replay

The problem

Compute sound interval bounds for a sequence of mathematical-integer affine transforms.

The checked result

Sound enclosure: yes; Tight interval bounds: yes.

Endpoint propagation encloses every concrete output. Negative multiplication swaps extrema; multiple transformations compose while preserving containment.

Why the checker accepts it

Start from every integer in the initial interval.
Apply each affine transform to the concrete set.
Apply endpoint arithmetic to the interval, reordering endpoints for negative scales.
Check every concrete value remains enclosed and the final bounds are tight.

Formal specification

{
  "initial_interval": [
    -2,
    3
  ],
  "transforms": [
    [
      2,
      1
    ]
  ]
}

Claim and evidence

{
  "claim": {
    "sound": true,
    "tight_interval": true
  },
  "witness": {
    "intervals": [
      [
        -2,
        3
      ],
      [
        -3,
        7
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

With a concrete interval of k integers and t transformations, this finite replay costs O(kt). Abstract endpoint propagation alone costs O(t).

The abstraction encloses gaps. Machine overflow, branches, and widening are not modeled.

A boundary to investigate

A tight interval can include unattainable interior values; it is not necessarily an exact concrete set. Add control-flow joins, fixed points, widening, and overflow-specific abstractions.

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-038 ↘Related KL-FCS-039 ↘

KL-FCS-038
Abstract interpretationNegative scaling reverses boundsComplete concrete inputs + interval transfer replay

The problem

Compute sound interval bounds for a sequence of mathematical-integer affine transforms.

The checked result

Sound enclosure: yes; Tight interval bounds: yes.

Endpoint propagation encloses every concrete output. Negative multiplication swaps extrema; multiple transformations compose while preserving containment.

Why the checker accepts it

Start from every integer in the initial interval.
Apply each affine transform to the concrete set.
Apply endpoint arithmetic to the interval, reordering endpoints for negative scales.
Check every concrete value remains enclosed and the final bounds are tight.

Formal specification

{
  "initial_interval": [
    -3,
    4
  ],
  "transforms": [
    [
      -2,
      3
    ]
  ]
}

Claim and evidence

{
  "claim": {
    "sound": true,
    "tight_interval": true
  },
  "witness": {
    "intervals": [
      [
        -3,
        4
      ],
      [
        -5,
        9
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

With a concrete interval of k integers and t transformations, this finite replay costs O(kt). Abstract endpoint propagation alone costs O(t).

The abstraction encloses gaps. Machine overflow, branches, and widening are not modeled.

A boundary to investigate

A tight interval can include unattainable interior values; it is not necessarily an exact concrete set. Add control-flow joins, fixed points, widening, and overflow-specific abstractions.

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-037 ↘Related KL-FCS-039 ↘

KL-FCS-039
Abstract interpretationCompose three abstract transfersComplete concrete inputs + interval transfer replay

The problem

Compute sound interval bounds for a sequence of mathematical-integer affine transforms.

The checked result

Sound enclosure: yes; Tight interval bounds: yes.

Endpoint propagation encloses every concrete output. Negative multiplication swaps extrema; multiple transformations compose while preserving containment.

Why the checker accepts it

Start from every integer in the initial interval.
Apply each affine transform to the concrete set.
Apply endpoint arithmetic to the interval, reordering endpoints for negative scales.
Check every concrete value remains enclosed and the final bounds are tight.

Formal specification

{
  "initial_interval": [
    0,
    4
  ],
  "transforms": [
    [
      2,
      1
    ],
    [
      -1,
      5
    ],
    [
      3,
      -2
    ]
  ]
}

Claim and evidence

{
  "claim": {
    "sound": true,
    "tight_interval": true
  },
  "witness": {
    "intervals": [
      [
        0,
        4
      ],
      [
        1,
        9
      ],
      [
        -4,
        4
      ],
      [
        -14,
        10
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

With a concrete interval of k integers and t transformations, this finite replay costs O(kt). Abstract endpoint propagation alone costs O(t).

The abstraction encloses gaps. Machine overflow, branches, and widening are not modeled.

A boundary to investigate

A tight interval can include unattainable interior values; it is not necessarily an exact concrete set. Add control-flow joins, fixed points, widening, and overflow-specific abstractions.

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-037 ↘Related KL-FCS-038 ↘

KL-FCS-040
Program verificationSum-loop obligations for n ≤ 5Complete bounded program family · 6 inputs

The problem

Verify a loop that increments i and then adds i to total, starting from zero.

The checked result

Postcondition holds: yes; Variant decreases: yes.

The invariant explains the partial sum at each boundary. The remaining iteration count strictly decreases, and the exit condition turns the invariant into the postcondition.

Why the checker accepts it

Enumerate every admitted bound n.
Start with i=0 and total=0.
Check 2·total=i(i+1) and the decreasing variant n−i.
Replay the sample trace and require total=n(n+1)/2 at exit.

Formal specification

{
  "program": "sum-first-n",
  "max_n": 5,
  "sample_n": 3,
  "precondition": "n ≥ 0; i=0; total=0",
  "invariant": "2*total = i*(i+1) and 0 ≤ i ≤ n",
  "variant": "n-i"
}

Claim and evidence

{
  "claim": {
    "postcondition_holds": true,
    "variant_decreases": true
  },
  "witness": {
    "trace": [
      [
        0,
        0
      ],
      [
        1,
        1
      ],
      [
        2,
        3
      ],
      [
        3,
        6
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

The family runs Σ n loop iterations for n=0…N, so total replay is O(N²).

This replay checks n through the stated bound; it does not constitute an unrestricted deductive proof.

A boundary to investigate

A postcondition on one execution is weaker than an invariant and a declared input domain. Add inductive proof obligations and externally checked Hoare derivations.

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-041 ↘Related KL-FCS-042 ↘

KL-FCS-041
Program verificationSum-loop obligations for n ≤ 10Complete bounded program family · 11 inputs

The problem

Verify a loop that increments i and then adds i to total, starting from zero.

The checked result

Postcondition holds: yes; Variant decreases: yes.

The invariant explains the partial sum at each boundary. The remaining iteration count strictly decreases, and the exit condition turns the invariant into the postcondition.

Why the checker accepts it

Enumerate every admitted bound n.
Start with i=0 and total=0.
Check 2·total=i(i+1) and the decreasing variant n−i.
Replay the sample trace and require total=n(n+1)/2 at exit.

Formal specification

{
  "program": "sum-first-n",
  "max_n": 10,
  "sample_n": 5,
  "precondition": "n ≥ 0; i=0; total=0",
  "invariant": "2*total = i*(i+1) and 0 ≤ i ≤ n",
  "variant": "n-i"
}

Claim and evidence

{
  "claim": {
    "postcondition_holds": true,
    "variant_decreases": true
  },
  "witness": {
    "trace": [
      [
        0,
        0
      ],
      [
        1,
        1
      ],
      [
        2,
        3
      ],
      [
        3,
        6
      ],
      [
        4,
        10
      ],
      [
        5,
        15
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

The family runs Σ n loop iterations for n=0…N, so total replay is O(N²).

This replay checks n through the stated bound; it does not constitute an unrestricted deductive proof.

A boundary to investigate

A postcondition on one execution is weaker than an invariant and a declared input domain. Add inductive proof obligations and externally checked Hoare derivations.

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-040 ↘Related KL-FCS-042 ↘

KL-FCS-042
Program verificationSum-loop obligations for n ≤ 20Complete bounded program family · 21 inputs

The problem

Verify a loop that increments i and then adds i to total, starting from zero.

The checked result

Postcondition holds: yes; Variant decreases: yes.

The invariant explains the partial sum at each boundary. The remaining iteration count strictly decreases, and the exit condition turns the invariant into the postcondition.

Why the checker accepts it

Enumerate every admitted bound n.
Start with i=0 and total=0.
Check 2·total=i(i+1) and the decreasing variant n−i.
Replay the sample trace and require total=n(n+1)/2 at exit.

Formal specification

{
  "program": "sum-first-n",
  "max_n": 20,
  "sample_n": 8,
  "precondition": "n ≥ 0; i=0; total=0",
  "invariant": "2*total = i*(i+1) and 0 ≤ i ≤ n",
  "variant": "n-i"
}

Claim and evidence

{
  "claim": {
    "postcondition_holds": true,
    "variant_decreases": true
  },
  "witness": {
    "trace": [
      [
        0,
        0
      ],
      [
        1,
        1
      ],
      [
        2,
        3
      ],
      [
        3,
        6
      ],
      [
        4,
        10
      ],
      [
        5,
        15
      ],
      [
        6,
        21
      ],
      [
        7,
        28
      ],
      [
        8,
        36
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

The family runs Σ n loop iterations for n=0…N, so total replay is O(N²).

This replay checks n through the stated bound; it does not constitute an unrestricted deductive proof.

A boundary to investigate

A postcondition on one execution is weaker than an invariant and a declared input domain. Add inductive proof obligations and externally checked Hoare derivations.

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-040 ↘Related KL-FCS-041 ↘

KL-FCS-043
Combinatorial optimizationA four-item capacity decisionComplete subset enumeration · 16 candidates

The problem

Maximize total item value without exceeding the weight capacity.

The checked result

Maximum value: 11.

Each subset is a distinct candidate. The checker independently computes feasibility and objective, accepts any optimal witness, and rejects attractive but overweight selections.

Why the checker accepts it

Enumerate every binary item-selection vector.
Discard selections exceeding capacity.
Compute each remaining total value.
Check that the submitted subset is feasible and attains the maximum.

Formal specification

{
  "items": [
    [
      2,
      3
    ],
    [
      3,
      4
    ],
    [
      4,
      7
    ],
    [
      5,
      8
    ]
  ],
  "capacity": 7,
  "item_encoding": "[weight, value]; index identifies an indivisible item"
}

Claim and evidence

{
  "claim": {
    "maximum_value": 11
  },
  "witness": {
    "selected": [
      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 16 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

n items produce 2ⁿ subsets. Pseudopolynomial dynamic programming offers a different tradeoff for integral capacity.

Only this finite 0/1 instance is certified; no approximation ratio or measured solver speed is claimed.

A boundary to investigate

The highest value-to-weight ratio can fail for indivisible 0/1 items. Add assignment dual certificates, set cover, and branch-and-bound proof logs.

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-044 ↘Related KL-FCS-045 ↘

KL-FCS-044
Combinatorial optimizationValue ties in a five-item knapsackComplete subset enumeration · 32 candidates

The problem

Maximize total item value without exceeding the weight capacity.

The checked result

Maximum value: 15.

Each subset is a distinct candidate. The checker independently computes feasibility and objective, accepts any optimal witness, and rejects attractive but overweight selections.

Why the checker accepts it

Enumerate every binary item-selection vector.
Discard selections exceeding capacity.
Compute each remaining total value.
Check that the submitted subset is feasible and attains the maximum.

Formal specification

{
  "items": [
    [
      1,
      2
    ],
    [
      2,
      4
    ],
    [
      3,
      4
    ],
    [
      4,
      6
    ],
    [
      5,
      9
    ]
  ],
  "capacity": 8,
  "item_encoding": "[weight, value]; index identifies an indivisible item"
}

Claim and evidence

{
  "claim": {
    "maximum_value": 15
  },
  "witness": {
    "selected": [
      0,
      1,
      4
    ]
  }
}

Dataset construction

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

Complexity and limits

n items produce 2ⁿ subsets. Pseudopolynomial dynamic programming offers a different tradeoff for integral capacity.

Only this finite 0/1 instance is certified; no approximation ratio or measured solver speed is claimed.

A boundary to investigate

The highest value-to-weight ratio can fail for indivisible 0/1 items. Add assignment dual certificates, set cover, and branch-and-bound proof logs.

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-043 ↘Related KL-FCS-045 ↘

KL-FCS-045
Combinatorial optimizationSix items and a larger capacityComplete subset enumeration · 64 candidates

The problem

Maximize total item value without exceeding the weight capacity.

The checked result

Maximum value: 22.

Each subset is a distinct candidate. The checker independently computes feasibility and objective, accepts any optimal witness, and rejects attractive but overweight selections.

Why the checker accepts it

Enumerate every binary item-selection vector.
Discard selections exceeding capacity.
Compute each remaining total value.
Check that the submitted subset is feasible and attains the maximum.

Formal specification

{
  "items": [
    [
      2,
      5
    ],
    [
      2,
      4
    ],
    [
      3,
      6
    ],
    [
      4,
      7
    ],
    [
      5,
      11
    ],
    [
      1,
      1
    ]
  ],
  "capacity": 10,
  "item_encoding": "[weight, value]; index identifies an indivisible item"
}

Claim and evidence

{
  "claim": {
    "maximum_value": 22
  },
  "witness": {
    "selected": [
      0,
      2,
      4
    ]
  }
}

Dataset construction

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

Complexity and limits

n items produce 2ⁿ subsets. Pseudopolynomial dynamic programming offers a different tradeoff for integral capacity.

Only this finite 0/1 instance is certified; no approximation ratio or measured solver speed is claimed.

A boundary to investigate

The highest value-to-weight ratio can fail for indivisible 0/1 items. Add assignment dual certificates, set cover, and branch-and-bound proof logs.

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-043 ↘Related KL-FCS-044 ↘

KL-FCS-046
Constraint satisfactionA triangle cannot use two colorsComplete assignment space · 8 candidates

The problem

Decide and count color assignments satisfying every graph edge.

The checked result

Satisfiable: no; Solution count: 0.

Every assignment either yields a fully valid coloring or an edge witnessing failure. Counting includes distinct color labels, so symmetric assignments remain separate.

Why the checker accepts it

Enumerate one color value for each vertex.
Check every edge’s unequal-color constraint.
Count the complete solution space.
Validate a coloring witness, or require enumeration evidence when no model exists.

Formal specification

{
  "vertices": 3,
  "edges": [
    [
      0,
      1
    ],
    [
      1,
      2
    ],
    [
      2,
      0
    ]
  ],
  "colors": 2
}

Claim and evidence

{
  "claim": {
    "satisfiable": false,
    "solution_count": 0
  },
  "witness": {
    "method": "exhaustive enumeration"
  }
}

Dataset construction

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

Complexity and limits

k colors on n vertices produce kⁿ assignments. Color-label permutations can create symmetric solutions.

This is a finite coloring instance; the solution count is not reduced by graph or color symmetries.

A boundary to investigate

Failing to find a solution is not equivalent to proving there is none. Add symmetry reduction and checked propagation or conflict explanations.

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-047 ↘Related KL-FCS-048 ↘

KL-FCS-047
Constraint satisfactionA four-cycle admits two colorsComplete assignment space · 16 candidates

The problem

Decide and count color assignments satisfying every graph edge.

The checked result

Satisfiable: yes; Solution count: 2.

Every assignment either yields a fully valid coloring or an edge witnessing failure. Counting includes distinct color labels, so symmetric assignments remain separate.

Why the checker accepts it

Enumerate one color value for each vertex.
Check every edge’s unequal-color constraint.
Count the complete solution space.
Validate a coloring witness, or require enumeration evidence when no model exists.

Formal specification

{
  "vertices": 4,
  "edges": [
    [
      0,
      1
    ],
    [
      1,
      2
    ],
    [
      2,
      3
    ],
    [
      3,
      0
    ]
  ],
  "colors": 2
}

Claim and evidence

{
  "claim": {
    "satisfiable": true,
    "solution_count": 2
  },
  "witness": {
    "coloring": [
      0,
      1,
      0,
      1
    ]
  }
}

Dataset construction

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

Complexity and limits

k colors on n vertices produce kⁿ assignments. Color-label permutations can create symmetric solutions.

This is a finite coloring instance; the solution count is not reduced by graph or color symmetries.

A boundary to investigate

Failing to find a solution is not equivalent to proving there is none. Add symmetry reduction and checked propagation or conflict explanations.

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-046 ↘Related KL-FCS-048 ↘

KL-FCS-048
Constraint satisfactionFour pairwise adjacent vertices need more colorsComplete assignment space · 81 candidates

The problem

Decide and count color assignments satisfying every graph edge.

The checked result

Satisfiable: no; Solution count: 0.

Every assignment either yields a fully valid coloring or an edge witnessing failure. Counting includes distinct color labels, so symmetric assignments remain separate.

Why the checker accepts it

Enumerate one color value for each vertex.
Check every edge’s unequal-color constraint.
Count the complete solution space.
Validate a coloring witness, or require enumeration evidence when no model exists.

Formal specification

{
  "vertices": 4,
  "edges": [
    [
      0,
      1
    ],
    [
      0,
      2
    ],
    [
      0,
      3
    ],
    [
      1,
      2
    ],
    [
      1,
      3
    ],
    [
      2,
      3
    ]
  ],
  "colors": 3
}

Claim and evidence

{
  "claim": {
    "satisfiable": false,
    "solution_count": 0
  },
  "witness": {
    "method": "exhaustive enumeration"
  }
}

Dataset construction

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

Complexity and limits

k colors on n vertices produce kⁿ assignments. Color-label permutations can create symmetric solutions.

This is a finite coloring instance; the solution count is not reduced by graph or color symmetries.

A boundary to investigate

Failing to find a solution is not equivalent to proving there is none. Add symmetry reduction and checked propagation or conflict explanations.

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-046 ↘Related KL-FCS-047 ↘

KL-FCS-049
Game theoryTake one or two stonesComplete backward classification · 13 states

The problem

Classify each heap size and certify a winning strategy under optimal normal play.

The checked result

Winning heap sizes: [1, 2, 4, 5, 7, 8, 10, 11].

Every winning state has a legal move to a losing state. A losing state has no such move, so the opponent controls the next winning position.

Why the checker accepts it

Set the empty heap to losing.
Process heap sizes in increasing order.
Mark a heap winning if an allowed subtraction reaches a losing heap.
Validate every submitted winning move and every losing-state marker.

Formal specification

{
  "moves": [
    1,
    2
  ],
  "max_heap": 12,
  "terminal_rule": "A player unable to move loses; no draws; perfect information."
}

Claim and evidence

{
  "claim": {
    "winning_positions": [
      1,
      2,
      4,
      5,
      7,
      8,
      10,
      11
    ]
  },
  "witness": {
    "strategy": [
      null,
      1,
      2,
      null,
      1,
      2,
      null,
      1,
      2,
      null,
      1,
      2,
      null
    ]
  }
}

Dataset construction

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

Complexity and limits

N heap sizes with m allowed moves require O(Nm) dynamic-programming checks.

These are finite impartial subtraction games, not equilibrium analyses of simultaneous or imperfect-information games.

A boundary to investigate

A single successful play does not establish a strategy against all opponent choices. Add alternating-player reachability graphs and strategy certificates.

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-050 ↘Related KL-FCS-051 ↘

KL-FCS-050
Game theoryOdd-sized subtraction choicesComplete backward classification · 17 states

The problem

Classify each heap size and certify a winning strategy under optimal normal play.

The checked result

Winning heap sizes: [1, 3, 5, 7, 9, 11, 13, 15].

Every winning state has a legal move to a losing state. A losing state has no such move, so the opponent controls the next winning position.

Why the checker accepts it

Set the empty heap to losing.
Process heap sizes in increasing order.
Mark a heap winning if an allowed subtraction reaches a losing heap.
Validate every submitted winning move and every losing-state marker.

Formal specification

{
  "moves": [
    1,
    3
  ],
  "max_heap": 16,
  "terminal_rule": "A player unable to move loses; no draws; perfect information."
}

Claim and evidence

{
  "claim": {
    "winning_positions": [
      1,
      3,
      5,
      7,
      9,
      11,
      13,
      15
    ]
  },
  "witness": {
    "strategy": [
      null,
      1,
      null,
      1,
      null,
      1,
      null,
      1,
      null,
      1,
      null,
      1,
      null,
      1,
      null,
      1,
      null
    ]
  }
}

Dataset construction

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

Complexity and limits

N heap sizes with m allowed moves require O(Nm) dynamic-programming checks.

These are finite impartial subtraction games, not equilibrium analyses of simultaneous or imperfect-information games.

A boundary to investigate

A single successful play does not establish a strategy against all opponent choices. Add alternating-player reachability graphs and strategy certificates.

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-049 ↘Related KL-FCS-051 ↘

KL-FCS-051
Game theoryA game with a nontrivial move setComplete backward classification · 21 states

The problem

Classify each heap size and certify a winning strategy under optimal normal play.

The checked result

Winning heap sizes: [2, 3, 4, 5, 6, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20].

Every winning state has a legal move to a losing state. A losing state has no such move, so the opponent controls the next winning position.

Why the checker accepts it

Set the empty heap to losing.
Process heap sizes in increasing order.
Mark a heap winning if an allowed subtraction reaches a losing heap.
Validate every submitted winning move and every losing-state marker.

Formal specification

{
  "moves": [
    2,
    3,
    5
  ],
  "max_heap": 20,
  "terminal_rule": "A player unable to move loses; no draws; perfect information."
}

Claim and evidence

{
  "claim": {
    "winning_positions": [
      2,
      3,
      4,
      5,
      6,
      9,
      10,
      11,
      12,
      13,
      16,
      17,
      18,
      19,
      20
    ]
  },
  "witness": {
    "strategy": [
      null,
      null,
      2,
      2,
      3,
      5,
      5,
      null,
      null,
      2,
      2,
      3,
      5,
      5,
      null,
      null,
      2,
      2,
      3,
      5,
      5
    ]
  }
}

Dataset construction

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

Complexity and limits

N heap sizes with m allowed moves require O(Nm) dynamic-programming checks.

These are finite impartial subtraction games, not equilibrium analyses of simultaneous or imperfect-information games.

A boundary to investigate

A single successful play does not establish a strategy against all opponent choices. Add alternating-player reachability graphs and strategy certificates.

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-049 ↘Related KL-FCS-050 ↘

KL-FCS-052
Distributed protocolsAtomic acquisition with two processesComplete reachable interleaving graph

The problem

Check mutual exclusion over all one-shot lock-acquisition interleavings.

The checked result

Mutual exclusion holds: yes.

An atomic acquisition prevents simultaneous entry. A split acquisition can let both processes remember a free lock before either marks it occupied.

Why the checker accepts it

Start all processes outside the critical section with a free lock.
Explore every enabled interleaving to a complete reachable closure.
Check the number of processes in the critical section at each state.
For a failure, replay the provided schedule to the unsafe state.

Formal specification

{
  "processes": 2,
  "mode": "atomic",
  "state_encoding": "process PCs, lock bit, process saved-free bits; PC 0=start, 1=checked, 2=critical, 3=done",
  "atomicity": "Atomic mode tests and acquires together; split mode tests then acquires in separate steps."
}

Claim and evidence

{
  "claim": {
    "mutual_exclusion": true
  },
  "witness": {
    "method": "reachable-state enumeration"
  }
}

Dataset construction

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

Complexity and limits

The finite state space is exponential in the number of processes; this family uses two or three one-shot processes.

This is a shared-memory mutual-exclusion model. It does not verify a network protocol, message loss, liveness, or fairness.

A boundary to investigate

Separating a lock check from acquisition allows another process to observe the same free lock. Extend from shared-memory concurrency to bounded message queues and explicit network faults.

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-053 ↘Related KL-FCS-054 ↘

KL-FCS-053
Distributed protocolsA race between check and acquisitionComplete reachable interleaving graph

The problem

Check mutual exclusion over all one-shot lock-acquisition interleavings.

The checked result

Mutual exclusion holds: no.

An atomic acquisition prevents simultaneous entry. A split acquisition can let both processes remember a free lock before either marks it occupied.

Why the checker accepts it

Start all processes outside the critical section with a free lock.
Explore every enabled interleaving to a complete reachable closure.
Check the number of processes in the critical section at each state.
For a failure, replay the provided schedule to the unsafe state.

Formal specification

{
  "processes": 2,
  "mode": "split",
  "state_encoding": "process PCs, lock bit, process saved-free bits; PC 0=start, 1=checked, 2=critical, 3=done",
  "atomicity": "Atomic mode tests and acquires together; split mode tests then acquires in separate steps."
}

Claim and evidence

{
  "claim": {
    "mutual_exclusion": false
  },
  "witness": {
    "counterexample": [
      [
        0,
        0,
        0,
        0,
        0
      ],
      [
        1,
        0,
        0,
        1,
        0
      ],
      [
        1,
        1,
        0,
        1,
        1
      ],
      [
        2,
        1,
        1,
        1,
        1
      ],
      [
        2,
        2,
        1,
        1,
        1
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

The finite state space is exponential in the number of processes; this family uses two or three one-shot processes.

This is a shared-memory mutual-exclusion model. It does not verify a network protocol, message loss, liveness, or fairness.

A boundary to investigate

Separating a lock check from acquisition allows another process to observe the same free lock. Extend from shared-memory concurrency to bounded message queues and explicit network faults.

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-052 ↘Related KL-FCS-054 ↘

KL-FCS-054
Distributed protocolsAtomic acquisition with three processesComplete reachable interleaving graph

The problem

Check mutual exclusion over all one-shot lock-acquisition interleavings.

The checked result

Mutual exclusion holds: yes.

An atomic acquisition prevents simultaneous entry. A split acquisition can let both processes remember a free lock before either marks it occupied.

Why the checker accepts it

Start all processes outside the critical section with a free lock.
Explore every enabled interleaving to a complete reachable closure.
Check the number of processes in the critical section at each state.
For a failure, replay the provided schedule to the unsafe state.

Formal specification

{
  "processes": 3,
  "mode": "atomic",
  "state_encoding": "process PCs, lock bit, process saved-free bits; PC 0=start, 1=checked, 2=critical, 3=done",
  "atomicity": "Atomic mode tests and acquires together; split mode tests then acquires in separate steps."
}

Claim and evidence

{
  "claim": {
    "mutual_exclusion": true
  },
  "witness": {
    "method": "reachable-state enumeration"
  }
}

Dataset construction

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

Complexity and limits

The finite state space is exponential in the number of processes; this family uses two or three one-shot processes.

This is a shared-memory mutual-exclusion model. It does not verify a network protocol, message loss, liveness, or fairness.

A boundary to investigate

Separating a lock check from acquisition allows another process to observe the same free lock. Extend from shared-memory concurrency to bounded message queues and explicit network faults.

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-052 ↘Related KL-FCS-053 ↘

KL-FCS-055
Information theoryA probability-shaped prefix codeComplete codeword-pair check + exact rational average

The problem

Check binary prefix-freeness and compute exact mean codeword length.

The checked result

Prefix free: yes; Expected bits per symbol: 7/4.

The pairwise check reveals every possible prefix collision. Expected length is an exact fraction, avoiding rounding in the acceptance artifact.

Why the checker accepts it

Require one binary codeword for every declared symbol.
Check every ordered pair for the prefix relation.
Verify symbol probabilities form an exact rational distribution.
Compute the average code length using rational arithmetic.

Formal specification

{
  "probabilities": {
    "A": "1/2",
    "B": "1/4",
    "C": "1/8",
    "D": "1/8"
  }
}

Claim and evidence

{
  "claim": {
    "prefix_free": true,
    "expected_bits": "7/4"
  },
  "witness": {
    "codes": {
      "A": "0",
      "B": "10",
      "C": "110",
      "D": "111"
    }
  }
}

Dataset construction

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

Complexity and limits

With n symbols and maximum code length L, naive pairwise prefix checking is O(n²L).

No entropy estimate or code optimality claim is made. A rejected prefix code is retained as an instructive checked negative result.

A boundary to investigate

Short-looking codewords can be ambiguous; a prefix check does not establish minimum expected length. Add Huffman construction traces, lossless round trips, and exact small-tree optimality certificates.

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-056 ↘Related KL-FCS-057 ↘

KL-FCS-056
Information theoryA fixed-length four-symbol codeComplete codeword-pair check + exact rational average

The problem

Check binary prefix-freeness and compute exact mean codeword length.

The checked result

Prefix free: yes; Expected bits per symbol: 2.

The pairwise check reveals every possible prefix collision. Expected length is an exact fraction, avoiding rounding in the acceptance artifact.

Why the checker accepts it

Require one binary codeword for every declared symbol.
Check every ordered pair for the prefix relation.
Verify symbol probabilities form an exact rational distribution.
Compute the average code length using rational arithmetic.

Formal specification

{
  "probabilities": {
    "A": "1/4",
    "B": "1/4",
    "C": "1/4",
    "D": "1/4"
  }
}

Claim and evidence

{
  "claim": {
    "prefix_free": true,
    "expected_bits": "2"
  },
  "witness": {
    "codes": {
      "A": "00",
      "B": "01",
      "C": "10",
      "D": "11"
    }
  }
}

Dataset construction

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

Complexity and limits

With n symbols and maximum code length L, naive pairwise prefix checking is O(n²L).

No entropy estimate or code optimality claim is made. A rejected prefix code is retained as an instructive checked negative result.

A boundary to investigate

Short-looking codewords can be ambiguous; a prefix check does not establish minimum expected length. Add Huffman construction traces, lossless round trips, and exact small-tree optimality certificates.

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-055 ↘Related KL-FCS-057 ↘

KL-FCS-057
Information theoryA prefix collision as negative evidenceComplete codeword-pair check + exact rational average

The problem

Check binary prefix-freeness and compute exact mean codeword length.

The checked result

Prefix free: no; Expected bits per symbol: 3/2.

The pairwise check reveals every possible prefix collision. Expected length is an exact fraction, avoiding rounding in the acceptance artifact.

Why the checker accepts it

Require one binary codeword for every declared symbol.
Check every ordered pair for the prefix relation.
Verify symbol probabilities form an exact rational distribution.
Compute the average code length using rational arithmetic.

Formal specification

{
  "probabilities": {
    "A": "1/2",
    "B": "1/2"
  }
}

Claim and evidence

{
  "claim": {
    "prefix_free": false,
    "expected_bits": "3/2"
  },
  "witness": {
    "codes": {
      "A": "0",
      "B": "01"
    }
  }
}

Dataset construction

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

Complexity and limits

With n symbols and maximum code length L, naive pairwise prefix checking is O(n²L).

No entropy estimate or code optimality claim is made. A rejected prefix code is retained as an instructive checked negative result.

A boundary to investigate

Short-looking codewords can be ambiguous; a prefix check does not establish minimum expected length. Add Huffman construction traces, lossless round trips, and exact small-tree optimality certificates.

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-055 ↘Related KL-FCS-056 ↘

KL-FCS-058
Finite probabilitySuccess and failure after four stepsExact rational trajectory · 4 transitions

The problem

Compute the exact distribution at each step of a finite Markov chain.

The checked result

Final probability distribution: ["1/16", "15/32", "15/32"].

Each step distributes the current mass across outgoing transitions. Absorbing rows retain their mass, and every row of the artifact preserves total probability one.

Why the checker accepts it

Validate the initial distribution and each matrix row.
Multiply the row distribution by the transition matrix.
Repeat for the exact declared horizon.
Compare every trajectory row and the final rational distribution.

Formal specification

{
  "transition": [
    [
      "1/2",
      "1/4",
      "1/4"
    ],
    [
      "0",
      "1",
      "0"
    ],
    [
      "0",
      "0",
      "1"
    ]
  ],
  "initial": [
    "1",
    "0",
    "0"
  ],
  "steps": 4,
  "semantics": "Discrete time, row-stochastic transition matrix, no nondeterministic scheduler."
}

Claim and evidence

{
  "claim": {
    "distribution": [
      "1/16",
      "15/32",
      "15/32"
    ]
  },
  "witness": {
    "trajectory": [
      [
        "1",
        "0",
        "0"
      ],
      [
        "1/2",
        "1/4",
        "1/4"
      ],
      [
        "1/4",
        "3/8",
        "3/8"
      ],
      [
        "1/8",
        "7/16",
        "7/16"
      ],
      [
        "1/16",
        "15/32",
        "15/32"
      ]
    ]
  }
}

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

A dense n-state chain over h steps costs O(hn²) arithmetic operations, with fraction sizes growing over time.

The result is for the declared horizon. The browser chart uses floating-point display; Python fractions establish the exact certificate.

A boundary to investigate

A finite-horizon probability is not automatically an eventual-reachability answer. Add absorbing-state equations, expected hitting time, and nondeterministic MDP choices.

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-059 ↘Related KL-FCS-060 ↘

KL-FCS-059
Finite probabilityA reversible two-state distributionExact rational trajectory · 6 transitions

The problem

Compute the exact distribution at each step of a finite Markov chain.

The checked result

Final probability distribution: ["2731/4096", "1365/4096"].

Each step distributes the current mass across outgoing transitions. Absorbing rows retain their mass, and every row of the artifact preserves total probability one.

Why the checker accepts it

Validate the initial distribution and each matrix row.
Multiply the row distribution by the transition matrix.
Repeat for the exact declared horizon.
Compare every trajectory row and the final rational distribution.

Formal specification

{
  "transition": [
    [
      "3/4",
      "1/4"
    ],
    [
      "1/2",
      "1/2"
    ]
  ],
  "initial": [
    "1",
    "0"
  ],
  "steps": 6,
  "semantics": "Discrete time, row-stochastic transition matrix, no nondeterministic scheduler."
}

Claim and evidence

{
  "claim": {
    "distribution": [
      "2731/4096",
      "1365/4096"
    ]
  },
  "witness": {
    "trajectory": [
      [
        "1",
        "0"
      ],
      [
        "3/4",
        "1/4"
      ],
      [
        "11/16",
        "5/16"
      ],
      [
        "43/64",
        "21/64"
      ],
      [
        "171/256",
        "85/256"
      ],
      [
        "683/1024",
        "341/1024"
      ],
      [
        "2731/4096",
        "1365/4096"
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

A dense n-state chain over h steps costs O(hn²) arithmetic operations, with fraction sizes growing over time.

The result is for the declared horizon. The browser chart uses floating-point display; Python fractions establish the exact certificate.

A boundary to investigate

A finite-horizon probability is not automatically an eventual-reachability answer. Add absorbing-state equations, expected hitting time, and nondeterministic MDP choices.

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-058 ↘Related KL-FCS-060 ↘

KL-FCS-060
Finite probabilityProgress through two transient statesExact rational trajectory · 8 transitions

The problem

Compute the exact distribution at each step of a finite Markov chain.

The checked result

Final probability distribution: ["1/256", "1/32", "247/256"].

Each step distributes the current mass across outgoing transitions. Absorbing rows retain their mass, and every row of the artifact preserves total probability one.

Why the checker accepts it

Validate the initial distribution and each matrix row.
Multiply the row distribution by the transition matrix.
Repeat for the exact declared horizon.
Compare every trajectory row and the final rational distribution.

Formal specification

{
  "transition": [
    [
      "1/2",
      "1/2",
      "0"
    ],
    [
      "0",
      "1/2",
      "1/2"
    ],
    [
      "0",
      "0",
      "1"
    ]
  ],
  "initial": [
    "1",
    "0",
    "0"
  ],
  "steps": 8,
  "semantics": "Discrete time, row-stochastic transition matrix, no nondeterministic scheduler."
}

Claim and evidence

{
  "claim": {
    "distribution": [
      "1/256",
      "1/32",
      "247/256"
    ]
  },
  "witness": {
    "trajectory": [
      [
        "1",
        "0",
        "0"
      ],
      [
        "1/2",
        "1/2",
        "0"
      ],
      [
        "1/4",
        "1/2",
        "1/4"
      ],
      [
        "1/8",
        "3/8",
        "1/2"
      ],
      [
        "1/16",
        "1/4",
        "11/16"
      ],
      [
        "1/32",
        "5/32",
        "13/16"
      ],
      [
        "1/64",
        "3/32",
        "57/64"
      ],
      [
        "1/128",
        "7/128",
        "15/16"
      ],
      [
        "1/256",
        "1/32",
        "247/256"
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

A dense n-state chain over h steps costs O(hn²) arithmetic operations, with fraction sizes growing over time.

The result is for the declared horizon. The browser chart uses floating-point display; Python fractions establish the exact certificate.

A boundary to investigate

A finite-horizon probability is not automatically an eventual-reachability answer. Add absorbing-state equations, expected hitting time, and nondeterministic MDP choices.

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-058 ↘Related KL-FCS-059 ↘

KL-FCS-061
Relational algebraIntersection distributes over unionComplete relation assignments · 512 triples

The problem

Decide the proposed set identity over every triple of finite-universe relations.

The checked result

Equivalent on the stated domain: yes.

The finite universe makes every relation assignment enumerable. The sample output illustrates the identity or supplies a direct refutation.

Why the checker accepts it

Enumerate every subset of the universe.
Evaluate both expressions on every triple of sets.
Compare the complete finite-domain outputs.
Replay a concrete sample, including a differing output for a false identity.

Formal specification

{
  "universe_size": 3,
  "law": "intersection-distribution",
  "semantics": "Mathematical sets; unique values; no NULL or tuple multiplicity."
}

Claim and evidence

{
  "claim": {
    "equivalent_on_domain": true
  },
  "witness": {
    "sample": {
      "A": [
        0,
        1
      ],
      "B": [
        1,
        2
      ],
      "C": [
        0
      ],
      "left": [
        0,
        1
      ],
      "right": [
        0,
        1
      ]
    }
  }
}

Dataset construction

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

Complexity and limits

A universe of n values has 2ⁿ subsets; three relation inputs create 2³ⁿ assignments.

Finite enumeration is bounded to this universe; these artifacts do not certify an SQL optimizer or measured execution speed.

A boundary to investigate

SQL bag semantics, NULL values, and outer joins can invalidate a rewrite valid for mathematical sets. Add equijoin trees, bag multiplicities, NULL handling, and an explicit query-cost model.

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-062 ↘Related KL-FCS-063 ↘

KL-FCS-062
Relational algebraSubtract after a unionComplete relation assignments · 4096 triples

The problem

Decide the proposed set identity over every triple of finite-universe relations.

The checked result

Equivalent on the stated domain: yes.

The finite universe makes every relation assignment enumerable. The sample output illustrates the identity or supplies a direct refutation.

Why the checker accepts it

Enumerate every subset of the universe.
Evaluate both expressions on every triple of sets.
Compare the complete finite-domain outputs.
Replay a concrete sample, including a differing output for a false identity.

Formal specification

{
  "universe_size": 4,
  "law": "difference-distribution",
  "semantics": "Mathematical sets; unique values; no NULL or tuple multiplicity."
}

Claim and evidence

{
  "claim": {
    "equivalent_on_domain": true
  },
  "witness": {
    "sample": {
      "A": [
        0,
        1
      ],
      "B": [
        1,
        2
      ],
      "C": [
        1
      ],
      "left": [
        0,
        2
      ],
      "right": [
        0,
        2
      ]
    }
  }
}

Dataset construction

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

Complexity and limits

A universe of n values has 2ⁿ subsets; three relation inputs create 2³ⁿ assignments.

Finite enumeration is bounded to this universe; these artifacts do not certify an SQL optimizer or measured execution speed.

A boundary to investigate

SQL bag semantics, NULL values, and outer joins can invalidate a rewrite valid for mathematical sets. Add equijoin trees, bag multiplicities, NULL handling, and an explicit query-cost model.

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-061 ↘Related KL-FCS-063 ↘

KL-FCS-063
Relational algebraSet difference is not commutativeComplete relation assignments · 64 triples

The problem

Decide the proposed set identity over every triple of finite-universe relations.

The checked result

Equivalent on the stated domain: no.

The finite universe makes every relation assignment enumerable. The sample output illustrates the identity or supplies a direct refutation.

Why the checker accepts it

Enumerate every subset of the universe.
Evaluate both expressions on every triple of sets.
Compare the complete finite-domain outputs.
Replay a concrete sample, including a differing output for a false identity.

Formal specification

{
  "universe_size": 2,
  "law": "difference-commutativity",
  "semantics": "Mathematical sets; unique values; no NULL or tuple multiplicity."
}

Claim and evidence

{
  "claim": {
    "equivalent_on_domain": false
  },
  "witness": {
    "sample": {
      "A": [
        0
      ],
      "B": [],
      "C": [],
      "left": [
        0
      ],
      "right": []
    }
  }
}

Dataset construction

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

Complexity and limits

A universe of n values has 2ⁿ subsets; three relation inputs create 2³ⁿ assignments.

Finite enumeration is bounded to this universe; these artifacts do not certify an SQL optimizer or measured execution speed.

A boundary to investigate

SQL bag semantics, NULL values, and outer joins can invalidate a rewrite valid for mathematical sets. Add equijoin trees, bag multiplicities, NULL handling, and an explicit query-cost model.

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-061 ↘Related KL-FCS-062 ↘

KL-FCS-064
Linear algebra over GF(2)Dependent parity equationsElimination + complete kernel · 16 vectors

The problem

Compute rank, nullity, reduced row-echelon form, and the complete binary kernel.

The checked result

Rank: 2; Nullity: 2.

XOR row operations preserve the solution space. Free columns account for the kernel’s degrees of freedom, and full enumeration checks every binary candidate.

Why the checker accepts it

Reduce the binary matrix by row swapping and XOR elimination.
Identify pivot columns and compute rank and nullity.
Enumerate every binary vector of the declared column dimension.
Compare the full kernel list and verify its size against rank-nullity.

Formal specification

{
  "matrix": [
    [
      1,
      1,
      0,
      1
    ],
    [
      0,
      1,
      1,
      0
    ],
    [
      1,
      0,
      1,
      1
    ]
  ],
  "field": "GF(2); column vectors; all dot products modulo two."
}

Claim and evidence

{
  "claim": {
    "rank": 2,
    "nullity": 2
  },
  "witness": {
    "rref": [
      [
        1,
        0,
        1,
        1
      ],
      [
        0,
        1,
        1,
        0
      ],
      [
        0,
        0,
        0,
        0
      ]
    ],
    "kernel": [
      [
        0,
        0,
        0,
        0
      ],
      [
        0,
        1,
        1,
        1
      ],
      [
        1,
        0,
        0,
        1
      ],
      [
        1,
        1,
        1,
        0
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

For m rows and n columns, elimination is polynomial; full kernel enumeration checks 2ⁿ vectors.

Only these exact matrices are certified; the witness is a complete kernel list rather than a scalable basis certificate.

A boundary to investigate

Ordinary real-number arithmetic gives different answers. A few null vectors need not span the kernel. Add row-operation certificates, nullspace bases, and inconsistency witnesses.

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-065 ↘Related KL-FCS-066 ↘

KL-FCS-065
Linear algebra over GF(2)An invertible binary identity matrixElimination + complete kernel · 8 vectors

The problem

Compute rank, nullity, reduced row-echelon form, and the complete binary kernel.

The checked result

Rank: 3; Nullity: 0.

XOR row operations preserve the solution space. Free columns account for the kernel’s degrees of freedom, and full enumeration checks every binary candidate.

Why the checker accepts it

Reduce the binary matrix by row swapping and XOR elimination.
Identify pivot columns and compute rank and nullity.
Enumerate every binary vector of the declared column dimension.
Compare the full kernel list and verify its size against rank-nullity.

Formal specification

{
  "matrix": [
    [
      1,
      0,
      0
    ],
    [
      0,
      1,
      0
    ],
    [
      0,
      0,
      1
    ]
  ],
  "field": "GF(2); column vectors; all dot products modulo two."
}

Claim and evidence

{
  "claim": {
    "rank": 3,
    "nullity": 0
  },
  "witness": {
    "rref": [
      [
        1,
        0,
        0
      ],
      [
        0,
        1,
        0
      ],
      [
        0,
        0,
        1
      ]
    ],
    "kernel": [
      [
        0,
        0,
        0
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

For m rows and n columns, elimination is polynomial; full kernel enumeration checks 2ⁿ vectors.

Only these exact matrices are certified; the witness is a complete kernel list rather than a scalable basis certificate.

A boundary to investigate

Ordinary real-number arithmetic gives different answers. A few null vectors need not span the kernel. Add row-operation certificates, nullspace bases, and inconsistency witnesses.

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-064 ↘Related KL-FCS-066 ↘

KL-FCS-066
Linear algebra over GF(2)One equation with four binary variablesElimination + complete kernel · 16 vectors

The problem

Compute rank, nullity, reduced row-echelon form, and the complete binary kernel.

The checked result

Rank: 1; Nullity: 3.

XOR row operations preserve the solution space. Free columns account for the kernel’s degrees of freedom, and full enumeration checks every binary candidate.

Why the checker accepts it

Reduce the binary matrix by row swapping and XOR elimination.
Identify pivot columns and compute rank and nullity.
Enumerate every binary vector of the declared column dimension.
Compare the full kernel list and verify its size against rank-nullity.

Formal specification

{
  "matrix": [
    [
      1,
      1,
      1,
      1
    ],
    [
      1,
      1,
      1,
      1
    ]
  ],
  "field": "GF(2); column vectors; all dot products modulo two."
}

Claim and evidence

{
  "claim": {
    "rank": 1,
    "nullity": 3
  },
  "witness": {
    "rref": [
      [
        1,
        1,
        1,
        1
      ],
      [
        0,
        0,
        0,
        0
      ]
    ],
    "kernel": [
      [
        0,
        0,
        0,
        0
      ],
      [
        0,
        0,
        1,
        1
      ],
      [
        0,
        1,
        0,
        1
      ],
      [
        0,
        1,
        1,
        0
      ],
      [
        1,
        0,
        0,
        1
      ],
      [
        1,
        0,
        1,
        0
      ],
      [
        1,
        1,
        0,
        0
      ],
      [
        1,
        1,
        1,
        1
      ]
    ]
  }
}

Dataset construction

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

Complexity and limits

For m rows and n columns, elimination is polynomial; full kernel enumeration checks 2ⁿ vectors.

Only these exact matrices are certified; the witness is a complete kernel list rather than a scalable basis certificate.

A boundary to investigate

Ordinary real-number arithmetic gives different answers. A few null vectors need not span the kernel. Add row-operation certificates, nullspace bases, and inconsistency witnesses.

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-064 ↘Related KL-FCS-065 ↘

FormalComputerScience.

Explore the areas.

Algorithms ↗

Automata ↗

Programming-language semantics ↗

Type systems ↗

SAT / SMT ↗

Model checking ↗

Circuit minimization ↗

Scheduling ↗

Compiler optimization ↗

Graph algorithms ↗

Formal languages ↗

Term rewriting ↗

Abstract interpretation ↗

Program verification ↗

Combinatorial optimization ↗

Constraint satisfaction ↗

Game theory ↗

Distributed protocols ↗

Information theory ↗

Finite probability ↗

Relational algebra ↗

Linear algebra over GF(2) ↗

Work through the mechanics.

Inspect the records.

The problem

The checked result

Why the checker accepts it

Formal specification

Claim and evidence

Dataset construction

Complexity and limits

A boundary to investigate

The problem

The checked result

Why the checker accepts it

Formal specification

Claim and evidence

Dataset construction

Complexity and limits

A boundary to investigate

The problem

The checked result

Why the checker accepts it

Formal specification

Claim and evidence

Dataset construction

Complexity and limits

A boundary to investigate

The problem

The checked result

Why the checker accepts it

Formal specification

Claim and evidence

Dataset construction

Complexity and limits

A boundary to investigate

The problem

The checked result

Why the checker accepts it

Formal specification

Claim and evidence

Dataset construction

Complexity and limits

A boundary to investigate

The problem

The checked result

Why the checker accepts it

Formal specification

Claim and evidence

Dataset construction

Complexity and limits

A boundary to investigate

The problem

The checked result

Why the checker accepts it

Formal specification

Claim and evidence

Dataset construction

Formal
Computer
Science.