Report the state and execution bounds behind a successful check

For safety predicate P, bounded model checking asks whether some allowed execution of up to a chosen number of transitions reaches a state violating P. A typical symbolic encoding combines initialization, a chain of transition relations, and a disjunction of bad states. A satisfying assignment supplies a counterexample within the encoding's scope. An unsatisfiable query rules out those bounded witnesses under the encoded domains and assumptions; it does not rule out a longer failure. Solver timeout or unknown is a separate outcome, not evidence that the property passed.

Apalache's documented bounded mode checks execution lengths under a configured limit; its separate induction workflow asks stronger initiation and preservation questions. TLC ordinarily explores reachable states of a concrete model instance rather than merely enumerating one trace. When that reachable graph is finite and its configured exploration completes without a safety violation, the result covers arbitrarily long paths within that finite instance. It still does not generalize to larger constant domains without an additional argument. State the tool version, specification, configuration, property, and completion status when recording either result.

A finite instance can have deep reachable failures and many paths revisiting the same states. Distinct-state exploration avoids treating every repeated path as a new state, but path depth and state count remain different measures. A counter with eight residue values and one Boolean history flag has at most sixteen valuations. Returning to the same residue does not return to the same full state if the flag changed. Dropping that flag can erase the very property being checked, turning a smaller model into a model of a different contract.

Bounds and constraints require a semantic review. Restricting a parameter to three workers defines a finite instance. Artificially pruning states when a queue exceeds two messages can exclude an overflow failure, especially if that boundary is being investigated. The exact order of constraint and property handling is tool-specific, so inspect it rather than using pruning as a hidden proof premise. A valid cutoff theorem can justify a small instance for a particular parameterized property, but the existence of such a theorem must be established rather than inferred from several successful sizes.

Store a failing trace with its specification and configuration, then identify which action first violates the property. Minimize the witness without changing its essential crash, message, or identity assumptions. For successful checks, retain bounds and termination evidence rather than only a green screenshot. A regression suite can compare several small domains and deliberately injected mutants, while an inductive proof or justified reduction addresses a stronger claim. Each method supplies different evidence; their results should not be flattened into a single unqualified 'verified' label.

The modular instrument illustrates a residue that hides history. Reset, set modulus m=8 and additive step a=1, predict residues zero initially, seven after seven transitions, and zero after eight, then take eight Steps. The instrument advances one transition per half-second Step and reports period eight. It has no overflow flag and does not mark the return to zero as an error. The separate counterexample below adds such a flag deliberately. This additive orbit is neither TLC nor a bounded checker and cannot establish that a service's state abstraction preserves its safety property.