You might find this paper interesting (uses examples in Dafny) - https://news.ycombinator.com/item?id=47334375