Creusot Alternatives
Similar projects and alternatives to creusot
-
misra-rust
An investigation into what adhering to each MISRA-C rule looks like in Rust. The intention is to decipher how much we "get for free" from the Rust compiler.
-
-
SonarLint
Deliver Cleaner and Safer Code - Right in Your IDE of Choice!. SonarLint is a free and open source IDE extension that identifies and catches bugs and vulnerabilities as you code, directly in the IDE. Install from your favorite IDE marketplace today.
-
-
-
-
-
-
Scout APM
Less time debugging, more time building. Scout APM allows you to find and fix performance issues with no hassle. Now with error monitoring and external services monitoring, Scout is a developer's best friend when it comes to application development.
-
-
-
-
-
prusti-dev
A static verifier for Rust, based on the Viper verification infrastructure.
-
-
unsafe-code-guidelines
Home for the Unsafe Code Guidelines working group.
-
rust-verification-tools
RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.
-
app-template
Quickly set up a `probe-run` + `defmt` + `flip-link` embedded project (by knurling-rs)
-
-
-
creusot reviews and mentions
-
What Is Rust's Unsafe?
I’m doing my PhD on the formal verification of Rust, and while you’re right that safe code provides a lot of informal advantages it also dramatically simplified form reasoning.
In particular, the dirty secret of C verifiers is that they don’t handle pointers all that well. Either you find yourself doing a lot of manual proof work or you have to dramatically simplify the memory model.
In contrast, when verifying safe Rust, the rules of the borrow checker allow us to dramatically simplify the verification work. All of a sudden verifying a manual memory program with pointers (borrows) becomes as simple as verifying a basic imperative language. I’ve been working on a tool: https://github.com/xldenis/creusot to put this into practice
On the other hand, the moment you dive into unsafe, all bets are off and you find yourself wading through the marshes of (weak) memory models with your favorite CSL as your only friend.
> I’ve been working on a tool: https://github.com/xldenis/creusot to put this into practice
Note that there are other tools trying to deal with formal statements about Rust code. AIUI, Rust developers are working on forming a proper working group for pursuing these issues. We might get a RFC-standardized way of expressing formal/logical conditions about Rust code, which would be a meaningful first step towards supporting proof-carrying code within Rust.
-
AdaCore and Ferrous Systems Joining Forces to Support Rust
This is exciting! I've met with people from AdaCore and Ferrous systems (individually) several times and they're all serious, competent and motivated.
I'm curious what kinds of software they want to (eventually) verify, my PhD thesis is developing a verification tool for Rust (https://github.com/xldenis/creusot) and I'm always on the look out for case studies to push me forward.
The road to formally verified Rust is still long but in my unbiased opinion looking quite bright, especially compared to other languages like C.
-
Uncovered Intermediate Topics
An introduction to formal verification in Rust! The whole field is probably is probably too big to cover fully, but an introduction should fit in a single lecture :) Topics that come to mind are Prusti, Cruseot, RustBelt, RustHorn, Stacked Borrows, Miri. These also lend themselves to do follow up topics on.
-
Automatic Rust verification tools (2021)
Found another one: https://github.com/xldenis/creusot
-
From Rust to SPARK: Formally Proven Bip-Buffers
There's a couple prototypes already, such as Prusti or Creusot.
-
Safer Rust: Program Verification with Creusot [video]
Project in github for those who don't have the time to watch the video: https://github.com/xldenis/creusot
Stats
xldenis/creusot is an open source project licensed under GNU Lesser General Public License v3.0 only which is an OSI approved license.
Popular Comparisons
There are 7 new remote jobs listed recently.
Are you hiring? Post a new remote job listing for free.