Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free. Learn more →
Top 7 Rust Verification Projects
-
Project mention: CVE-2023-4863: Heap buffer overflow in WebP (Chrome) | news.ycombinator.com | 2023-09-12
> those applications need the proof for correctness so that more dangerous code---say, what would need `unsafe` in Rust---can be safely added
There are actually already tools built for this very purpose in Rust (see Kani [1] for instance).
Formal verification has a serious scaling problem, so forming programs in such a way that there are a few performance-critical areas that use unsafe routines seems like the best route. I feel like Rust leans into this paradigm with `unsafe` blocks.
-
You might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specifications such as pre and post-conditions, loop body invariants, termination checking and so on.
-
SonarQube
Static code analysis for 29 languages.. Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.
-
creusot
deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications!
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.
-
-
-
Project mention: A Python package written in Rust for email verification without sending any emails. | /r/Python | 2023-04-12
-
-
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.
Rust Verification related posts
- Kani 0.36.0 has been released!
- Kani 0.34.0 has been released!
- Kani 0.33.0 has been released!
- Kani 0.32.0 has been released!
- Conditioonal Compilation across Crates?
- Kani 0.31.0 has been released
- Formal verification for unsafe code?
-
A note from our sponsor - SonarQube
www.sonarqube.org | 28 Sep 2023
Index
What are some of the best open-source Verification projects in Rust? This list will help you:
Project | Stars | |
---|---|---|
1 | kani | 1,410 |
2 | prusti-dev | 1,330 |
3 | creusot | 765 |
4 | ed25519-dalek | 638 |
5 | CreuSAT | 542 |
6 | pyrustify | 14 |
7 | lincheck | 6 |