3a. Towards Formal Corrigibility — LessWrong