Foundational Constraint Solving for Expressive Refinement Typing

• URL: http://arxiv.org/abs/2607.12226v1
• Date: Tue, 14 Jul 2026 00:15:23 GMT
• Title: Foundational Constraint Solving for Expressive Refinement Typing
• Abstract summary: We present FLEX, a Constrained Horn Clause (CHC) solver implemented in LEAN.<n>We show how FLEX reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code.
• Score: 0.9624643581968987
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Evidence-Driven LLM Agent for C-to-Synthesizable-C Conversion and Verification [3.285367305212235]
  C programs fail to complete the four-stage pipeline of a high-level synthesis (HLS) toolchain.<n>We formulate C-to-HLS-C conversion as a closed-loop generation-verification-diagnosis-repair problem on an HLS tool.
  arXiv  Detail & Related papers  (2026-06-25T02:55:02Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
  We introduce TorchLean, a framework that treats learned models as first-class mathematical objects with a single, precise semantics shared by execution and verification.<n>We validate TorchLean end-to-end on certified robustness, physics-informed residual bounds for PINNs, and Lyapunov-style neural controller verification.
  arXiv  Detail & Related papers  (2026-02-26T05:11:44Z)
• Plug-and-Play Benchmarking of Reinforcement Learning Algorithms for Large-Scale Flow Control [61.155940786140455]
  Reinforcement learning (RL) has shown promising results in active flow control (AFC)<n>Current AFC benchmarks rely on external computational fluid dynamics (CFD) solvers, are not fully differentiable, and provide limited 3D and multi-agent support.<n>We introduce FluidGym, the first standalone, fully differentiable benchmark suite for RL in AFC.
  arXiv  Detail & Related papers  (2026-01-21T14:13:44Z)
• CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses [0.0]
  Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for verification tasks.<n>This paper introduces a portfolio-based CHC solver that adopts a software verification approach for solving CHCs.
  arXiv  Detail & Related papers  (2025-10-30T12:25:06Z)
• ImCoref-CeS: An Improved Lightweight Pipeline for Coreference Resolution with LLM-based Checker-Splitter Refinement [45.01372641622595]
  We present ImCoref-CeS, a novel framework that integrates an enhanced supervised model with Large Language Models (LLMs)-based reasoning.<n>First, we present an improved CR method (textbfImCoref) to push the performance boundaries of the supervised neural method.<n>We employ an LLM acting as a multi-role Checker-Splitter agent to validate candidate mentions and coreference results.
  arXiv  Detail & Related papers  (2025-10-11T14:48:08Z)
• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  We propose an unsupervised conformal inference framework for generation.<n>Our gates achieve close-to-nominal coverage and provide tighter, more stable thresholds than split UCP.<n>The result is a label-free, API-compatible gate for test-time filtering.
  arXiv  Detail & Related papers  (2025-09-26T23:40:47Z)
• HALT-RAG: A Task-Adaptable Framework for Hallucination Detection with Calibrated NLI Ensembles and Abstention [0.0]
  HALT-RAG is a post-hoc verification system designed to identify hallucinations in the outputs of Retrieval-Augmented Generation pipelines.<n>Our flexible and task-adaptable framework uses a universal feature set derived from an ensemble of two frozen, off-the-shelf Natural Language Inference (NLI) models and lightweight lexical signals.<n>By pairing our universal feature set with a lightweight, task-adapted and a precision-constrained decision policy, HALT-RAG achieves strong OOF F1-scores of 0.7756, 0.9786, and 0.7391 on the summarization, QA, and dialogue
  arXiv  Detail & Related papers  (2025-09-09T07:58:46Z)
• Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning [7.574481956683386]
  This work presents Proof2Silicon, a novel end-to-end synthesis framework.<n>It embeds the previously proposed PREFACE flow to enable the generation of correctness-by-construction hardware directly from natural language specifications.
  arXiv  Detail & Related papers  (2025-09-07T23:04:15Z)
• Rectified Diffusion Guidance for Conditional Generation [94.83538269086613]
  We revisit the theory behind CFG and rigorously confirm that the improper combination coefficients (textiti.e.) brings about expectation shift the generative distribution.<n>We show that our approach enjoys a textbftextitform solution given the strength.<n> Empirical evidence on real-world data demonstrate the compatibility of our design with existing state-of-the-art diffusion models.
  arXiv  Detail & Related papers  (2024-10-24T13:41:32Z)
• General Cutting Planes for Bound-Propagation-Based Neural Network Verification [144.7290035694459]
  We generalize the bound propagation procedure to allow the addition of arbitrary cutting plane constraints. We find that MIP solvers can generate high-quality cutting planes for strengthening bound-propagation-based verifiers. Our method is the first verifier that can completely solve the oval20 benchmark and verify twice as many instances on the oval21 benchmark.
  arXiv  Detail & Related papers  (2022-08-11T10:31:28Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.