Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny

TL;DR

This paper presents a fully verified SAT solver implementing the DPLL algorithm in Dafny, demonstrating that auto-active verification can produce trustworthy solvers with competitive performance.

Contribution

The paper introduces the first fully verified DPLL SAT solver in Dafny, combining formal correctness guarantees with practical efficiency.

Findings

Dafny solver is as efficient as C# implementation

Dafny solver is roughly half as fast as C++ implementation

Auto-active verification offers a promising balance between trustworthiness and performance

Abstract

We build a SAT solver implementing the DPLL algorithm in the verification-enabled programming language Dafny. The resulting solver is fully verified (soundness, completeness and termination are computer checked). We benchmark our Dafny solver and we show that it is just as efficient as an equivalent DPLL solver implemented in C# and roughly two times less efficient than an equivalent solver written in C++. We conclude that auto-active verification is a promising approach to increasing trust in SAT solvers, as it combines a good trade-off between execution speed and degree of trustworthiness of the final product.