Dafny
Fewer than 5 people recommend it so far, so there's no written verdict. Here is what commenters said.
4recommend
0warn against
Nov 2, 2025first mention
Sep 18, 2026latest mention
Why people recommend it
“SPARK/Ada and Dafny work similarly, and have good documentation”
“dafny + iris are the closest to being industrial I think.”
Show 2 more
“See the Dafny language for some background”
Caveats and dissent
No one in these comments warned against it.
Often compared with
Who recommends it in their own words
Threads where it came up
- Developing provably correct Rust code with Verus 2 mentions
- Bend 2 and the Vibe-Coding Trap 1 mention
- Formal Methods and the Future of Programming 1 mention
- There's Never Been a Better Time to Study Computer Science 1 mention
- Vera: a programming language designed for machines to write 1 mention
- I formally verified AI-generated code. All 4 bugs were in the integration layer 1 mention
Data: dafny.json. Quotes are verbatim; the verdict and theme labels are written by a model from these comments, and every clause links to its sources.
All comments 9
“my main toolbox of formal verification tools in the past have been Rocq, Idris, Dafny, and TLA+”
“The former, I don't know if anyone actually uses it in production though theoretically you can”
“SPARK/Ada and Dafny work similarly, and have good documentation”
“dafny + iris are the closest to being industrial I think.”
“See the Dafny language for some background”
“This reminds me of Dafny: https://dafny.org/”
“uses Dafny (backed by Z3)”
“Dafny is really approachable and practical”
“Leftpad proofs using Rust Creusot, Dafny, or LiquidHaskell are quite straightforward”