IsaSAT is one of the few verified SAT solvers (and to my knowledge the only one that is currently maintained). It is verified in Isabelle using the Isabelle Refinement Framework by synthesizing code. See the presentation for more details.