Formally Verifying a Real World Smart Contract. - Alexandre Mota 001; Fei Yang; Cristiano Teixeira (CoRR, 2023)