H-Houdini: Scalable Invariant Learning

Proving that a chip is free of a whole class of security flaw means finding an inductive invariant, and the machine-learning-style method for learning one asks a solver a single giant question about the entire design at once — which is hopeless for a modern out-of-order processor; this paper from UC Berkeley shows how to break that one giant question into a hierarchy of tiny local questions that can be answered in parallel and stitched back into a correct proof, learning an invariant for a RISC-V core in under 10 seconds instead of 8 hours, and scaling to the out-of-order BOOM core that no prior tool could handle.

Why this problem is worth solving

The object every verifier is chasing is a specific mathematical thing, and understanding it explains why the search is so hard.

The particular property this work proves is one the security community cares about deeply.

What people did before, and where it broke

• Write the invariant by hand. An expert studies the design and crafts an invariant, then a solver checks it, as one prior tool did for a mid-sized BOOM. Where it broke. It takes deep expertise and enormous manual effort per design, and it does not generalize — every new chip or property is a fresh hand-crafting job.
• Learn it with machine-learning-inspired synthesis (Houdini). Let experts throw in all candidate facts and have an algorithm search for a self-sustaining subset, checking candidates with a solver. Where it broke. It treats the design as a black box, so each check is one monolithic query over all the candidate facts at once, made in the innermost loop — prohibitively expensive on a large design.
• Make the learner property-directed (Sorcar, ConjunCT). Improve the black-box learner by keeping the target property in view throughout to prune the search harder. Where it broke. The queries are still monolithic and structure-blind, so it helped but did not change the fundamental cost; the resulting tool took eight hours on an in-order core and could not run on an out-of-order one.
• Use white-box SAT-based methods (IC3, PDR). Open the design up and exploit its structure to make cheap, incremental checks that eliminate bad states one relative step at a time. Where it broke. These give cheap queries but lose the machine-learning method’s conveniences — the kitchen-sink freedom to add any predicate, the search-shrinking predicate abstraction, and the bootstrapping from positive examples.
• The gap. One camp had the convenient, search-shrinking learning framework but paid for it with one giant structure-blind query; the other camp had cheap structure-aware queries but lacked the learning conveniences. No method combined the shrinking of the search space from the first with the cheap incremental checks of the second — which is exactly what a large out-of-order core needs.

How H-Houdini works

The idea

Keep the black-box learner’s conveniences but open the box to make the checks cheap. The two families of invariant methods each had half of what was needed. The machine-learning-inspired learners were pleasant to use — you could throw in any candidate fact without fear, a predicate abstraction kept the search space bounded, and examples of states the invariant must allow pruned it further — but because they ignored the design’s structure, every check was one enormous query over all the facts at once, and that query does not scale. The white-box solvers, by contrast, exploited structure to ask cheap incremental questions but gave up all those conveniences. H-Houdini refuses to choose. It keeps the learner’s search-shrinking machinery — the kitchen-sink predicates, the abstraction, the positive examples — and layers on top the white-box move of asking cheap, structure-aware checks instead of one monolithic one. Taking a search that a black-box method runs blindly and expensively and making it interrogate the problem’s own structure to go dramatically faster is the same reframing the explainable design-space work covered elsewhere on this site performs, replacing an opaque optimizer that only sees a score with one that reasons about why a design costs what it does and acts on it.

Decompose the one giant proof into local pieces that compose correct-by-construction. The heart of the method is a way to never ask the giant question at all. To prove a target fact holds, H-Houdini asks only a local question: what conditions on the state elements that directly feed this fact would force it to hold on the next step? Those conditions become new facts to establish, and the same local question is asked of each, so the reasoning spreads outward through the circuit’s wiring rather than confronting the whole design at once. Each of these local checks is small and cheap, involving only a handful of neighboring state elements. And crucially, when every local piece has been proven, a mathematical argument guarantees that their combination is a valid inductive invariant for the whole design — the pieces compose into the monolithic invariant correctly by construction, so the expensive whole-design check is simply never performed. Cutting one intractable global check into a hierarchy of small local checks whose answers reassemble into the global guarantee is the same divide-and-conquer discipline the on-chip-memory-allocation work covered elsewhere on this site relies on, breaking a hard combinatorial problem into pieces small enough for a solver to dispatch and recombining them into a whole solution.

The structure that makes the checks local also makes them parallel, reusable, and prunable. Opening the black box does more than shrink each query — it hands over three further gifts that come directly from the circuit’s shape. Because the outward recursion branches at every fan-in, the independent branches have no dependence on one another and can be explored on separate cores at once, so the work spreads across a cluster. Because different targets often share the same upstream logic, their fan-in cones overlap, and the shared region need only be analyzed a single time and its result reused everywhere it appears — a proven fact is never re-proven. And because the learner still carries positive examples, any candidate fact that contradicts a state the invariant must allow is thrown out before a solver ever sees it. Together these turn a design of over a hundred thousand state bits from hopeless into a job of minutes. Exploiting the overlap in a structured problem so that shared sub-work is computed once and reused rather than repeated is the same move the graph-neural-network training work covered elsewhere on this site makes when it reuses the nodes that neighboring subgraphs share instead of re-fetching them.

Following the reasoning through H-Houdini

The output being 1 is the property; the whole point is to prove it self-sustaining without ever checking the full design in one shot.

Why it works

• Local abducts make each query cheap instead of prohibitive. A black-box check spans every candidate fact over the whole design → but asking only what the target’s immediate fan-in must satisfy touches a handful of facts → so each solver query collapses from the monolithic one no tool could run to a small local one, the barrier that blocked out-of-order cores.
• Composition-by-construction skips the whole-design check entirely. Proving a giant invariant directly is the query that does not scale → but a mathematical argument guarantees the proven local pieces combine into a valid whole → so the expensive monolithic check is never asked, only its many small parts.
• Keeping the learning conveniences shrinks how many pieces there are. Structure alone does not bound the search → but retaining the predicate abstraction and positive examples pre-filters candidates to plausible ones → so far fewer local abducts must be synthesized, preserving the kitchen-sink ease without its cost.
• Independent fan-in branches run in parallel. The outward recursion branches at every input with no cross-dependence → so separate branches execute on separate cores at once → which is why doubling the core count roughly halves the time until saturation, and Rocketchip finishes in seconds.
• Overlapping cones are analyzed once, not repeatedly. Different targets in a real design share upstream logic → but memoizing a solved fact and reusing it wherever its cone reappears avoids re-proving → which is what turns a hundred-thousand-bit design from intractable into a job of minutes.

What it costs (trade-offs and scope)

• It is mostly, not fully, push-button on out-of-order cores. Rocketchip needs no expert annotations, but BOOM requires modest ones — extra predicates for its micro-op decoding and a cleaning step to keep the positive examples valid. A graduate student unfamiliar with BOOM needed about two days to produce and generalize them, so the fully automatic ideal holds only for the simpler in-order core.
• Soundness leans on the abstraction and examples being good enough. The guarantees are proof-sketched and rest on premises that must hold — chiefly that the positive examples are non-contradictory and cover the invariant; when they are not exhaustive, the search backtracks, and an inadequate predicate abstraction could miss an invariant that exists.
• The headline speedup is against the authors’ own prior tool. The 2880-times figure is Rocketchip versus ConjunCT, an earlier tool from the same group, and the BOOM result is really “we can, they could not,” since ConjunCT simply cannot run BOOM at all — an important capability jump, but not a like-for-like speed ratio there.
• BOOM is still slow in absolute terms, and scaling is steep. The largest variant takes up to 199 minutes, with a heavy tail — a single subtask ran over two and a half hours — and the analysis time grows with roughly the cube of the design size, so still-larger designs will strain it despite the parallelism.
• Much of the runtime is implementation overhead. About half the time is spent outside the solver, in the Python framework, so the reported numbers carry engineering slack rather than being a floor on what the algorithm requires.
• Only one application is demonstrated. H-Houdini is presented as a general invariant learner, but the sole instance shown is VeloCT for a single security property, constant-time safety; its breadth across other properties and designs is argued, not evidenced.
• It needs white-box access and a specific pipeline. The design must be flattened, turned into a product circuit with assertions, and emitted in a solver-friendly format, and caches are excluded on the assumption that memory instructions are already unsafe — so the setup is real preprocessing, not a drop-in on arbitrary RTL.
• Results are configuration-specific. Whether the multiply family is safe flipped between chips and even between instruction-set widths, and the one genuine bug it surfaced is a valuable but single anecdote — reminders that the answers depend closely on the exact design analyzed.

The evaluation

Check yourself

Sources

The paper is “H-Houdini: Scalable Invariant Learning” by Sushant Dinesh, Yongye Zhu, and Christopher W. Fletcher, published at ASPLOS 2025, pages 603-618, DOI 10.1145/3669940.3707263. The authors are at the University of California, Berkeley.

This explainer is written from the full 16-page text. Everything above comes from the paper’s own sections: the introduction contrasting machine-learning-inspired invariant synthesis (Houdini, Sorcar) with white-box SAT-based approaches (IC3, PDR) and stating the goal of blending them; the background formalizing transition systems, inductive invariants, relative inductivity, abducts, and the Houdini algorithm with its monolithic query cost; the H-Houdini section presenting the abductive decomposition, the recursion over the cone of influence as a memoizable and parallelizable wavefront, the soundness argument via chained relative-inductive queries and the positive-example premise, and the algorithm with its slicing, mining, and abduct oracles; the VeloCT sections instantiating H-Houdini for the safe-instruction-set problem with the definitions of traces, trace indistinguishability, equal-modulo-secret states, and safe sets; and the evaluation on Rocketchip and the four BOOM variants, reporting the under-10-second Rocketchip result and 2880-times speedup over ConjunCT, the 6.95-to-199.1-minute BOOM results with their expert-annotation requirements, the parallel scaling and cubic growth in design size, the linear growth of per-query SMT time with long tails, the backtracking frequency, and the security results matching prior work including the multiply-family differences by ISA width and the discovery that the auipc instruction has variable timing on BOOM.