Horn-Clause Verification

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 $B_1 \wedge B_2 \wedge \cdots \wedge B_k \Rightarrow H$, where each $B_i$ is a constraint and $H$ 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.

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.

<!-- {{c_html_intro}} -->
<div class="panel">
  <div class="section-label">{{label_program}}</div>
  <pre class="code-block" id="program-code"></pre>
</div>
<div class="panel">
  <div class="section-label">{{label_clauses}}</div>
  <div id="clause-list" class="clause-list"></div>
</div>
<div class="panel">
  <div class="section-label">{{label_derivation}}</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">{{btn_step}}</button>
  <button id="btn-run" type="button">{{btn_run}}</button>
  <button id="btn-reset" type="button" class="ghost">{{btn_reset}}</button>
</div>

/* {{c_css_intro}} */
* { 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; }

// Code not found

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.

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 $k$ 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.

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.

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.