We present an Isabelle/HOL formalization of Simple Clause Learning for first-order logic without equality: SCL(FOL). The main results are formal proofs of soundness, non-redundancy of learned clauses, termination, and refutational completeness. Compared to the unformalized version, the formalized calculus is simpler, a number of results could be generalized, and the non-redundancy strengthened. We found one bug in a previously published version of the SCL Backtrack rule. Compared to related formalizatons, we introduce a new technique for showing termination based on non-redundant clause learning.