Programming Languages Going Above and Beyond

• dafny

  11 2,528 0.0 C#

  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 https://github.com/dafny-lang/dafny/issues/601 and in https://github.com/dafny-lang/dafny/issues/547, 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

  7 1,369 0.0 Rust

  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.

  https://github.com/viperproject/prusti-dev

• Onboard AI

  getonboard.dev

  sponsored

  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 www.getonboard.dev.

  

• evm-dafny

  1 106 7.9 Dafny

  An EVM interpreter in Dafny

  

• z3

  8 9,192 9.7 C++

  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.

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

• tlaplus

  12 2,123 0.0 Java

  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+ (https://lamport.azurewebsites.net/tla/tla.html) was supported in modern language compilers - perhaps with annotations/macros and a mini formal DSL.

• quint

  2 206 9.7 TypeScript

  Executable specification language with delightful tooling (by informalsystems)

  

  It's still in pretty early development, but you may be interested in https://github.com/informalsystems/quint

  > 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 ;)

Suggest a related project