To clarify, they implemented the algorithm in Dafny, and then proved that version correct. They did not verify code that will actually run in production.

From the paper:

> Dafny is a practical option for the verification of mission-critical smart contracts, and a possible avenue for adoption could be to extend the Dafny code generator engine to support Solidity … or to automatically translate Solidity into Dafny. We are currently evaluating these options