Formal BMC bound

Sketch bounded model checking: set bugAt step and bound k, then Run BMC. If k ≥ bugAt → CEX; else PASS_BOUND. Depth bars visualize the search horizon. Starter: bug at step 3, k=5 → CEX.