Prusti: Static Analyzer for Rust

• prusti-dev

  10 1,202 9.6 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

  8 6,326 9.7 Java

  Catch common Java mistakes as compile-time errors

  

• SonarLint

  www.sonarlint.org

  sponsored

  Clean code begins in your IDE with SonarLint. Up your coding game and discover issues early. SonarLint is a free plugin that helps you find & fix bugs and security issues from the moment you start writing code. Install from your favorite IDE marketplace today.

  

• SPARTA

  1 564 10.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

  26 13,805 9.9 OCaml

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

  

• gobra

  3 71 6.5 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

  34 577 3.4 Go

  Public DNS resolver that protects you from ad trackers

  

• MIRAI

  7 800 8.1 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()))]

• InfluxDB

  www.influxdata.com

  sponsored

  Build time-series-based applications quickly and at scale.. InfluxDB is the Time Series Platform where developers build real-time applications for analytics, IoT and cloud-native services. Easy to start, it is available in the cloud or on-premises.

  

Suggest a related project