Formalized priority argument
Computability theory in general has been somewhat under-formalized. The short answer is that most theorems of computability theory do not pass one of the three tests for formalization:


A proof that is computationally intensive or untrusted for some reason (long, complex).
A result that is relevant to undergraduate mathematics.
A result that is useful to program verification.


Reason 1 may apply in this case, but the preliminary work to build up to that result unfortunately hasn't been carried out. I found one reference to mechanized computability theory by Xu, Zhang and Urban in Isabelle. It falls significantly short of priority results though.