Programming Languages Going Above and Beyond

This page summarizes the projects mentioned and recommended in the original post on

Our great sponsors
  • Onboard AI - Learn any GitHub repo in 59 seconds
  • InfluxDB - Collect and Analyze Billions of Data Points in Real Time
  • SaaSHub - Software Alternatives and Reviews
  • dafny

    Dafny is a verification-aware programming language

    > I think we can assume it won't be as efficient has hand written code

    Actually, surprisingly, not necessarily the case!

    If you'll refer to the discussion in and in, Dafny can statically prove that certain compiler branches are not possible and will never be taken (such as out-of-bounds on index access, logical assumptions about whether a value is greater than or less than some other value, etc). This lets you code in the assumptions (__assume in C++ or unreachable_unchecked() under rust) that will allow the compiler to optimize the codegen using this information.

  • prusti-dev

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

    You might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specifications such as pre and post-conditions, loop body invariants, termination checking and so on.

  • Onboard AI

    Learn any GitHub repo in 59 seconds. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at

  • evm-dafny

    An EVM interpreter in Dafny

  • z3

    The Z3 Theorem Prover

    I believe, Nim also has this functionality, although, it uses the [0]Z3Prover tool with a nim frontend [1]"DrNim" for proving.


  • tlaplus

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

    I wish something like Lamport's TLA+ ( was supported in modern language compilers - perhaps with annotations/macros and a mini formal DSL.

  • quint

    Executable specification language with delightful tooling (by informalsystems)

    It's still in pretty early development, but you may be interested in

    > It combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art static analysis and development tooling.

    And it is typed ;)

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts