leanbv: Verified SAT Tactic for Bitvector and Propositional Problems
leanbv
is supporting the development of a verified SATbased tactic
for bitvector and propositional problems.
Please see the LICENSE file for leanbv's licensing and CONTRIBUTING.md for external contribution guidelines.
Summary
Lean users will be able to prove propositional and bitvector goals by reduction to SAT, solving with local or cloudbased solvers, and reconstructing the proof in Lean. Automation is needed to allow Lean to scale to program verification problems. Existing tactics like leanauto allow Lean to appeal to SMT, but this trusts that the SMT solver is correct. Validating SMT proofs is a research area, but SAT proofs are well studied. Moreover, many program verification problems, like correctness of block ciphers and hashes, need no theories beyond bitvectors, and are well suited to automation through SAT.
leanbv
is a start at a tactic for Lean that can convert proof goals
into SAT problems, invoke a solver, and then soundly interpret SAT and
UNSAT results back into the Lean without a trusted assumption. Adding
this capability to Lean will enable other projects to apply SAT
solving to their goals.
LeanSatTactic Status
In LeanSatTactic
, we have successfully demonstrated the ability to
discharge propositional/Booelan goals in Lean4 via SAT by using the
Lean kernel to encode propositional problems into CNF and also replay
the LRAT proof steps via the
FromLRAT
library. However, we suspect that this method will not scale for the
kind of problems users care about. While improving the efficiency of
the Lean kernel to handle larger contexts and to process tactics is
certainly a possibility, this will require a large amount of effort on
development on Lean as a whole. Instead, we should focus our efforts
on developing a SAT tactic that appeals to individual utilities that
are proven correct and internalized via reflection.
In order to move away from the Lean kernel, we need to create the following tools that have associated proofs of correctness and reflection into Lean. Note that these tasks can be developed in parallel depending on interest and support. We will prioritize developing a solution as quickly as possible, and then iterating on that design to improve soundness and performance.
 Verified Encoding to CNF for Propositional Logic and Bitvectors
 We will initially develop an unverified encoding via conversion to AIG (AndInverter Graphs) and then to CNF.
 Once this is completed, we can begin to prove soundness of our implementation
 Verified LRAT Proof Checker. See Josh Clune's
leansat.
 Further develop LeanSAT (verified LRAT proof checker) into a standalone tactic that is capable of adding a negated CNF formula to the local context based on the formula and proof given to the checker.
There are several opportunities for collaboration with academic groups and the Lean community. We will use Zulip to coordinate our efforts.
Prerequisites

Install CaDiCaL, and make sure that it is in your path.

Install Lean4 and your preferred editor's plugin on your machine by following these instructions.
Build Instructions
Run lake build
at the toplevel of leanbv.
Directory Overview
LeanSatTactic
: Demonstration of verified Lean SAT tactic using Lean kernel.