k-Induction

You learned mathematical induction in school: prove a base case, then prove that if it holds for $n$ it holds for $n+1$, and you have it for all $n$. The same idea appears in verification: if a system starts safely and every safe state leads to another safe state, the system is always safe.

But there is a subtle trap. The inductive step says: "assume the property holds right now; can it break in the next step?" Sometimes the property is too weak — there exist hypothetical states that satisfy the property but cannot actually be reached, and from one of those phantom states the property breaks. Plain induction fails even though the system is genuinely safe.

k-induction plugs this gap. Instead of one step, it demands that any run of $k$ consecutive states that all satisfy the property must continue satisfying it in step $k+1$. A longer history makes the hypothesis stronger, eventually ruling out the phantom states — and the proof closes.

The technique was formalized by Sheeran, Singh, and Stålmarck in 2000 and quickly became a cornerstone of SAT-based model checking.

The demo below models a tiny counter that must stay below a threshold. Plain induction ($k=1$) fails because the inductive hypothesis is too weak. Raise $k$ with the slider until the proof closes.

<!-- {{c_intro}} -->
<div class="panel">
  <div class="row-label">
    <label for="kSlider">{{lbl_depth}} <strong id="kVal">1</strong></label>
    <input id="kSlider" type="range" min="1" max="10" value="1" />
  </div>
  <div class="row-label">
    <label for="threshSlider">{{lbl_threshold}} <strong id="tVal">5</strong></label>
    <input id="threshSlider" type="range" min="4" max="7" value="5" />
  </div>
</div>
<div id="trace" class="trace"></div>
<div id="status" class="status"></div>
<div class="btns">
  <button id="btnRun" type="button">{{btn_run}}</button>
  <button id="btnReset" type="button" class="ghost">{{btn_reset}}</button>
</div>

/* {{c_style}} */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.panel { display: flex; flex-direction: column; gap: .5rem; margin-bottom: .8rem; }
.row-label { display: flex; align-items: center; gap: .6rem; font-size: .9rem; }
.row-label label { min-width: 9.5rem; }
input[type=range] { flex: 1; accent-color: #1d3557; }
.trace { display: flex; flex-wrap: wrap; gap: 6px; min-height: 2.8rem; margin-bottom: .6rem; align-items: center; }
.state { width: 38px; height: 38px; display: flex; align-items: center; justify-content: center;
         font: 700 13px ui-monospace, monospace; border-radius: 8px; border: 1px solid #adb1b8; }
.state.ok { background: #e8f5e9; border-color: #66bb6a; color: #1b5e20; }
.state.bad { background: #ffebee; border-color: #ef5350; color: #b71c1c; }
.state.init { background: #e3f2fd; border-color: #42a5f5; color: #0d47a1; }
.state.phantom { background: #fff3e0; border-color: #ffa726; color: #e65100; }
.arrow { font-size: 1rem; color: #888; }
.status { font-size: .95rem; font-weight: 600; margin: .5rem 0; min-height: 1.4em; }
.status.pass { color: #0a7d33; }
.status.fail { color: #c92f3c; }
.status.phantom-msg { color: #e65100; }
.legend { font-size: .76rem; color: #555; margin-top: .3rem; display: flex; flex-wrap: wrap; gap: .3rem .8rem; }
.legend span { display: flex; align-items: center; gap: .25rem; }
.dot { width: 10px; height: 10px; border-radius: 3px; border: 1px solid; flex-shrink: 0; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-top: .4rem; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }

// Code not found

Notice that for small $k$ the tool finds a phantom path — a sequence of states that satisfies the property but ends with a violation — even though that path is not reachable from any real initial state. Raising $k$ forces the tool to check longer prefixes, eventually eliminating all phantom paths and closing the proof.

Under the hood, k-induction turns into two families of SAT/SMT queries that grow with $k$:

• Base check ($k$ steps from an initial state): unroll the transition relation $k$ times and ask whether the property can be violated. This is essentially bounded model checking — if a counterexample exists in $k$ or fewer steps, the solver finds it and the proof fails.
• Inductive step ($k$-step consecution): assume $k$ consecutive states all satisfy the property; ask whether the next state can violate it. If the answer is no, the property is $k$-inductive and the proof is complete.

The queries live in NP (satisfiability), so each check can in principle be expensive. Key facts:

• Every $k$-inductive property is also $(k+1)$-inductive, but not the other way around.
• For finite-state systems, if the property holds at all, there always exists a $k$ that closes the proof — so the method is complete in theory.
• In practice, finding the right $k$ can require exponentially many steps in the state-space diameter. Modern solvers pair k-induction with IC3/PDR (Bradley, 2011) to avoid this blowup.
• The technique generalizes beyond safety to liveness properties and inductive invariant synthesis, where the tool automatically strengthens the candidate property.

k-induction is not a classroom exercise — it runs inside the tools that prove real systems correct:

• Hardware model checking: every major chip vendor uses tools such as JasperGold and VC Formal that combine k-induction with IC3/PDR to verify that datapaths, arbiters and caches are free of assertion failures.
• Software verification: tools like CBMC and Kind2 unroll C or Lustre programs and apply k-induction to prove that array indices stay in bounds or that control loops satisfy their contracts.
• Protocol analysis: security and communication protocols are modeled as transition systems; k-induction proves that forbidden states (key leakage, deadlock) are unreachable.
• Autonomous systems: safety requirements for automotive and aviation software are verified against formal models, often using k-induction as the underlying engine.

The underlying pattern — "prove by looking back $k$ steps" — also appears in loop invariant generation, abstract interpretation, and the consecution queries inside IC3, making k-induction one of the load-bearing ideas in modern formal verification.

k-induction exposes a beautiful asymmetry at the heart of proof: a property can be true yet not provable by plain one-step induction, simply because the inductive hypothesis is not strong enough to exclude phantom states. Raising the depth $k$ strengthens the hypothesis until the phantom paths disappear — and the proof closes.

That is the lesson beyond the algorithm: truth and provability are not the same thing, and bridging the gap sometimes requires looking further back in time. The same insight drives IC3/PDR, abstract interpretation, and the whole enterprise of model checking — the quest to prove, not just test, that systems do what they claim.