Rust Formal Verification

Open-source Rust projects categorized as Formal Verification

Top 4 Rust Formal Verification Projects

Formal Verification
  • prusti-dev

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

    Project mention: Using_Prolog_as_the_AST | news.ycombinator.com | 2023-10-21

    > The overall goal would be to figure out classical error conditions like nill pointers deference.

    > If I can figure out if a pointer will be nil in some execution branch, there is no reason why a computer cannot do the same.

    Note, this is called flow-sensitive typing (also called type narrowing) and I think that typescript does it.

    https://en.wikipedia.org/wiki/Flow-sensitive_typing

    > I personally would see this as an human race level upgrades. Imagine feeding your code to a CI that spit back something like: "you will have a panic at line 156 when your input is > 4"

    A model checker can do that!

    See this

    https://model-checking.github.io/kani/tutorial-kinds-of-fail...

    Other techniques are also possible

    https://github.com/viperproject/prusti-dev#quick-example

    (Here I could link a lot of things, I just selected two Rust projects to illustrate)

    This works better if you are able to provide contracts in your API that says which guarantees you provide. Alternatively, asserts are useful too.

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

    InfluxDB logo
  • creusot

    Creusot helps you prove your code is correct in an automated fashion.

    Project mention: Release Creusot 0.1 · creusot-rs/creusot | news.ycombinator.com | 2024-05-20
  • CreuSAT

    CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

  • supervisionary

    The Supervisionary proof-checking kernel for higher-order logic

NOTE: The open source projects on this list are ordered by number of github stars. The number of mentions indicates repo mentiontions in the last 12 Months or since we started tracking (Dec 2020).

Rust Formal Verification discussion

Log in or Post with

Rust Formal Verification related posts

  • Release Creusot 0.1 · creusot-rs/creusot

    1 project | news.ycombinator.com | 20 May 2024
  • Creusot, a deductive verifier for Rust code

    1 project | news.ycombinator.com | 29 Feb 2024
  • Creusot, a deductive verifier for Rust code

    1 project | news.ycombinator.com | 25 Feb 2024
  • Conditioonal Compilation across Crates?

    1 project | /r/rust | 4 Jul 2023
  • Kani 0.29.0 has been released!

    2 projects | /r/rust | 31 May 2023
  • Trying to find a crate that allows you to constrain the value of arguments in various ways via a proc macro

    2 projects | /r/rust | 16 May 2023
  • Prop v0.42 released! Don't panic! The answer is... support for dependent types :)

    5 projects | /r/rust | 18 Jan 2023
  • A note from our sponsor - InfluxDB
    www.influxdata.com | 15 Jul 2024
    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. Learn more →

Index

What are some of the best open-source Formal Verification projects in Rust? This list will help you:

Project Stars
1 prusti-dev 1,528
2 creusot 1,068
3 CreuSAT 598
4 supervisionary 3

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.
www.influxdata.com

Did you konow that Rust is
the 5th most popular programming language
based on number of metions?