Whiel: A Neurosymbolic Platform for Certified Relational Program Verification
Jesse Comer, Fangzhu Shen, Shuo Zhang, Mayur Naik, Sudeepa Roy, Val Tannen
cs.DB
Nov 3, 2026 · v1
cs.AI cs.LO
TL;DR
Builds a Lean library formalizing relational programs and Hoare logic soundness, and certifies LLM-found invariants and counterexamples as kernel-checked Lean proofs.
Abstract
We present the Whiel (a contraction of Whi(le-R)el) system for Lean-certified reasoning about imperative relational programs. The system can encode containment and equivalence problems for Datalog, its extensions with negation, and the core fragment of graph query languages. It can also represent optimized or incremental evaluation algorithms that are not expressible in the original query language, as well as first-order specifications of integrity constraints, schema mappings, and views arising in data integration, exchange, and sharing. Whiel's program states are database instances, and its imperative structure enables compositional Hoare-style reasoning with first-order relational specifications, using prophecy variables and leveled invariants to support inductive arguments. Whiel supports neurosymbolic discovery of loop invariants whose verification conditions can be checked using the Vampire first-order theorem prover. Counterexamples are fed back into the neurosymbolic pipeline, while proposed solutions are translated into Lean proof certificates. To validate the Whiel system, we evaluate its performance on a curated benchmark suite. In summary, we envision the Whiel system as a tool for tackling mathematically demanding, typically undecidable problems involving complex query and constraint languages, with a high degree of trust in its output.
Problem
Database problems such as Datalog query equivalence, containment, evaluation strategies and incremental view maintenance are often undecidable. LLM-proposed solutions to them need correctness guarantees that testing or manual review cannot give.
Approach
Whiel encodes these problems as Hoare triples over imperative relational programs whose states are database instances. An LLM proposer (AgentHoudini) suggests invariant clauses or counterexamples. A LeveledHoudini verifier uses Vampire and prophecy variables to check them and returns feedback. A Lean library formalizes relational algebra, Whiel semantics, Hoare logic soundness, wlp computation, and equivalidity of single-loop preprocessing. Valid results are certified by reconstructing Vampire proofs via VampLean, and invalid results by a Lean-implemented interpreter and model checker, so only the Lean kernel needs to be trusted.
Results
The benchmark contains 86 curated tasks (69 valid, 17 invalid). Two baselines solve fewer tasks: DirectLean, where the LLM writes Lean proofs directly, solves 20, and a non-iterating one-round variant solves 46. The full iterative Whiel pipeline is reported to outperform both, and certification is an optional step with measured overhead.
