Verifying the Conversion into CNF in Dafny.

We present two computer-verified implementations of the CNF conversion for propositional logic. The two implementations are fully verified: functional correctness and termination is machine-checked using the Dafny language for both. The first approach is based on repeatedly applying a set of equivalences and is often presented in logic textbooks. The second approach is based on Tseitin's transformation and is more efficient. We present the main ideas behind our formalization and we discuss the main difficulties in verifying the two algorithms.