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.