Introduction

You learned mathematical induction in school: prove a base case, then prove that if it holds for nn it holds for n+1n+1, and you have it for all nn. 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 kk consecutive states that all satisfy the property must continue satisfying it in step k+1k+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.

Try It

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

<!-- k-induction demo — counter mod 4, threshold T, property s < T -->
<div class="panel">
  <div class="row-label">
    <label for="kSlider">Induction depth k = <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">Safety threshold T = <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">Run k-induction</button>
  <button id="btnReset" type="button" class="ghost">Reset</button>
</div>

/* state colours — init=blue, ok=green, phantom=orange, bad=red */
* { 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; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Model: counter starts at 0 and increments mod WRAP (wraps 3->0).
// Safety property P(s) = (s < T). Property is TRUE: max reachable = WRAP-1 < T.
// Plain 1-step induction fails: step-check finds phantom window [T-1, T]
// even though T-1 is unreachable (counter wraps before reaching T).

const WRAP = 4;
const kSlider   = document.getElementById('kSlider');
const tSlider   = document.getElementById('threshSlider');
const kVal      = document.getElementById('kVal');
const tVal      = document.getElementById('tVal');
const traceEl   = document.getElementById('trace');
const statusEl  = document.getElementById('status');

// real transition — wrapping increment
function nextReal(s) { return (s + 1) % WRAP; }

// safety property — counter must stay strictly below threshold T
function prop(s, T) { return s < T; }

// Base check — follow the real (mod WRAP) trajectory from state 0
// for k steps; if the property breaks, it is a REAL counterexample.
function baseCheck(k, T) {
  const path = [];
  let s = 0;
  for (let i = 0; i <= k; i++) {
    path.push(s);
    if (!prop(s, T)) return { ok: false, path };
    s = nextReal(s);
  }
  return { ok: true, path };
}

// Step (consecution) check — search over unbounded integer windows.
// A SAT solver has no reachability info, so it may find a phantom window
// of k states satisfying P whose next state violates P.
function stepCheck(k, T) {
  // search all starting integers up to T+k
  for (let start = 0; start <= T + k; start++) {
    const window = [];
    let allP = true;
    let s = start;
    for (let i = 0; i < k; i++) {
      if (!prop(s, T)) { allP = false; break; }
      window.push(s);
      s = s + 1; // phantom step — unbounded integer, ignores the modulo wrap
    }
    if (!allP) continue;
    if (!prop(s, T)) {
      window.push(s);
      return { ok: false, phantom: window };
    }
  }
  return { ok: true };
}

function run() {
  const k = parseInt(kSlider.value);
  const T = parseInt(tSlider.value);
  traceEl.innerHTML = '';
  statusEl.className = 'status';

  const base = baseCheck(k, T);
  const step = stepCheck(k, T);

  if (!base.ok) {
    renderPath(base.path, T, false);
    statusEl.textContent = i18nFmt('✗ Real counterexample: property violated within %k% real steps.', { k });
    statusEl.className = 'status fail';
    return;
  }
  if (!step.ok) {
    renderPath(step.phantom, T, true);
    statusEl.textContent = i18nFmt('⚠ Phantom path at k=%k%: step fails — raise k to eliminate.', { k });
    statusEl.className = 'status phantom-msg';
    return;
  }
  renderProof(k, T);
  statusEl.textContent = i18nFmt('✓ Proof closed at k=%k%: property is k-inductive — always safe!', { k });
  statusEl.className = 'status pass';
}

function renderPath(path, T, isPhantom) {
  path.forEach((s, i) => {
    if (i > 0) addArrow();
    let cls;
    if (isPhantom) {
      cls = i < path.length - 1 ? 'phantom' : 'bad';
    } else {
      cls = prop(s, T) ? (i === 0 ? 'init' : 'ok') : 'bad';
    }
    addState(s, cls);
  });
  if (isPhantom) {
    const leg = document.createElement('div');
    leg.className = 'legend';
    leg.innerHTML =
      '<span><span class="dot" style="background:#fff3e0;border-color:#ffa726"></span>phantom states (satisfy P but unreachable)</span>' +
      '<span><span class="dot" style="background:#ffebee;border-color:#ef5350"></span>violation state</span>';
    traceEl.appendChild(leg);
  }
}

function renderProof(k, T) {
  for (let i = 0; i <= k && i <= WRAP; i++) {
    if (i > 0) addArrow();
    addState(i % WRAP, i === 0 ? 'init' : 'ok');
  }
}

function addState(val, cls) {
  const d = document.createElement('div');
  d.className = 'state ' + cls;
  d.textContent = val;
  traceEl.appendChild(d);
}
function addArrow() {
  const d = document.createElement('span');
  d.className = 'arrow';
  d.textContent = '→';
  traceEl.appendChild(d);
}

kSlider.addEventListener('input', () => { kVal.textContent = kSlider.value; });
tSlider.addEventListener('input', () => { tVal.textContent = tSlider.value; });
document.getElementById('btnRun').addEventListener('click', run);
document.getElementById('btnReset').addEventListener('click', () => {
  kSlider.value = 1; kVal.textContent = '1';
  tSlider.value = 5; tVal.textContent = '5';
  traceEl.innerHTML = ''; statusEl.textContent = ''; statusEl.className = 'status';
});
run();
Result
Console

Notice that for small kk 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 kk forces the tool to check longer prefixes, eventually eliminating all phantom paths and closing the proof.

The Real Complexity

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

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

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

  • Every kk-inductive property is also (k+1)(k+1)-inductive, but not the other way around.
  • For finite-state systems, if the property holds at all, there always exists a kk that closes the proof — so the method is complete in theory.
  • In practice, finding the right kk 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.

Where It Matters

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 kk 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.

Conclusion

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 kk 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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/k-induction/Content licensed under CC BY-NC 4.0.