Layer 2 and Layer 3, checked against each other. See "What conformance checks" in guides/reference.md.

They compute over the same specification and never look at one another. Layer 2 says which states are reachable. Layer 3 runs a real GenServer and observes behaviour through a refinement mapping. A trace the implementation produces that is not a path in the checker's graph means one of three things:

1. the implementation is wrong — the finding Layer 3 exists for;
2. the refinement mapping is wrong — ExTLA.Simulation's own stated catch, "a refinement mapping that is wrong in a state no test happened to reach";
3. the search missed a state — a checker defect, found by running code.

A simulation alone considers only the first two, and the third is indistinguishable from them. It is also the one nothing else finds: a running server explores paths driven by real OTP scheduling rather than by the checker's own traversal code, so it can reach a state the search missed.

What is decidable here, and what is not

Given a step the graph does not contain, replaying it against the DSL semantics settles one question completely: does the spec permit it?

• it does, and the graph lacks it — the search missed something. :checker, and the finding this module exists to make.
• it does not — the implementation did something the spec forbids, or the mapping described the step wrongly. :not_a_step_of_the_spec.

That last pair is not split, and not because it is hard: one of the two is wrong, and which one is not something the checker can decide from the step. The same holds for a ExTLA.Replay's :not_followed, and a confident split would be a self-consistent wrong answer. Layer 3's own check_step/5 runs during the simulation and reports its reading; this adds the containment view beside it rather than overruling it.

It declines to answer about a truncated graph

Past max_states, or under a state_constraint, absence from the graph is a fact about the bound rather than about the search. Reporting that as a checker finding would manufacture exactly the false positive that gets a check like this turned off, so the run's status is a required argument and a bounded one is refused.