Dafny is cool, but I believe they tackle different problem spaces. For example, how would you verify a distributed algorithm with Dafny?

Check out IronFleet! https://www.microsoft.com/en-us/research/wp-content/uploads/...

Thanks, Hillel. I brought a speculation to a citation fight -- I'm glad you won :) Seriously, this is a very interesting read.

You absolutely can. TLA+ is basically a state transition system. Something you can write in Dafny and prove correct using its Refinement types. And the end result is running software you can drop right into production.