  This paper attempts to address the question of how best to assure the
correctness of saturation-based automated theorem provers using our experience
developing the theorem prover Vampire. We describe the techniques we currently
employ to ensure that Vampire is correct and use this to motivate future
challenges that need to be addressed to make this process more straightforward
and to achieve better correctness guarantees.
