awesome-rust-formalized-reasoning VS kani

Unsurprisingly, we can see a growing interest in the Rust ecosystem regarding formal verification. I try to keep https://github.com/newca12/awesome-rust-formalized-reasoning up to date. I will add CreuSAT shortly.

This dispersed progress is the sign of an absence of maturity but the exploration of this space with Rust is very promising : https://github.com/newca12/awesome-rust-formalized-reasoning

> those applications need the proof for correctness so that more dangerous code---say, what would need `unsafe` in Rust---can be safely added

There are actually already tools built for this very purpose in Rust (see Kani [1] for instance).

Formal verification has a serious scaling problem, so forming programs in such a way that there are a few performance-critical areas that use unsafe routines seems like the best route. I feel like Rust leans into this paradigm with `unsafe` blocks.

[1] - https://github.com/model-checking/kani

You can also use Kani to check unsafe code. https://github.com/model-checking/kani

Here's a summary of what's new in version 0.28.0:

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.

kani (e.g. used by hifitime)

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).