MIRI's publications seem to exclusively refer to TDT

Why do you say that? If I do a search for "UDT" or "TDT" on intelligence.org, I seem to get about an equal number of results.

people here on LW seem to refer pretty much exclusively to UDT in serious discussion

This seems accurate to me. I think what has happened is that UDT has attracted a greater "mindshare" on LW, to the extent that it's much easier to get a discussion about UDT going than about TDT. Within MIRI it's probably more equal between the two.

that UDT is just an uninteresting variant of TDT so as to hardly merit its own name

As I recall, Eliezer was actually the one who named UDT. (Here's the comment where he called it "updateless", which everyone else then picked up. In my original post I never gave it a name but just referred to "this decision theory".)

Has either one been fully specified/formalized?

There has been a number of attempts to formalize UDT, which you can find by searching for variations on "formal UDT" on LW. I'm not aware of a similar attempt to formalize TDT, although this paper gives some hints about how it might be done. It's not really possible to "fully" specify either one at this time because both need to interface with a to-be-discovered solution to the problem of logical uncertainty, and at this point we don't even know the type signature of such a solution. In the attempts to formalize UDT, people either make a guess as to what the type signature is, or side-step the problem by assuming that all relevant logical facts can be deduced by the agent.

I'm not serious, but I'd say that there's little actual use of TDT because it requires us to solve the difficult problem of finding the right causal and logical structure of the problem - this can be handwaved in by the user, but doing that feels awkward. Folk-UDT ("just execute the best strategy") is sufficient for most purposes, both in application and in e.g. trying to understand logical uncertainty.

On the other hand, using causal structure is what lets us consider hypotheticals properly - so TDT will not have some issues that typical-UDT does with hypotheticals about its own actions. On the mutant third hand, TDT's solution of adding logical nodes to the causal structure might just be a simplification of something deeper, so it's not like we (us non-serious decision-theory dilettantes) should put all our eggs in one basket.

Has either one been fully specified/formalized?

Here's one attempt to further formalize the different decision procedures: http://commonsenseatheism.com/wp-content/uploads/2014/04/Hintze-Problem-class-dominance-in-predictive-dilemmas.pdf (H/T linked by Luke)

Good questions!

All the things you've heard are consistent and together they answer your final question by denying that there is a discrepancy in choice of theory, just in choice of name. (Not that I'm sure that all the things you've heard are true.)