A Natively Parallel Proof Framework for Clause-Sharing SAT Solving

Foundational Constraint Solving for Expressive Refinement Typing

FLEX is presented, 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.

Formally Verified Certification of Constraint Programming Proofs

This work presents a formal definition of DRCP, a proof system for CP over integer domains that captures core solver operations, including conflict analysis and heterogeneous propagation, by modular inference rules with precise semantics and develops FznDrcpCheck, a formally verified proof checker in Rocq that validates DRCP proofs directly against FlatZinc models.

LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean

This work introduces a framework that addresses both verification levels in the Lean theorem prover, and can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints, parametrically for entire problem families.

Spain: Succinct proofs for numerical computations

Trimming Pseudo-Boolean Proofs

CaDiCaL 3.0

This system description reports on how Kissat’s award-winning techniques were adapted to the full-featured incremental SAT solver CaDiCaL, including clausal congruence closure, clausal equivalence sweeping, and bounded variable addition, to support efficient linear proof production with hints.