Residual finite simplicity of $\mathrm{Aut}(F_2)$

Let $F_2$ be the free group on two generators. A group is fully residually finite simple if, for every finite subset of its nontrivial elements, there is a homomorphism to a finite simple group whose restriction to that subset is injective. Residual finite simplicity conjecture. $\mathrm{Aut}(F_2)$ is fully residually finite simple. The paper presents this as a strengthened version of its theorem on characteristic finite simple quotients and expects it to imply strong separation of finite subsets by finite simple quotients.