Programming Languages Going Above and Beyond

• dafny

  31 2,665 9.7 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

  23 1,466 8.5 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

• InfluxDB

  www.influxdata.com sponsored

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

• evm-dafny

  1 113 8.5 Dafny

  An EVM interpreter in Dafny

  

• z3

  28 9,708 9.8 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

  38 2,208 9.1 Java

  TLC is a 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

  6 584 9.8 TypeScript

  An executable specification language with delightful tooling based on the temporal logic of actions (TLA) (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