crucible
kani
Our great sponsors
- Appwrite - The Open Source Firebase alternative introduces iOS support
- InfluxDB - Access the most powerful time series database as a service
- SonarLint - Clean code begins in your IDE with SonarLint
- ONLYOFFICE ONLYOFFICE Docs — document collaboration in your environment
| crucible | kani | |
|---|---|---|
| 2 | 30 | |
| 532 | 1,123 | |
| 2.4% | 5.3% | |
| 8.0 | 8.5 | |
| about 9 hours ago | about 8 hours ago | |
| HTML | Rust | |
| - | Apache License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
crucible
-
Kani Rust Verifier – a bit-precise model-checker for Rust
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.
-
Type Theory Forall Podcast #13 - C/C++, Emacs, Haskell, and Coq. The Journey (John Wiegley)
When we talk about formal methods being used in the industry I honestly think Galois' approach is the future. The main idea is to symbolically execute llvm code and run a SAT solver on the desired properties. See Crucible and SAW.
kani
-
Kani 0.28.0 has been released!
Here's a summary of what's new in version 0.28.0:
-
Kani 0.27.0 has been released!
However, there may be more down the line since we don't have (1) for now. If you're interested, would you mind commenting to this issue?
We're excited to announce the release of Kani Rust Verifier v0.27.0! Kani is a bit-precise model checker for Rust, and this new release comes with exciting changes and improvements.
-
Is there something like "super-safe" rust?
kani (e.g. used by hifitime)
-
Must move types by Niko Matsakis
Doing this legwork for unsafe code is 100% required, and the compiler isn't of much help here (but there are external tools that check unsafe code like kani).
-
Kani 0.23.0 has been released
change about to be merged.. thanks for the contribution! https://github.com/model-checking/kani/pull/2287
I did the thing.
-
Teaching Rust 101 at Imperial College
I would also spend a bit of time talking about how unsafe code can be used appropriately. And along with that you have the responsibility of doing the verification on u u our own using tools like kani
-
Prop v0.42 released! Don't panic! The answer is... support for dependent types :)
Wow that sounds really cool! I'm not an expert but does that mean that one day you could implement dependend types or refinement types in Rust as a crate ? I currently only know of tools like: Flux Creusot Kani Prusti
What are some alternatives?
prusti-dev - A static verifier for Rust, based on the Viper verification infrastructure.
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.
MIRAI - Rust mid-level IR Abstract Interpreter
rmc - Kani Rust Verifier [Moved to: https://github.com/model-checking/kani]
rustig - A tool to detect code paths leading to Rust's panic handler
gdbstub - An ergonomic and easy-to-integrate implementation of the GDB Remote Serial Protocol in Rust, with full no_std support.
watt - Runtime for executing procedural macros as WebAssembly
seer - symbolic execution engine for Rust
macro_railroad_ext - Display syntax-diagrams for Rust-macros on docs.rs and doc.rust-lang.org
paxakos - Rust implementation of Paxos consensus algorithm
coq-of-ocaml - Formal verification for OCaml