Rust Verification

Open-source Rust projects categorized as Verification

Top 8 Rust Verification Projects

Verification
  1. kani

    Kani Rust Verifier

    Project mention: Matt Godbolt sold me on Rust (by showing me C++) | news.ycombinator.com | 2025-05-06

    The point I'm sure was to prevent the checks from incurring runtime overhead in production. Even in release mode, the overflow will only wrap rather than trigger undefined behavior, so this won't cause memory corruption unless you are writing unsafe code that ignores the possibility of overflow.

    The checks being on in the debug config means your tests and replications of bug reports will catch overflow if they occur. If you are working on some sensitive application where you can't afford logic bugs from overflows but can afford panics/crashes, you can just turn on checks in release mode.

    If you are working on a library which is meant to do something sensible on overflow, you can use the wide variety of member functions such as 'wrapping_add' or 'checked_add' to control what happens on overflow regardless of build configuration.

    Finally, if your application can't afford to have logic bugs from overflows and also can't panic, you can use kani [0] to prove that overflow never happens.

    All in all, it seems to me like Rust supports a wide variety of use cases pretty nicely.

    [0]: https://github.com/model-checking/kani

  2. Stream

    Stream - Scalable APIs for Chat, Feeds, Moderation, & Video. Stream helps developers build engaging apps that scale to millions with performant and flexible Chat, Feeds, Moderation, and Video APIs and SDKs powered by a global edge network and enterprise-grade infrastructure.

    Stream logo
  3. prusti-dev

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

  4. creusot

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

    Project mention: Coq-of-rust: Formal verification tool for Rust | news.ycombinator.com | 2025-03-14
  5. ed25519-dalek

    Fast and efficient ed25519 signing and verification in Rust.

  6. CreuSAT

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

    Project mention: LIMO: Less Is More for Reasoning | news.ycombinator.com | 2025-02-09

    You tell it what you want it to prove. Or the tooling surrounding it does.

    The tooling surrounding it might want to prove that "this main function never invokes undefined behavior", or something more local like "for all possible inputs to the public interface to this module, no undefined behavior is invoked".

    Or you might want to specify constraints by hand. For examples, you might do that by writing normal tests except you can use magical variables that take on any value [1], or you might do that by annotating functions with contracts that they obey [2]. Or at a simpler level you might just annotate functions that should never panic.

    Ultimately once you can prove things about your code, it's a tool in the toolbox for querying how your code works. You can use that to write correct code from the start, or to debug incorrect code, or various other things. The problem is that right now the state of the art (non-ai) can't reason about very complex code without a lot of human help - making it a fairly impractical tool. I think AI might mange to fix that.

    [1] This is how kani works in rust, here's an example: https://github.com/model-checking/verify-rust-std/pull/112/f...

    [2] Creusot takes this route, here's an example https://github.com/sarsko/CreuSAT/blob/master/CreuSAT/src/so...

  7. anvil

    Anvil is an experimental framework to build practical, formally verified, cluster management controllers. (by anvil-verifier)

  8. pyrustify

    A Python package written in Rust for email verification without sending any emails.

  9. InfluxDB

    InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.

    InfluxDB logo
  10. lincheck

    A linearizability checker for concurrent data structures (by SmnTin)

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 Verification discussion

Log in or Post with

Rust Verification related posts

Index

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

# Project Stars
1 kani 2,600
2 prusti-dev 1,656
3 creusot 1,297
4 ed25519-dalek 704
5 CreuSAT 648
6 anvil 122
7 pyrustify 17
8 lincheck 11

Sponsored
Stream - Scalable APIs for Chat, Feeds, Moderation, & Video.
Stream helps developers build engaging apps that scale to millions with performant and flexible Chat, Feeds, Moderation, and Video APIs and SDKs powered by a global edge network and enterprise-grade infrastructure.
getstream.io

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