Prusti: Static Analyzer for Rust

• prusti-dev

  23 1,459 8.8 Rust

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

  

And have it checked at compile time that the assertion holds! Which is a bit like Liquid Haskell in capability: https://ucsd-progsys.github.io/liquidhaskell/

... and now I just noticed that prusti has a crate prusti_contracts that can do the same thing!! https://github.com/viperproject/prusti-dev/blob/master/prust...

Now I'm wondering which tool is more capable (as I understand, they leverage a SMT solver like Z3 to discharge the proof obligations, right?)

• Error Prone

  16 6,711 9.4 Java

  Catch common Java mistakes as compile-time errors

  

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

  

• SPARTA

  1 608 8.0 C++

  SPARTA is a library of software components specially designed for building high-performance static analyzers based on the theory of Abstract Interpretation. (by facebook)

  

• infer

  42 14,688 9.9 OCaml

  A static analyzer for Java, C, C++, and Objective-C

  

• gobra

  3 92 8.9 Scala

  Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.

  

According to the Readme, this is based on a more-general verification framework called Viper, which apparently works for several languages (including Rust): https://www.pm.inf.ethz.ch/research/viper.html

There also appear to be equivalents of this tool in Python ("Nagini" https://www.pm.inf.ethz.ch/research/nagini.html) and Go ("Gobra" https://www.pm.inf.ethz.ch/research/gobra.html).

I'll definitely be checking out Nagini for my work!

• AdGuardDNS

  60 727 4.4 Go

  Public DNS resolver that protects you from ad trackers

  

• MIRAI

  9 956 0.0 Rust

  Rust mid-level IR Abstract Interpreter

  

Here's a 2020 overview of Rust verification tools https://alastairreid.github.io/rust-verification-tools/ - it says

> Auto-active verification tools

> While automatic tools focus on things not going wrong, auto-active verification tools help you verify some key properties of your code: data structure invariants, the results of functions, etc. The price that you pay for this extra power is that you may have to assist the tool by adding function contracts (pre/post-conditions for functions), loop invariants, type invariants, etc. to your code.

> The only auto-active verification tool that I am aware of is Prusti. Prusti is a really interesting tool because it exploits Rust’s unusual type system to help it verify code. Also Prusti has the slickest user interface: a VSCode extension that checks your code as you type it!

> https://marketplace.visualstudio.com/items?itemName=viper-ad...

Now, on that list, there is also https://github.com/facebookexperimental/MIRAI that, alongside the crate https://crates.io/crates/contracts (with the mirai_assertion feature enabled) enables writing code like this

    #[ensures(person_name.is_some() -> ret.contains(person_name.unwrap()))]

• WorkOS

  workos.com sponsored

  The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

  

Suggest a related project