Prusti: Static Analyzer for Rust

This page summarizes the projects mentioned and recommended in the original post on

Our great sponsors
  • InfluxDB - Power Real-Time Data Analytics at Scale
  • WorkOS - The modern identity platform for B2B SaaS
  • 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:

    ... and now I just noticed that prusti has a crate prusti_contracts that can do the same thing!!

    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

  • InfluxDB

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

    There also appear to be equivalents of this tool in Python ("Nagini" and Go ("Gobra"

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

  • AdGuardDNS

    Public DNS resolver that protects you from ad trackers


    Rust mid-level IR Abstract Interpreter

    Here's a 2020 overview of 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!


    Now, on that list, there is also that, alongside the crate (with the mirai_assertion feature enabled) enables writing code like this

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

  • WorkOS

    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.

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