Properties can be debugged by the tool; claims about results cannot, because the tool never hears them. Each item below is a sentence candidates actually say, followed by why it is false, the correction, and the lesson that proves the correction. Practise answering each in two sentences: the false part named, the true statement with its evidence.
Job of this lesson: replace six false claims with six true ones, each carrying its evidence.
The claim: the bounded run found a trace but the full proof still passed, so both stand. Why it fails: a counterexample on a model wins over every other reading of the same model, assumptions, and reset; an apparent conflict means the models differed. The correction: restate both runs with their assumption lists and find the difference, usually a tightened assumption or a different reset. Say instead: the trace refutes the claim on its model, and the second run must name what changed. Taught in a counterexample always wins; the depth-10 pass and depth-11 failure of one design are in the whiteboard answers.
The claim: the step fails on states that can really happen. Why it fails: the step starts from arbitrary states including ones unreachable from reset, and its failing trace may be spurious; reachable is a subset of possible. The correction: replay the step's start state from reset before calling it a design bug, and strengthen with a helper that excludes the unreachable region. Say instead: the step fails from an unreachable state, and the invariant is missing. Taught in CTIs and unreachable states, where the unreachable chain 10 to 14 breaks the step at every k.
The claim: shrinking the cone removed behaviour and caused the false pass. Why it fails: cone reduction is exact, removing only logic that cannot affect the property; over-constraint comes from assumptions or unsound abstraction, three different things with different cures. The correction: read the assumption list and the abstraction contracts, not the cone report. Say instead: the cone is exact, and the vacuity lives in the assumptions. Taught in COI reduction is exact.
The claim: the liveness property passed without the event because vacuity. Why it fails: vacuity means an antecedent never true; a weak sequence that never completes is unfinished business, not vacuity, and the formal point is sharper: an unconstrained environment makes liveness fail with a starvation trace, never pass. The correction: state liveness with strong forms or bounded windows, and add fairness on environment choices only. Say instead: the property is too weak to fail, and the window plus fairness are missing. Taught in weak and strong in a proof engine, and the bounded form is run in the deadlock scenario.
The claim: the proof spins, so constrain the inputs until it closes. Why it fails: tightening is the last resort with a written justification, because each new rule prunes the shipped behaviour; diagnose cone, depth, and state bits first, then reduce, split, and strengthen. The correction: the ordered response with an honest bounded-to-N interim status. Say instead: the diagnosis comes first, and the assumption ships with an exception note. Taught in diagnose before you tune; the helper that closes what no assumption should is run in the non-convergence scenario.
The claim: the miter passes, therefore the changed block is right. Why it fails: equivalence proves the twins agree, never that either matches the specification; a shared misunderstanding passes perfectly. The correction: pair every miter with the spec properties on at least one side, and pin intended differences with proven per-mode properties. Say instead: the twins agree, and here is the spec proof that they agree on the right thing. Taught in equivalence is not correctness; the intended-difference property is run in the ECO scenario.
Which of the three outcomes it is, with the depth or induction form: closed and converged are not outcomes, and the question exposes whether either hides inconclusive.