Verus seems to be exactly what I have been looking for! I discovered AllConcur[0] on HN a while back, and I wanted to port it to Go, but since it used TLA+ and C, and it was very confusing for me to understand how you can trust the implementation unless you can compile TLA+ to C.

I was talking to Gemini about comparing Verus to TLA+ and it said that TLA+ is usually used (for example) "to prove that a distributed consensus protocol is logically sound" but when I asked if Verus can do that too, it said yes. So Verus can be compiled and integrated with Rust, whereas TLA+ is used more for blueprint development that then guides the implementation in the mind of the implementer.

Seems awesome!

[0]: https://news.ycombinator.com/item?id=12357976

If you found this interesting, you may also be interested to hear about some related projects with similar goals/scopes: Miri[0], Kani[1], and Creusot[2]. There looks to be some significant overlap between Verus, Kani, and Creusot but I've not used any of them so I'll refrain from trying to differentiate them.

[0]https://github.com/rust-lang/miri

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

[2]https://github.com/creusot-rs/creusot

That's fascinating. Does it mean it verifies mathematical proofs directly within the Rust code? Does anyone know the underlying principles of how this is possible?

I have long been critical of verification tools requiring annotations. Humans cannot write correct code, so asking them to write correct proof annotations seems futile.

But maybe this changes in the age of LLMs. A deterministic check to let LLMs verify the correctness of an API could improve the success rate of large scale refactors or performance optimizations.

Exciting!

Does anyone now if something like this exist and is used (and actively maintained) for .NET/C#, not like Dafny where I write in another language (unlikely my company would allow that). Also as annotations (likely that I can start with it).

Ive been using Rust with LLMs for the past 2 years already. It's just amazing, I can't really think anything else to code with. Normally, been testing my codes unit tests + integration tests where necessary. But, I will take a look at this seriously.

Would it help with the bugs in the new and improved ubuntu coreutils?

I just read the whole thing, the post would be even better if it includes an example for concurrency. It's not easy to imagine it just by looking at the binary search's example.

see also https://lean-lang.org/use-cases/aeneas/ https://github.com/AeneasVerif/aeneas (by Microsoft)

Reminds me of Whiley, which was developed by one of my university professors.

This seems like a big deal

This is very interesting.

I am new to Rust and also new to formal verification.

Can someone ELI5 this for me?

(Also, when does the proof happen? During compilation or by running extra tests during unit testing?)

> With Verus, however, developers can mathematically prove the safety of their unsafe Rust code, re-establishing machine-checked safety guarantees

Why then does rust even need the unsafe keyword?

>>The result is fast code that's more correct and secure than average.

Welcome to Rust

[flagged]

What if the 'mathematical specification of its functionality' is incorrect? How to prove the correctness of the mathematical specification faster than the underlying environment, code and dependencies change?

IMO, formal verification is never going to work. It's very clear that a lot of people are desperate to see it used in mainstream software development, but every innovation which proponents have seen as an opportunity to finally prove its utility has only served to further discredit it.

Now proponents are at a point that they literally have to convince us that people who aren't able to write correct code are somehow able to write correct mathematical specifications!

This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself... And every experienced software engineer knows that mistakes grow proportionally to the size of the logic... Unfortunately, mathematical spec is logic; just like code, except it's more complex and thus more error-prone.

And don't even get me started on the fact that APIs, engines and languages change constantly from under you and thus the mathematical spec would get completely invalidated every week or so each time you did an update. Unfortunately, even in the best case scenario, reality is always going to change and invalidate our proofs faster than we can publish them. By the time you've proven the theory, its underlying assumptions already ceased to hold true.

Even in a far simpler hypothetical world with just one piece of software; the software's own execution could potentially change the reality which it relied on to prove its own correctness and would thus invalidate its own correctness merely by executing.

"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth.

> With Verus, however, developers can mathematically prove the safety of their unsafe Rust code

what about proving safety of not-unsafe code? The meme that rust is "safe" is becoming tiring. Does this thing allow proving absence of infinite loops? Bounded resource use? Correctness of comparison operations? Etc.

Also, why is there still no hardware tagging to simply prevent memory misuse at cpu level, if it actually is such an important issue?