Having used both Dafny and F* quite extensively, Dafny, and its predecessor Spec#, are simple and practical, thanks to being based on Hoare logic (contracts).

It's a great place to start with verification, as proofs are discharged to SAT/SMT, so things are automated. It can get a bit frustrating when automation is not able to prove things, that's the major disadvantage of SAT/SMT.

But it's not a toy. Some of the largest verification efforts have been done in Dafny. See e.g. IronFleet [1].

[1] https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf