Search papers, labs, and topics across Lattice.
This paper introduces FLEX, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, addressing the limitations of SMT-based program verifiers in terms of expressiveness and trust. By encoding CHCs as LEAN propositions and implementing verified CHC generators, FLEX enables the use of LEAN's proof ecosystem to verify low-level systems code effectively. The results show that FLEX can automatically discharge 95.7% of the CHCs from the FLUX benchmark suite, significantly enhancing the reliability of CHC-based verification tools.
FLEX achieves a remarkable 95.7% success rate in automatically discharging CHCs, redefining trust in program verification.
SMT-based program verifiers are hamstrung by two problems: expressiveness, because predictable verification restricts to the boundaries of SMT decidability, and trust, because the solver is a large, unverified artifact whose soundness bugs may quietly compromise every tool built on it. We present FLEX, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions. First, FLEX encodes CHCs as plain LEAN propositions where the Horn variables are existentially bound predicates, and shows how to implement CHC solvers as tactics (meta-programs) that compute kernel checkable proofs of the CHC propositions. Second, we show how to implement two verified CHC generators in LEAN: a Floyd-Hoare style generator for an imperative language, and a refinement-type-based generator for a functional calculus, which can be composed with the solving tactics to yield the first end-to-end foundational CHC-based verifiers. Finally, we show how FLEX allows us to leapfrog the expressiveness limitations of SMT by unleashing LEAN's entire ecosystem of proof machinery to prove arbitrary functional correctness properties of various low-level Rust libraries using the FLUX refinement type checker, and demonstrate the viability of FLEX as a trustworthy CHC backend, by showing it automatically discharges 95.7% of the CHCs from FLUX's benchmark suite.
