dafny

Dafny is a verification-aware programming language (by dafny-lang)

Dafny Alternatives

Similar projects and alternatives to dafny

  1. rust

    2,842 dafny VS rust

    Empowering everyone to build reliable and efficient software.

  2. InfluxDB

    InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.

    InfluxDB logo
  3. Django

    536 dafny VS Django

    The Web framework for perfectionists with deadlines.

  4. Pandas

    425 dafny VS 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

  5. csharplang

    The official repo for the design of the C# programming language

  6. buttplug-rs

    Rust Implementation of the Buttplug Sex Toy Control Protocol

  7. rocq

    88 dafny VS 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.

  8. lean4

    62 dafny VS lean4

    Lean 4 programming language and theorem prover

  9. SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
  10. FStar

    48 dafny VS FStar

    A Proof-oriented Programming Language

  11. tlaplus

    40 dafny VS tlaplus

    TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

  12. WeasyPrint

    49 dafny VS WeasyPrint

    The awesome document factory

  13. Idris2

    40 dafny VS Idris2

    A purely functional programming language with first class types

  14. z3

    31 dafny VS z3

    The Z3 Theorem Prover

  15. 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.

  16. prusti-dev

    23 dafny VS prusti-dev

    A static verifier for Rust, based on the Viper verification infrastructure.

  17. magmide

    A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

  18. zz

    10 dafny VS zz

    Discontinued πŸΊπŸ™ ZetZ a zymbolic verifier and tranzpiler to bare metal C

  19. mintable

    8 dafny VS mintable

    πŸƒ Automate your personal finances – for free, with no ads, and no data collection.

  20. pasv

    6 dafny VS pasv

    The Pascal-F Verifier

  21. Rust-for-Linux

    Adding support for the Rust language to the Linux kernel. (by Rust-for-Linux)

  22. koka

    33 dafny VS koka

    Koka language compiler and interpreter

  23. SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
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

Log in or Post with

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 2025-01-28.
  • Long division verified via Hoare logic
    1 project | news.ycombinator.com | 26 Feb 2025
    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
    2 projects | dev.to | 28 Jan 2025
    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
    6 projects | news.ycombinator.com | 6 Jan 2025
    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
    5 projects | news.ycombinator.com | 25 Dec 2024
    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
    2 projects | news.ycombinator.com | 16 Oct 2024
    > 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/ ?

  • Verified Rust for low-level systems code
    6 projects | news.ycombinator.com | 4 May 2024
    For those that are interested but perhaps not aware in this similar project, Dafny is a "verification-aware programming language" that can compile to rust: https://github.com/dafny-lang/dafny
  • Dafny is a verification-aware programming language
    4 projects | news.ycombinator.com | 23 Apr 2024
  • Candy – a minimalistic functional programming language
    5 projects | news.ycombinator.com | 24 Feb 2024
  • Dafny – a verification-aware programming language
    1 project | news.ycombinator.com | 28 Nov 2023
  • Lean4 helped Terence Tao discover a small bug in his recent paper
    10 projects | news.ycombinator.com | 27 Oct 2023
    Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model.

    C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead.

    The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5].

    [1] https://www.microsoft.com/en-us/research/project/code-contra...

    [2] https://github.com/Z3Prover/z3

    [3] https://github.com/microsoft/CodeContracts

    [4] https://github.com/dafny-lang/dafny

    [5] https://github.com/dotnet/csharplang/issues/105

  • A note from our sponsor - SaaSHub
    www.saashub.com | 13 Jun 2025
    SaaSHub helps you find the best software and product alternatives Learn more β†’

Stats

Basic dafny repo stats
38
3,092
9.5
7 days ago

Sponsored
InfluxDB – Built for High-Performance Time Series Workloads
InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.
www.influxdata.com

Did you know that C# is
the 10th most popular programming language
based on number of references?