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.
That is my pet peeve against TLA+ advocacy, the disassociation between a theoretical proof of a specific algorithm, data structures, and the actual implementation in production.
I rather push for tooling that allows code generation based on the formal proofs like FStart or Dafny, or is integrated with specific programming languages like SPARK, Frama-C or this Verus.
You can write everything in Lean and generate an implementation. Given that LLMs can now generate Lean proofs, this does not seem to be prohibitively expensive anymore. The real issue with distributed algorithms is that they are hard to reason about, and reasoning about them at the code level does not make the verification problem easier, it makes it harder.
I'm working on a ISO-29148 aligned spec standard with formal modelling baked in. It's meant to sit above the code with types, contracts, proofs and other objects that lower mechanically into code and/or are deterministically verified.
I'm targeting Rust primarily but my goal is that any language could sit under it via an integration layer.
The first public version of the formal specification standard isn't available yet. Pushing hard to get it out soon! But Quoin ships with an earlier version of the spec standard. It features derived property tests, which was the POC for fully adopting a formal-spec-to-derived-formal-verification ecosystem.
> as very confusing for me to understand how you can trust the implementation unless you can compile TLA+ to C.
Preach. I feel like I'm taking crazy pills every time someone claims TLA+ as the sine qua non of provably correct systems. They should sub probably for provably.
There is no contradiction here, TLA+ is mostly about proving properties of toy models, not end-to-end proofs about real programs. As TLA+ practitioners like to point out, the latter is only applicable to favorable "local" properties - this is what type systems do, they state claims that are quite aligned with the program's syntactic structure; or else to rather trivial programs where proving "whole-program" claims is still feasible. Even Verus itself doesn't really change this.
Isn’t the value in being able to verify the design before implementing? It would be more ideal surely to prove correctness of the deployed code, but I still find it very useful.
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?
https://verus-lang.github.io/verus/publications-and-projects... - The papers here go into their implementation. They take the proof statements and information about the program and turn it into an SMT problem (and run it through Z3 if I read correctly) and then they use that to prove the properties of the program.
SPARK/Ada and Dafny work similarly, and have good documentation if you want to try your hand at something with a (presently) better set of documentation.
All it does is dispatch proof obligations to an SMT solver like Z3. There is nothing special about Verus, it works in the same way other program verification frameworks like Dafny and Frama-C work - except it's for Rust.
Most of this article presents nothing unique to Verus and is more of an advertisement for the authors research work and the other work AWS is doing.
Not the first time Microsoft employees invented a formal methods tool, Microsoft ignored them, and AWS scooped them up. Not the second or third time, either.
I don't think it's entirely fair to say they ignored them. As far as I know they are still employed at Microsoft Research and working on developing and improving the tool?
What if the mathematical specification of its functionality is wrong?
IMO, formal verification is never going to work. It's very clear that a lot of people are desperate to see it working, 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.
> How to prove the correctness of the mathematical specification?
You can show that your specifications satisfy well-accepted criteria like confidentiality and integrity. This is usually done as the final verification step. For example, AWS just did it for the Nitro hypervisor used by EC2: https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng....
I feel like the exact same line could be used to argue the opposite point against formal verification.
I'm not saying that proof is inherently bad. If it was free, then I agree it would be good, but my point is that it's not free. Proofs are expensive to produce, maintain, they lock-down flawed implementations, focus on correctness but disregard more important aspects like modularity (I.e. loose coupling, high cohesion). Also; formal proofs discourage change and they create false confidence about reliability because sometimes the bug is in the spec itself, especially as the spec gets more complicated.
I think modularity is a more useful property to aim for in terms of achieving the right degree of correctness over the life of the software, in a practical sense.
Formal proofs can work against modularity if the proof must be rewritten in order to achieve modularity as requirements change over time; which is the reality for most software.
> people who aren't able to write correct code are somehow able to write correct mathematical specifications
This describes about one or two thirds of the Theoretical CS academic community (conservative estimate) /s
> This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself
I find this hard to believe. The mathematical specification for "array a is sorted" is "forall n in Nat: 0 < n < len(a) -> a[n] >= a[n+1]". The average sorting algorithm is usually a tad longer than this.
> the mathematical spec would get completely invalidated every week or so each time you did an update
Well of course nobody serious advocates for formalizing/verifying code that is subject to that much churn (be it internal or external).
Nothing forces developers to write a complete specification of the algorithm. You want to have it both ways.
If developers keep the spec concise but incomplete, then you say the spec is incorrect so now you have to prove that the spec is correct. Ok, but people already use unit tests to sample the behaviour of a function so they already accept some degree of inaccuracy. By your logic you have to enumerate the entire input space otherwise unit testing is worthless.
If developers decide to build a complete specification of the algorithm, you counter that the specification is now too long so they should not bother.
You are basically arguing with yourself.
The update argument doesn't make sense either, because you generally want to prove properties like absence of panics throughout your entire codebase. Again this is just a roundabout way of arguing against the very idea of a tradeoff.
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.
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.
It will prove the bugs were corrected implemented... :-) And that your mistaken specialization of the tax rules in Switzerland, was correctly translated to code, and that your mistaken specification of the process to request a mortgage is mathematically valid...
I wouldn't say it's all rubbish - it's very easy for someone new to theorem proving to presume the equivalent of "strong typing will eliminate the possibility of errors", but the more correct understanding is "strong typing will reduce the number of things you have to keep in your head at any one time thus reducing the possibility of errors".
The thing with ubuntu's rust coreutils is that they, for example, crash when told to recurse because they use actual recursive calls to go into subdirs and run out of stack space if the structure is big enough.
I presume you also can't stand people who write software tests for similar reasons? The test is wrong, the code is wrong. The spec is wrong, the code is wrong. What a waste of effort! Just write correct code people! Verification is left as an exercise for the end users. Who cares about them anyways? /s
That's exactly what testers are selling though. If they aren't guaranteeing the program is correct (up to what is tested) then what purpose do they serve? Same with formal methods, offering guarantees up to what is proven.
Tests are guaranteeing that the product doesn't fail under the test conditions. Formal verification is guaranteeing the product doesn't deviate from the formal spec under a given set of assumptions. Both of them are useful but depend on how well the thing being checked actually correlates with what you care about.
Interesting definition of guarantee....what about the people who run millions of them? Well Microsoft: "AS IS." Apple: "WITH ALL FAULTS" Adobe: "no guarantee of error-free operation."
Apparently their lawyers never got the memo that the tests already guaranteed the software...
Well yeah, why would they offer an legal guarantee if they don't have to? They could have a watertight proof that their software works perfectly in all situations (lol) but the lawyers still would prefer to disclaim as much liability as possible.
And even if they did, all the test guarantee is that the tests pass, of course the main limit is that they don't actually test even a small fraction of what the customers actually want to do.
I'd rather have all the unsafe code scoped and the safety invariants explained than the alternative. You still can't do a whole class of scary things in an unsafe block; common misconception
Yeah but if this program can prove unsafe code is safe... Why can't rust compiler do it, and hence, why do we even need unsafe if the compiler can do it.
> Yeah but if this program can prove unsafe code is safe... Why can't rust compiler do it
This question only makes sense if you think Verus is part of the Rust compiler. It's not. And even if it were, the additional annotations are still required to prove that the unsafe block is actually safe. So this could, if integrated into the Rust compiler, help programmers eliminate some unsafe blocks (perhaps even most), but likely not all, and not without additional code proving that the section is safe.
It generates additional code that's fed into an SMT solver. Poor compiler performance is a top issue developers have with Rust, which they're working to solve. I think adding this layer into every piece of code (which is probably impossible since inferring the invariants is essentially inferring your business logic) would eat away gains they've achieved.
I also think the functional style, typestate, and borrow checker is enough for writing correct code across many business domains, so there's no need to add this to your toolchain. We are a med device company building a class III (really 3 class II) device, and Verus is making our verification story extremely compelling.
There's a huge difference between "Verus can prove the safety of unsafe code" and "Verus can EASILY prove the safety of unsafe code." And I bet it can't prove everything, like calls to a C ABI.
> 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?
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.
AI tells me that code using the verus! macro everywhere would double in build time but if only used ocassionally the verus! macro would only increase build time by a few percent. The attribute annotation would basically be free, but there is a downside that loop invariants would be rejected by stable rustc.
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. Having a nice deterministic way to let LLMs verify that an API is "correct" might let them do larger scale reactors or performance optimizations.
You seem to have misunderstood the idea. The entire idea of proof annotations is that they are not manual. Rather, the verifier checks you fulfill the preconditions for the method you calls, and it checks inside the method that if the preconditions are fulfilled then the postconditions are too. This just helps the verifier reason locally. At the end besides more burden, the only thing you really need to check is the top-level annotations, like any formal verifier.
the vast majority of such annotations are checked though. There's generally three kinds of annotations in formal proof systems: assertions about inputs that cannot be checked by the system, statements of propositions that want to be checked, and proofs that those propositions follow from the assertions. The proofs are checked by the system, so writing them is mainly just tedious and difficult, not really a source of error. What needs to be verified carefully is that the assertions are true, and that the propositions actually correlate with what people actually want out of the system. The mark of how effective a formal verification system is is in how strong of a proposition can be proven from how small a set of assertions. (well, and then how difficult it is to write the proofs).
You were clear, and you were wrong. The annotations are checked like I said, you cannot break the guarantees using them. If they're incorrect they won't pass verification. They just help the verifier.
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).
Proof happens before compilation, and doesn't require compilation. You can follow the Verus tutorials for the specifics, but you can use it as a standalone verifier or as a compilation "stage" where it'll run its verification and then conditionally continue on to compilation.
But if you want a more complete tutorial on this concept using similar tools (so what you learn from them will transfer well to Verus, even if you need to learn Verus or Rust specific details) check out Dafny or SPARK/Ada. The latter is mature and used in some parts of the software industry today. The former, I don't know if anyone actually uses it in production though theoretically you can (it generates code in several languages, I have not used it for that myself, just in an instructional capacity).
66 comments
[ 4.2 ms ] story [ 54.0 ms ] threadI 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.
Seems awesome!
[0]: https://news.ycombinator.com/item?id=12357976
I rather push for tooling that allows code generation based on the formal proofs like FStart or Dafny, or is integrated with specific programming languages like SPARK, Frama-C or this Verus.
I'm targeting Rust primarily but my goal is that any language could sit under it via an integration layer.
https://github.com/agent-ix/quoin
The first public version of the formal specification standard isn't available yet. Pushing hard to get it out soon! But Quoin ships with an earlier version of the spec standard. It features derived property tests, which was the POC for fully adopting a formal-spec-to-derived-formal-verification ecosystem.
Preach. I feel like I'm taking crazy pills every time someone claims TLA+ as the sine qua non of provably correct systems. They should sub probably for provably.
SPARK/Ada and Dafny work similarly, and have good documentation if you want to try your hand at something with a (presently) better set of documentation.
IMO, formal verification is never going to work. It's very clear that a lot of people are desperate to see it working, 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.
You can show that your specifications satisfy well-accepted criteria like confidentiality and integrity. This is usually done as the final verification step. For example, AWS just did it for the Nitro hypervisor used by EC2: https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng....
I don't understand this type of thinking. Proving what you can is still better. Don't let perfect be the enemy of good.
I feel like the exact same line could be used to argue the opposite point against formal verification.
I'm not saying that proof is inherently bad. If it was free, then I agree it would be good, but my point is that it's not free. Proofs are expensive to produce, maintain, they lock-down flawed implementations, focus on correctness but disregard more important aspects like modularity (I.e. loose coupling, high cohesion). Also; formal proofs discourage change and they create false confidence about reliability because sometimes the bug is in the spec itself, especially as the spec gets more complicated.
I think modularity is a more useful property to aim for in terms of achieving the right degree of correctness over the life of the software, in a practical sense.
Formal proofs can work against modularity if the proof must be rewritten in order to achieve modularity as requirements change over time; which is the reality for most software.
This describes about one or two thirds of the Theoretical CS academic community (conservative estimate) /s
> This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself
I find this hard to believe. The mathematical specification for "array a is sorted" is "forall n in Nat: 0 < n < len(a) -> a[n] >= a[n+1]". The average sorting algorithm is usually a tad longer than this.
> the mathematical spec would get completely invalidated every week or so each time you did an update
Well of course nobody serious advocates for formalizing/verifying code that is subject to that much churn (be it internal or external).
If developers keep the spec concise but incomplete, then you say the spec is incorrect so now you have to prove that the spec is correct. Ok, but people already use unit tests to sample the behaviour of a function so they already accept some degree of inaccuracy. By your logic you have to enumerate the entire input space otherwise unit testing is worthless.
If developers decide to build a complete specification of the algorithm, you counter that the specification is now too long so they should not bother.
You are basically arguing with yourself.
The update argument doesn't make sense either, because you generally want to prove properties like absence of panics throughout your entire codebase. Again this is just a roundabout way of arguing against the very idea of a tradeoff.
Welcome to Rust
Jesus, I cant stand formal methods people...
it’s all rubbish, grandparent is a small mind who can’t figure out how it’s a step up from nothing.
What formal correctness proof will detect that?
"Program testing can be used to show the presence of bugs, but never to show their absence"
Apparently their lawyers never got the memo that the tests already guaranteed the software...
And even if they did, all the test guarantee is that the tests pass, of course the main limit is that they don't actually test even a small fraction of what the customers actually want to do.
Why then does rust even need the unsafe keyword?
This question only makes sense if you think Verus is part of the Rust compiler. It's not. And even if it were, the additional annotations are still required to prove that the unsafe block is actually safe. So this could, if integrated into the Rust compiler, help programmers eliminate some unsafe blocks (perhaps even most), but likely not all, and not without additional code proving that the section is safe.
I also think the functional style, typestate, and borrow checker is enough for writing correct code across many business domains, so there's no need to add this to your toolchain. We are a med device company building a class III (really 3 class II) device, and Verus is making our verification story extremely compelling.
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?
[0]https://github.com/rust-lang/miri
[1]https://github.com/model-checking/kani
[2]https://github.com/creusot-rs/creusot
Kani: use in a test suite
Creusot: annotations
Verus: annotations or macro
The macro system looks very nice if it doesn't slow down the normal build.
But maybe this changes in the age of LLMs. Having a nice deterministic way to let LLMs verify that an API is "correct" might let them do larger scale reactors or performance optimizations.
Exciting!
Sorry if I wasn’t clear.
My point is that the annotations are manual and inherently prone to error.
If humans could correctly write annotations according to a spec, we wouldn’t need verifiers at all. We could just write correct code directly.
There is an argument to be made that the annotations are a smaller surface than full blown code and therefore easier for humans to reason about.
However, in practice formal verification tools and annotations are far more obscure than regular code.
Most people writing annotations have a PhD in some field adjacent to formal verification.
For example if you are trying to prove that your new sorting algorithm yields sorted list for all inputs.
If there is as much annotations as there is code, then testing is better tool for the job than verification.
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?)
Their tutorial seems ok: https://verus-lang.github.io/verus/guide/overview.html
But if you want a more complete tutorial on this concept using similar tools (so what you learn from them will transfer well to Verus, even if you need to learn Verus or Rust specific details) check out Dafny or SPARK/Ada. The latter is mature and used in some parts of the software industry today. The former, I don't know if anyone actually uses it in production though theoretically you can (it generates code in several languages, I have not used it for that myself, just in an instructional capacity).