"every statement that can be derived also holds" is the difficult part to show, and something we refer to as soundness. For some fancy logics, it's not even possible to show, hence the discovered Kernel Soundness Bug in Lean!
"every statement that holds can also be derived", a notion known as completeness, is often a trivial property; in practice, we use refutation completeness instead, i.e. "every statement that doesn't hold can derive false". A bug that would allow a user to prove/derive a previously unproven statement would fall under this category of "completeness bug".
However, such completeness bugs immediately show up in testing. Generally, deduction systems have two kinds of rules: a handful of rules that are enough to establish (refutation) completeness, and then a few extra rules to optimize inference. Because so few rules are needed for completeness, lots of test cases will break if one of the rules break.
--
I'm not actually sure how the completeness situation looks like for proper provers like Lean. It's my graduate student's hubris to assume completeness remains easy to show for more advanced systems than the Superposition calculus ;)