It isn't at all obvious that "a theorem prover proving itself correct" and "an axiomatic system proving its own consistency" are the same thing, beyond both being in the category of things which refer to themselves in the domain of mathematical proofs. Software correctness isn't the same as consistency. A program is correct if it refines its specification, and an axiomatic system is consistent if it does not lead to contradiction. Before doing a deep dive into Gödel we need to firmly establish we're actually looking at the right problem.

Even if Gödel is shown to apply in the strict generalized theoretical sense, it might be irrelevant to practice. Theory and practice often differ enough for practice to be very useful; we easily prove halting for most programs we care about, compute solutions to average-case NP-Complete problems without a noticeable rise in CPU temp, and (as the other poster at this level said) write compression algorithms which work well on all relevant inputs. This is poor analogous reasoning, of course, but I include it because demonstration of universal practical pitfall would be very interesting in much the same way specific manifestations of availability loss in fault-tolerant consensus algorithms are interesting.

Really though, I am tired of the above exact exchange playing out in every thread I've seen here on formal verification. Someone raises the obvious concern of bugs in the theorem prover. Someone else raises the bootstrapping solution, cribbed from compilers. Someone else raises the Gödel objection; and there the conversation dies. Dig deeper.