Andrew Critch has a preprint on using Löb’s theorem to encode cooperation between agents. The idea is that proving that one is in the conditions of Löb’s theorem ensures a form of Lobian cooperation between agents, and can be used for the alignment problem.