facebookexperimental/MIRAI
View on GitHub ↗ ★ 1,009 Rust archived
Rust mid-level IR Abstract Interpreter
7 mentions on Hacker News by 4 people: 0 stories, 7 comments · first 2020-09-04 · latest 2023-01-02
20082026
-
…MIRAI prover thing? I always thought it this was super neat: https://crates.io/crates/contracts https://github.com/facebookexperimental/MIRAI/blob/main/exam... [dependencies] mirai-annotations = ... contracts = {version = "XXX", features =…
comment by gavinray · 2023-01-02 · in Adding design-by-contract conditions to C++ via a GCC plugin -
…> https://marketplace.visualstudio.com/items?itemName=viper-ad... Now, on that list, there is also https://github.com/facebookexperimental/MIRAI that, alongside the crate https://crates.io/crates/contracts (with the mirai_assertion feature…
comment by nextaccountic · 2022-10-14 · in Prusti: Static Analyzer for Rust -
…by default check the contracts at runtime, but has an option to check them at compile time with https://github.com/facebookexperimental/MIRAI Now, this Rust library isn't generally understood as creating another type system on top of Rust,…
comment by nextaccountic · 2022-10-02 · in Ten Years of TypeScript -
…type errors can't catch. Now, there are some crates like https://github.com/dtolnay/no-panic or https://github.com/facebookexperimental/MIRAI that will check that your code is panic free. The first one is based on the fact that llvm…
comment by nextaccountic · 2022-09-14 · in A pair of Linux kernel modules using Rust -
…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…
comment by Klasiaster · 2022-03-25 · in Kani Rust Verifier – a bit-precise model-checker for Rust -
also what https://github.com/facebookexperimental/MIRAI does for rust: you add contracts (preconditions, postconditions, and invariants) using https://docs.rs/contracts/0.6.0/contracts/ and it checks whether they are true here is an…
comment by nextaccountic · 2021-08-11 · in Kind: A Modern Proof Language -
Check mirai https://github.com/facebookexperimental/MIRAI
comment by baby · 2020-09-04 · in Rust testing or verifying: Why not both?