Presentamos un solucionador SAT DPLL, al que llamamos TrueSAT, desarrollado en el lenguaje de programación con verificación Dafny. Hemos verificado completamente la corrección funcional de nuestro solucionador construyendo pruebas verificadas por máquina de su corrección, completitud y terminación. Presentamos un benchmark del tiempo de ejecución de TrueSAT y mostramos que es competitivo frente a un solucionador DPLL equivalente implementado en C++, aunque sigue siendo más lento que los solucionadores CDCL de última generación. Nuestro solucionador sirve como un estudio de caso significativo de un sistema de software verificado por máquina. El benchmark también muestra que la verificación auto-activa es un enfoque prometedor para aumentar la confianza en los solucionadores SAT, ya que combina la velocidad de ejecución con un alto grado de confiabilidad.