agda-stdlib VS creusot

Compare agda-stdlib vs creusot and see what are their differences.

agda-stdlib

The Agda standard library (by agda)

creusot

deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications! (by xldenis)
Our great sponsors
  • Scout APM - Less time debugging, more time building
  • SonarLint - Deliver Cleaner and Safer Code - Right in Your IDE of Choice!
  • SaaSHub - Software Alternatives and Reviews
agda-stdlib creusot
2 7
441 304
2.0% -
8.8 9.5
8 days ago 3 days ago
Agda Rust
GNU General Public License v3.0 or later GNU Lesser General Public License v3.0 only
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
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.

agda-stdlib

Posts with mentions or reviews of agda-stdlib. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2022-04-27.

creusot

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 2022-04-10.
  • 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 | reddit.com/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.
  • Automatic Rust verification tools (2021)
    1 project | reddit.com/r/rust | 5 Jun 2021
    Found another one: https://github.com/xldenis/creusot
  • From Rust to SPARK: Formally Proven Bip-Buffers
    1 project | reddit.com/r/rust | 6 May 2021
    There's a couple prototypes already, such as Prusti or Creusot.
  • Safer Rust: Program Verification with Creusot [video]
    1 project | reddit.com/r/rust | 28 Mar 2021
    Project in github for those who don't have the time to watch the video: https://github.com/xldenis/creusot

What are some alternatives?

When comparing agda-stdlib and creusot you can also consider the following projects:

cryptominisat - An advanced SAT solver

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.

Daikon - Dynamic detection of likely invariants

agda-life - Conway's Game of Life in Agda.

l4v - seL4 specification and proofs

ed25519-dalek - Fast and efficient ed25519 signing and verification in Rust.

template-agda - An Agda template, configured for Gitpod (www.gitpod.io) to give you pre-built, ephemeral development environments in the cloud.

hacspec - A specification language for cryptography primitives.