Dexter's smart contract has been formally verified by Nomadic Labs.
The behavior of the smart contract is described by the informal specification found here.
This specification has been formalized in the proof assistant Coq, and Dexter has been proven to satisfy it with a computer-checked proof. This ensures that there are no divergences between the specification and the implementation of Dexter.
The full development is available here.