SaaSHub helps you find the best software and product alternatives Learn more →
Dafny Alternatives
Similar projects and alternatives to dafny
-
-
ReSharper
ReSharper is now available in VS Code and Cursor. ReSharper brings a professional toolset for C# developers backed by over 20 years of experience, enterprise-grade security, SOC 2 compliance, and the trust of companies worldwide.
-
-
Pandas
Flexible and powerful data analysis / manipulation library for Python, providing labeled data structures similar to R data.frame objects, statistical functions, and much more
-
-
-
rocq
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
-
-
-
tlaplus
TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
-
-
-
checkedc
Checked C is an extension to C that lets programmers write C code with bounds checking and improved type-safety. The goal is to let people easily make their existing C code type-safe and eliminate entire classes of errors.
-
-
magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
-
-
-
-
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
NOTE:
The number of mentions on this list indicates mentions on common posts plus user suggested alternatives.
Hence, a higher number means a better dafny alternative or higher similarity.
dafny discussion
dafny reviews and mentions
Posts with mentions or reviews of dafny.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2026-05-20.
- There's Never Been a Better Time to Study Computer Science
-
Learnings from 100K lines of Rust with AI (2025)
It's a set of asserts that are a part of the type signature. Requires are asserts on the inputs, ensures are asserts on the outputs.
Depending on your backend you either ignore them, check them all of the time, some of the time, or have SMT-solvers prove that if you uphold the first one all else must follow.
If you're interested in the last one, have a look at Dafny[0]
[0] https://dafny.org/
-
Vera: a programming language designed for machines to write
> The signature declares types, preconditions, postconditions, and effects. The compiler verifies the contract via SMT solver.
This reminds me of Dafny: https://dafny.org/
Actually, that would be an interesting question: how good are LLMs at writing (correct) Dafny?
- Dafny: Verification-Aware Programming Language
-
Verified Ordered Set in Dafny
In the world of software development, we spend countless hours writing tests to prevent bugs. But what if we could prove, with mathematical certainty, that our code is free of entire classes of errors? This is the promise of formal verification, and tools like Dafny are making it more accessible than ever.
-
Long division verified via Hoare logic
Automation of Hoare logic is quite good these days. Dafny, from MS Research (https://dafny.org), is probably the most friendly formal language. Dafny has been used to verify large systems, including many components of AWS. I am hoping that LLMs make more advanced languages, such as Liquid Haskell or Agda, much easier to write. Ideally, lots of code should be autocompleted once a human provides a type signature. The advantage of formal verification is that we are sure the generated code is correct.
-
Automated reasoning and generative AI: Harness creativity with formal verifications
Modern software verification employs various approaches, each offering different trade-offs between ease of use and strength of guarantees. AWS contributes to the open source program verification tools used in the previous examples. Dafny and Kani represent two powerful approaches to program verification. Let's see how they work in practice before connecting the dots between automated reasoning and generative AI.
-
Playing Chess with 84,688 Regular Expressions
On that note, I discovered Dafny[1] recently, as a more accessible way to program with proofs. There's a companion book[2] that seems very accessible and down-to-earth (and, unfortunately, quite expensive). I didn't have the time to play with it yet, but it looks like it does what Ada/SPARK does (and more), but with less verbose syntax and more options for compilation targets. It seems to be actively developed, too. Personally, I had a very hard time getting into Coq, which is a proof assistant more than a programming environment - Dafny seems much more welcoming for a "working programmer" :)
[1] https://dafny.org/
[2] https://mitpress.mit.edu/9780262546232/program-proofs
-
F*: A proof oriented general purpose programming language
https://dafny.org/ also allows proof checking and allows do write real programs with it. It has a java like syntax and is also from MS I believe
-
Safer with Google: Advancing Memory Safety
> I do think there's a bit of the Ignaz Semmelweis[1] issue at hand here, where developers want to believe in their inherent quality and refuse processes that improve safety if it goes against their worldview
I think the problem is that other variables (not only safety) must be assessed beyond the pure "better". Haskell is very good also. Very correct. Who uses that, and where? And why? Why not everyone uses https://dafny.org/ ?
-
A note from our sponsor - SaaSHub
www.saashub.com | 15 Jun 2026
Stats
Basic dafny repo stats
43
3,431
8.3
4 days ago
dafny-lang/dafny is an open source project licensed under GNU General Public License v3.0 or later which is an OSI approved license.
The primary programming language of dafny is C#.
Sponsored
ReSharper is now available in VS Code and Cursor
ReSharper brings a professional toolset for C# developers backed by over 20 years of experience, enterprise-grade security, SOC 2 compliance, and the trust of companies worldwide.
www.jetbrains.com