Kani Rust Verifier – a bit-precise model-checker for Rust

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

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

    Kani Rust Verifier

    Looks like that the project has changed its name from "rmc" (Rust Model Checker) to this. Various sources point to rmc as https://github.com/model-checking/rmc (redirected to https://github.com/model-checking/kani) and https://model-checking.github.io/rmc/ (404). Anyone knows why?

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

    Discontinued Rust mid-level IR Abstract Interpreter

    Nice, I just would have liked to get all these different verification tools combined under the same interface, just being different backends as drafted by the rust verification tools work of project oak: have "cargo verify" as common command and use common test annotations, allowing the same test to be verified with different backends or just fuzzed/proptested.

    The model checking approach seems to be a bit limited regarding loops. There are also abstract interpreters, such as https://github.com/facebookexperimental/MIRAI, and symbolic executers, such as https://github.com/dwrensha/seer or https://github.com/GaloisInc/crucible.

    Overall I believe this space would benefit from more coordination and focus on developing something that has the theoretical foundations to cover as many needs as possible and then make a user-friendly tool out of it that is endorsed by the Rust project similar to how Rust analyzer is the one language server to come.

  4. seer

    symbolic execution engine for Rust (by dwrensha)

    Nice, I just would have liked to get all these different verification tools combined under the same interface, just being different backends as drafted by the rust verification tools work of project oak: have "cargo verify" as common command and use common test annotations, allowing the same test to be verified with different backends or just fuzzed/proptested.

    The model checking approach seems to be a bit limited regarding loops. There are also abstract interpreters, such as https://github.com/facebookexperimental/MIRAI, and symbolic executers, such as https://github.com/dwrensha/seer or https://github.com/GaloisInc/crucible.

    Overall I believe this space would benefit from more coordination and focus on developing something that has the theoretical foundations to cover as many needs as possible and then make a user-friendly tool out of it that is endorsed by the Rust project similar to how Rust analyzer is the one language server to come.

  5. crucible

    Crucible is a library for symbolic simulation of imperative programs

    Nice, I just would have liked to get all these different verification tools combined under the same interface, just being different backends as drafted by the rust verification tools work of project oak: have "cargo verify" as common command and use common test annotations, allowing the same test to be verified with different backends or just fuzzed/proptested.

    The model checking approach seems to be a bit limited regarding loops. There are also abstract interpreters, such as https://github.com/facebookexperimental/MIRAI, and symbolic executers, such as https://github.com/dwrensha/seer or https://github.com/GaloisInc/crucible.

    Overall I believe this space would benefit from more coordination and focus on developing something that has the theoretical foundations to cover as many needs as possible and then make a user-friendly tool out of it that is endorsed by the Rust project similar to how Rust analyzer is the one language server to come.

  6. awesome-rust-formalized-reasoning

    An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

    This dispersed progress is the sign of an absence of maturity but the exploration of this space with Rust is very promising : https://github.com/newca12/awesome-rust-formalized-reasoning

  7. rmc

    Discontinued Kani Rust Verifier [Moved to: https://github.com/model-checking/kani]

    Looks like that the project has changed its name from "rmc" (Rust Model Checker) to this. Various sources point to rmc as https://github.com/model-checking/rmc (redirected to https://github.com/model-checking/kani) and https://model-checking.github.io/rmc/ (404). Anyone knows why?

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

  • CreuSAT: Formally verified SAT solver written in Rust and verified with Creusot

    3 projects | news.ycombinator.com | 17 Jun 2022
  • Why We Chose Rust For Spin

    8 projects | dev.to | 27 Jun 2025
  • RSS Server Side Reader

    4 projects | news.ycombinator.com | 26 Jun 2025
  • Stop struggling with Rust CLI tool installs: the only guide you need (Mac, Linux, Windows)

    5 projects | dev.to | 19 Jun 2025
  • Rustls Server-Side Performance

    5 projects | news.ycombinator.com | 17 May 2025

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