Prusti: Static Analyzer for Rust

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

Our great sponsors
  • SonarLint - Clean code begins in your IDE with SonarLint
  • InfluxDB - Build time-series-based applications quickly and at scale.
  • SaaSHub - Software Alternatives and Reviews
  • prusti-dev

    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

    Catch common Java mistakes as compile-time errors

  • SonarLint

    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

    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

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

  • gobra

    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

    Public DNS resolver that protects you from ad trackers

  • MIRAI

    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

    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.

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