It's worth mentioning Mathias Fleury work who first verified a CDCL implementation [1]. He has written follow-up stuff.

[1] https://fmv.jku.at/fleury/papers/Fleury-thesis.pdf