At a recent MIRIx workshop, I gave an introductory talk about the surprising number of times that MIRI applied Löb's Theorem in their research papers. It was well-received, so I wrote up and expanded my notes into a primer for new researchers:

An Introduction to Löb's Theorem in MIRI Research (pdf)

Any comments appreciated!