Abstract. We provide a survey of the state of the art of 𝙧𝙖𝙩𝙞𝙤𝙣𝙖𝙡 𝙫𝙚𝙧𝙞𝙛𝙞𝙘𝙖𝙩𝙞𝙤𝙣: the problem of checking whether a given temporal logic formula 𝝋 is satisfied in some or all game theoretic equilibrium computations of a multi-agent system – that is, whether the system will exhibit the behaviour 𝝋 represents under the assumption that agents within the system act rationally in pursuit of their preferences. After motivating and introducing the overall framework of rational verification, we discuss key results obtained in the past few years as well as relevant related work in logic, AI, and Computer Science.