  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.
