Introduction

Every time a developer writes a loop, they are implicitly claiming something: no matter how many times this runs, such-and-such property always holds. That hidden claim is called a loop invariant, and finding one that is both true and strong enough to prove the program correct is the crux of automated verification.

One of the most elegant approaches encodes the whole problem as a set of constrained Horn clauses (CHCs) — logical implications of the form B1∧B2∧⋯∧Bk⇒HB_1 \wedge B_2 \wedge \cdots \wedge B_k \Rightarrow H, where each BiB_i is a constraint and HH is either another predicate or false. The program becomes a handful of such clauses, and a CHC solver finds — or proves the non-existence of — a model: an assignment of predicates that makes every clause true.

If a model exists it hands you the invariants for free. If it does not, the solver produces a counterexample trace that shows exactly how the program breaks its specification. Either way, you get a definitive answer without guessing.

Find the Invariant

The demo below encodes a simple counting loop as Horn clauses and runs a forward-chaining solver that derives the strongest reachable fact at each step.

<!-- Horn-clause verification demo layout -->
<div class="panel">
  <div class="section-label">Program</div>
  <pre class="code-block" id="program-code"></pre>
</div>
<div class="panel">
  <div class="section-label">Horn Clauses</div>
  <div id="clause-list" class="clause-list"></div>
</div>
<div class="panel">
  <div class="section-label">Derived Facts (Invariant)</div>
  <div id="deriv-table" class="deriv-table"></div>
</div>
<div class="status" id="status"></div>
<div class="btns">
  <button id="btn-step" type="button">Step</button>
  <button id="btn-run" type="button">Run all steps</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>

