Kani Rust Verifier – a bit-precise model-checker for Rust | Hacker News Reader

Kani Rust Verifier – a bit-precise model-checker for Rust

model-checking.github.io

137 pointspabs312 comments

Nice, I just would have liked to get all these different verification tools combined under the same interface, just being different backends as drafted by the rust verification tools work of project oak: have "cargo verify" as common command and use common test annotations, allowing the same test to be verified with different backends or just fuzzed/proptested (see https://project-oak.github.io/rust-verification-tools/using-... and https://project-oak.github.io/rust-verification-tools/using-...).

The model checking 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 https://github.com/GaloisInc/crucible.

Overall I believe this space would benefit from more coordination and focus on developing something that has the theoretical foundations to cover as many needs as possible and then make a user-friendly tool out of it that is endorsed by the Rust project similar to how Rust analyzer is the one language server to come.

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

> “Overall I believe this space would benefit from more coordination and focus on developing something that has the theoretical foundations …”

The Ferrocene project is a coordinated effort I believe: https://ferrous-systems.com/ferrocene/

Looks like that the project has changed its name from "rmc" (Rust Model Checker) to this. Various sources point to rmc as https://github.com/model-checking/rmc (redirected to https://github.com/model-checking/kani) and https://model-checking.github.io/rmc/ (404). Anyone knows why?

Unfortunately, cbmc that it depends on is way too slow for analyzing more than tiny trivial functions.

who would thought that the "safe" system language rust needs a formal model checker, plus formal concurrences checkers (loom and shuttle). what about a type checker also? or maybe just redefine "safe", so that truly safe languages stand out a bit.

note that formal model checkers cannot prove termination, only memory and type safeties.

I guess a bit of sarcasm but nevertheless.

Excerpt from Kani doc : Kani is especially useful for verifying unsafe code in Rust.

and regarding loom and shuttle : Excerpt from The Rustonomicon : Safe Rust guarantees an absence of data races, which are defined as: 1) two or more threads concurrently accessing a location of memory 2) one or more of them is a write 3) one or more of them is unsynchronized However Rust does not prevent general race conditions. This is pretty fundamentally impossible, and probably honestly undesirable.

concurrency safety does exist. checkout such languages, you'll be surprised. pony latest, but also singularity or concurrent pascal. also all other safeties rust only promises cannot provide

Did you known that in its early days Rust did take a more Pony-like approach but as ownership/borrowing took shape it was obvious that it was more scalable to move that abstraction into libraries.

What safe mean is not that easy to define. From the Pony FAQ: Pony prevents data races. It can’t stop you from writing race conditions into your program.

Also keep in mind that Rust is not garbage collected, the guarantees Rust provide regarding safety are a huge step forward but of course a lot need to be done.

Those guarantees are not promises, they are formally proven : https://www.ralfj.de/research/thesis.html (https://www.eurekalert.org/news-releases/610682)

safe is trivial to define. all the safe languages defined and implemented it. with rust we are still waiting for those promises.

remember how eBPF was formally proven to be safe also? until meltdown came along and all those proofs fell down.

Ho well probem solved then. I wonder why people keep searching ;-)

With all due respect, you don’t know too much about this topic to have such a strong opinion.

There is no safe language, as that would imply the solution of Rice’s theorem, Halting problem, etc.

Reply on news.ycombinator.com