creusot

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

Creusot Alternatives

Similar projects and alternatives to creusot

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better creusot alternative or higher similarity.

creusot reviews and mentions

Posts with mentions or reviews of creusot. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2023-05-31.
  • Kani 0.29.0 has been released!
    2 projects | /r/rust | 31 May 2023
    I believe https://github.com/xldenis/creusot is more similar in that it also uses proofs to prove rust code correct.
  • Prop v0.42 released! Don't panic! The answer is... support for dependent types :)
    5 projects | /r/rust | 18 Jan 2023
    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
  • Linus Torvalds: Rust will go into Linux 6.1
    12 projects | /r/programming | 26 Sep 2022
    Easy reasoning does not end on memory safety. For example, deductive verification of Rust code is possible exactly because there's no reference aliasing in safe Rust
  • A personal list of Rust grievances
    11 projects | news.ycombinator.com | 12 Sep 2022
    > No support for using something like separation logic within Rust itself to verify that unsafe code upholds the invariants that the safe language expects.

    I think this is something we might see in the future. There are a lot of formal methods people who are interested in rust. Creusot in particular is pretty close to doing this - at least for simpler invariants

    https://github.com/xldenis/creusot

  • What it feels like when Rust saves your bacon
    2 projects | news.ycombinator.com | 24 Jun 2022
    You often encounter this entire thread of rhetoric when someone wants to put a diversion into the central argument, yeah but it doesn't ____.

    But Rust does do that, match exhaustiveness, forcing the handling of errors and the type system enables things like CreuSAT [1] using creusot [2]

    [1] https://news.ycombinator.com/item?id=31780128

    [2] https://github.com/xldenis/creusot

    > Creusot works by translating Rust code to WhyML, the verification and specification language of Why3. Users can then leverage the full power of Why3 to (semi)-automatically discharge the verification conditions!

    Units of Measure, https://github.com/iliekturtles/uom

    The base properties of the language enable things that can never be done in C++.

  • What Is Rust's Unsafe?
    5 projects | news.ycombinator.com | 10 Apr 2022
    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.

    5 projects | news.ycombinator.com | 10 Apr 2022
    > 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
    14 projects | news.ycombinator.com | 2 Feb 2022
    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
    11 projects | /r/rust | 18 Dec 2021
    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.
  • A note from our sponsor - SonarLint
    www.sonarlint.org | 25 Sep 2023
    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. Learn more →

Stats

Basic creusot repo stats
15
765
9.0
4 days ago
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.
www.influxdata.com