/* Styles for the Horn-clause verification demo */
* { box-sizing: border-box; margin: 0; padding: 0; }
body { font-family: system-ui, sans-serif; font-size: 14px; color: #222; padding: 4px; }
.panel { margin-bottom: 8px; }
.section-label { font-size: 11px; font-weight: 700; text-transform: uppercase;
  letter-spacing: .06em; color: #5a7088; margin-bottom: 4px; }
.code-block { background: #f4f6f8; border: 1px solid #d0d7de; border-radius: 6px;
  padding: 8px 10px; font-size: 12px; line-height: 1.6; white-space: pre; overflow-x: auto; }
.clause-list { display: flex; flex-direction: column; gap: 4px; }
.clause { font-family: ui-monospace, monospace; font-size: 12px; padding: 5px 8px;
  border-radius: 5px; border: 1px solid #d0d7de; background: #f9fbfc; }
.clause .lbl { font-weight: 700; color: #1d3557; margin-right: 6px; }
.clause.fired { background: #e6f4ea; border-color: #7dc99e; }
.deriv-table { display: flex; flex-direction: column; gap: 3px; max-height: 140px; overflow-y: auto; }
.deriv-row { display: flex; gap: 8px; align-items: baseline; font-size: 12px;
  padding: 3px 6px; border-radius: 4px; }
.deriv-row.new { background: #e8f0fe; animation: fadein .35s; }
.deriv-row .step-num { font-weight: 700; color: #5a7088; min-width: 22px; }
.deriv-row .fact { font-family: ui-monospace, monospace; }
.deriv-row .source { color: #888; font-size: 11px; }
@keyframes fadein { from { opacity:0; transform: translateY(-4px); } to { opacity:1; transform:none; } }
.status { font-size: 13px; font-weight: 600; min-height: 1.4em; margin: 6px 0; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
.status.info { color: #1d3557; }
.btns { display: flex; gap: 6px; flex-wrap: wrap; }
button { font: 600 13px system-ui; padding: .4rem .8rem; border: 1px solid #1d3557;
  background: #1d3557; color: #fff; border-radius: 7px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .45; cursor: default; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
/* The program being verified — a simple counting loop from 0 to N */
const PROGRAM_TEXT = [
  'int x = 0, n = 5;',
  'while (x < n) {',
  '  x = x + 1;',
  '}',
  '// assertion: x == n'
].join('\n');
/* Horn clauses encoding the loop: init, body transition, query (post-condition) */
/* init: the invariant holds before the loop (x=0 is reachable) */
/* body: if Inv(x) and x<N then Inv(x+1) (the loop step preserves the invariant) */
/* query: if Inv(x) and x>=N then x=N (the post-condition) */
const CLAUSES = [
  { id: 'init',  label: 'init',  text: 'Inv(0)',       rule: null },
  { id: 'body',  label: 'body',  text: 'Inv(x) ∧ x<5 ⇒ Inv(x+1)', rule: 'body' },
  { id: 'query', label: 'query', text: 'Inv(x) ∧ x≥5 ⇒ x=5', rule: 'query' }
];
/* Forward-chaining solver state */
let derived = [];
let stepIndex = 0;
let done = false;
const N = 5;
/* Pre-compute all derivation steps from init through N body firings */
function computeAllSteps() {
  const steps = [];
  steps.push({ val: 0, clause: 'init', stepNum: 0 });
  for (let x = 0; x < N; x++) {
    steps.push({ val: x + 1, clause: 'body', stepNum: x + 1 });
  }
  return steps;
}
const ALL_STEPS = computeAllSteps();
function renderProgram() {
  document.getElementById('program-code').textContent = PROGRAM_TEXT;
}
function renderClauses(firedId) {
  const el = document.getElementById('clause-list');
  el.innerHTML = '';
  for (const c of CLAUSES) {
    const d = document.createElement('div');
    d.className = 'clause' + (firedId === c.id ? ' fired' : '');
    d.innerHTML = '<span class="lbl">[' + c.label + ']</span>' + c.text;
    el.appendChild(d);
  }
}
function renderDeriv() {
  const el = document.getElementById('deriv-table');
  el.innerHTML = '';
  for (let i = 0; i < derived.length; i++) {
    const r = document.createElement('div');
    r.className = 'deriv-row' + (i === derived.length - 1 ? ' new' : '');
    const { val, clause } = derived[i];
    r.innerHTML =
      '<span class="step-num">' + i + '</span>' +
      '<span class="fact">Inv(' + val + ')</span>' +
      '<span class="source">← [' + clause + ']</span>';
    el.appendChild(r);
  }
  el.scrollTop = el.scrollHeight;
}
function setStatus(msg, cls) {
  const el = document.getElementById('status');
  el.textContent = msg;
  el.className = 'status ' + (cls || '');
}
function applyStep() {
  if (done) return false;
  if (stepIndex < ALL_STEPS.length) {
    derived.push(ALL_STEPS[stepIndex]);
    stepIndex++;
    return true;
  }
  return false;
}
function checkQuery() {
  /* Check that the last derived fact satisfies the query clause */
  const last = derived[derived.length - 1];
  if (last && last.val === N) {
    return true;
  }
  return false;
}
function updateButtons() {
  document.getElementById('btn-step').disabled = done;
  document.getElementById('btn-run').disabled = done;
}
function step() {
  if (done) return;
  const progressed = applyStep();
  const lastStep = ALL_STEPS[stepIndex - 1];
  renderClauses(lastStep ? lastStep.clause : null);
  renderDeriv();
  if (!progressed || stepIndex >= ALL_STEPS.length) {
    /* Fixpoint reached — check the query clause */
    const valid = checkQuery();
    done = true;
    updateButtons();
    if (valid) {
      setStatus(i18nFmt('Proved: after %n% iterations the invariant guarantees x = %n%.', { n: N }), 'ok');
    } else {
      setStatus('Query clause not satisfied — verification failed.', 'bad');
    }
    renderClauses('query');
  } else {
    setStatus(i18nFmt('Derived: Inv(%x%) via [body].', { x: lastStep.val }), 'info');
  }
}
function runAll() {
  if (done) return;
  while (!done) { step(); }
}
function reset() {
  derived = [];
  stepIndex = 0;
  done = false;
  renderProgram();
  renderClauses(null);
  renderDeriv();
  setStatus('Press Step or Run to watch the solver derive the loop invariant.', 'info');
  updateButtons();
}
document.getElementById('btn-step').addEventListener('click', step);
document.getElementById('btn-run').addEventListener('click', runAll);
document.getElementById('btn-reset').addEventListener('click', reset);
reset();
Result
Console

The solver starts from the init clause (what is true before the loop), repeatedly fires the body clause (what the loop does), and finally checks the query clause (does the post-condition hold?). Each row you see is a derived fact — together they form the loop invariant discovered automatically by the solver.

The Real Complexity

Horn clauses look deceptively simple. Their complexity, however, spans a wide range depending on the fragment:

  • Propositional Horn-SAT is P-complete (linear time via unit propagation). This is the tractable island inside the NP-hard world of general SAT.
  • Constrained Horn clauses over linear arithmetic (CHC-LIA) remain decidable. Solvers such as Z3's Spacer and Eldarica handle these by constructing an inductive interpolant — essentially guessing a candidate invariant and verifying it iteratively.
  • Nonlinear CHC — where the head and body share nested predicate calls — is undecidable in general. This is the regime reached by programs with recursive procedures and unbounded data structures.
  • The CHC-solving algorithm most used in industry is PDR/IC3 (Property Directed Reachability, Bradley 2011), originally invented for hardware model checking. It builds a proof certificate layer by layer: each layer is a formula that over-approximates the states reachable in kk steps, and the loop terminates when two consecutive layers converge. Convergence is guaranteed for finite systems; for software it is a heuristic but works well in practice.

The beauty is that the encoding is compositional: every function call becomes its own predicate, every loop becomes a fixed-point equation, and the solver threads them all together. When it succeeds, the model it returns is the invariant — not just a yes/no answer, but a proof.

Where It Matters

Constrained Horn clauses are the common language spoken by most modern verification back-ends:

  • Smart-contract auditing: tools such as Certora Prover and Solidity's formal-verification mode translate EVM bytecode into CHCs and ask a solver whether a safety property can ever be violated — catching reentrancy and overflow bugs before deployment.
  • Operating-system kernels: seL4's verification toolchain encodes the kernel's C source as CHCs and has machine-checked every one of the 10,000 lines of the microkernel since 2009.
  • Hardware model checking: the algorithm PDR/IC3 was born in this domain and is now the default engine in commercial tools from Cadence and Synopsys.
  • Compiler verification: LLVM's bounded model checker and Infer (Meta's static analyser) reduce their checks to CHC queries before shipping to a solver.
  • Abstract interpretation: the classic Cousot–Cousot framework (1977) for computing program invariants is, in modern terms, a specific strategy for solving CHCs — widening operators correspond to heuristics that force convergence when the exact fixed point would take infinitely many steps.

Understanding Horn-clause verification is understanding the logical spine of program equivalence checking, abstract interpretation, and every tool that claims to prove software correct rather than merely test it.

Conclusion

A loop invariant is a claim about infinity — that no matter how many iterations run, a certain fact stays true. Constrained Horn clauses make that claim precise enough for a machine to check, and modern CHC solvers can discover the invariant from scratch, without any hint from the programmer.

The tractable fragment (linear, propositional) is solvable in polynomial time, a rare gift inside the landscape of P vs NP. The harder fragments push into undecidability, but practical heuristics — especially PDR/IC3 — tame most real programs. What emerges is not just a yes or no, but a proof: a mathematical certificate that the loop does what it promises, every single time.

Share this article

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

Comments

Loading comments...

https://www.kipuhub.com/en/article/horn-clause-verification/Content licensed under CC BY-NC 4.0.