lrat_isa is a checker for unsatisfiability certificates in the LRUP format, formally verified in Isabelle/HOL. It is implemented time and memory efficiently, and can be run in parallel to the SAT solver at low overhead.

Here are some benchmark plots or the raw data.

The verification is done wrt. a grammar of the DIMACS CNF format, and down to the LLVM code implementing the checker.

For building the tool from the generated LLVM test, you need:

• Clang compiler (I used version 14.0.0, but everything >10.0 should be fine), and make
• Boost C++ Libraries with iostreams library

For checking the proofs, or viewing the proofs inside Isabelle, you additionally need:

• Working installation of Isabelle/HOL with the Archive of Formal Proofs installed as described here. We require version = Isabelle-2024.

In the main directory, run

  make

This will generate the executables ./code/lrat_isa and ./code/lrat_isa_dbg, and do a quick check that they've been correctly build. The former is the formally verified proof checker. The latter has been generated by modifying the exported LLVM code to include output of debug information.

Invoke the tool as

lrat_isa <cnf-file> [<lrat-file>]

If no lrat-file is specified, the certificate is read from standard input. On successful verification, it will print the line s VERIFIED UNSAT and exit with exit-code 0. Otherwise, it will print an error message and exit with a non-zero exit code.

Check out the example. From the main directory, run:

./code/lrat_isa ex/ex1.cnf ex/ex1.lrat

To stream the certificate directly from CaDiCaL (requires CaDiCaL>=v1.9.4):

cadical -n -q --lrat ex/ex1.cnf - | ./code/lrat_isa ex/ex1.cnf

We have also build a prototype script that uses a named pipe, and handles satisfiable and unsatisfiable formulas. It assumes cadical and lrat_isa on the path.

./cert_cadical.sh ex/ex1.cnf

You can browse the html version of the theories. Note that the presentation in the paper has been simplified for better readability, and typically uses shorter names than the actual formalization.

Good starting points for browsing:

• Main Theory contains code generation and final correctness theorem at end.

• DIMACS Grammar contains our grammar for Dimacs CNF, a succinct characterization of it's language, and a proof that it is unambiguous.

• Semantics of CNF, with our definition of satisfiability.

• Abstract Checker contains the abstract transition relation for the checker, and it's correctness

• Unit checking (check_uot) the inner loop of our checker.

• Data Structures (the theories contain the abstract versions and the LLVM implementations)

  • Literal Encoding

  • Reversible Partial Assignment

  • Clauses

  • Clause Builder

  • Clause Database

  • Concrete checker states: outside proof (op) build-clause (bc) in proof (ip)

Run

  isabelle jedit -d . -l Isabelle_LLVM thys/LRAT_Checker_Impl.thy

On the first invocation of this command, a base image with the required libraries is built, which may take several minutes. When invoked, the IDE will display the last theory of the formal development, where the exported code is generated, and the final correctness theorem is proved. Moreover, the IDE will start to verify all dependent theories. If verification is finished (may take another few minutes), you can use the navigation features of the IDE to navigate the formalization and inspect the proof state.

In the main directory, run

  make check_thys

This will invoke Isabelle to check all proofs and re-generate the exported code, which is written to code/lrat_isa_export.ll This may take a while, in particular on the first invocation, when Isabelle builds some prerequisites.