Dafny's verification system can be too rigorous for high performance and rapidly changing codebases. S3 team had a paper[1] last year on how they verified ShardStore using a lightweight formal verification system. Since the system was written in Rust, they wrote their verifier in Rust, as well.

[1] https://assets.amazon.science/07/6c/81bfc2c243249a8b8b65cc21...