Rust Formal Methods

Open-source Rust projects categorized as Formal Methods
Edit details
Topics: #Rust #Formal Verification #Verification #rust-lang #deductive-reasoning
Free Global Payroll designed for tech teams
Building a great tech team takes more than a paycheck. Zero payroll costs, get AI-driven insights to retain best talent, and delight them with amazing local benefits. 100% free and compliant.
try.revelo.com
Sponsored

Top 4 Rust Formal Method Projects

  • sled

    the champagne of beta embedded databases

    Project mention: RFC: redb (embedded key-value store) nearing version 1.0 | /r/rust | 2023-05-10

    Sled uses bw-tree actually https://github.com/spacejam/sled/wiki/sled-architectural-outlook

  • creusot

    deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications!

    Project mention: Conditioonal Compilation across Crates? | /r/rust | 2023-07-04

    However, it seems that C is not "notified" whether --cfg thing is set, only the main crate being built is. Regardless of this flag, the dummy macro is always chosen. Am I doing something wrong? It should work; the Creusot project is doing something similar.

  • InfluxDB

    Collect and Analyze Billions of Data Points in Real Time. Manage all types of time series data in a single, purpose-built database. Run at any scale in any environment in the cloud, on-premises, or at the edge.

  • 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). The latest post mention was on 2023-07-04.

Rust Formal Methods related posts

Index

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

Project Stars
1 sled 7,293
2 creusot 767
3 CreuSAT 545
4 supervisionary 3

Sponsored
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.
www.sonarlint.org