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.
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.
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.
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.
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 only thing you really need to check is the top-level annotations
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.
Thousands of people write and review code both professionally and as a hobby. But most people writing verifier annotations have a PhD in some field adjacent to formal verification.
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.
Programmer intends to write code that does Y, but writes code that does X. Then they make the same mistake again and write an annotation that verifies the function does X.
Verification passes, but the code does the wrong thing.
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).
It will prove the bugs were corrected implemented... :-) And that your mistaken specification 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...and that your wrong logic about how much centrifugal force your rocket will be able to stand on ascent was mathematically translated to proven correct code running the incorrect logic...
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.
any of the quite many cost-aware logical frameworks. it’s SO. easy. to. do. you fools are just willfully ignorant on how to represent reasoning, despite alleging yourselves to be computer scientists?
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.
> You are trying to convince me that because you pressed "A" once on the vending machine and worked, you declare "A" is proven to dispense Coke...
This thread is hilarious, thank you. You start off saying you "cant [sic] stand formal methods people" and now you're giving an example of why formal methods are useful. And you're appealing to authority using a man who was a major proponent of formal methods. What's your actual position on formal methods?
The quote from Dijkstra stands on its own...quoting a famous person stating something independently demonstrable, does not magically turn the statement into an appeal to authority :-))
>> a man who was a major proponent of formal methods.
No he was not, but you see, its irrelevant in the context of the argument you failed to defend. And Dijkstra fails your purity test.
He himself wrote that he saw "no specific virtue in being a formalist" and would use formal methods "when I feel they help."
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.
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).
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?
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.
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'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
That's indeed a weird feeling when going back to another language after having coded in rust. First you're happy not having to write any "unsafe" keyword. Then you're horrified for the very same reason.
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.
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.
> 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.
That means when one goes out of whack, someone will notice. E.g. let's say the mathematical property is correct, but someone optimizes some behavior. Without tests or verification that could break production or worse: not break it, but break security without anybody noticing.
> 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.
> 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?
Objection was against "memory safety" somehow having become "safety". Here is an epic tool that allows one to attach and formally prove assertions. Genuinely impressive and massively useful.
Yet the pitch is that it is needed for the "unsafe" unsafe code, to make it "safe". Not for all code, to make all code safe.
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
Miri: proves pre-defined properties, no changes to code other than adding a few annotations
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.
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.
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
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.
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.
Thanks for sharing, always like to learn about this stuff.
> 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.
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!
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 only thing you really need to check is the top-level annotations
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.
Thousands of people write and review code both professionally and as a hobby. But most people writing verifier annotations have a PhD in some field adjacent to formal verification.
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).
> the propositions actually correlate with what people actually want out of the system
My point is that this is the hard part, and writing annotations does nothing to help with this problem.
To me it seems easier than proving the code does something useful without pinning down what that actually is.
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.
Sorry I’ll try to put it simply.
Programmer intends to write code that does Y, but writes code that does X. Then they make the same mistake again and write an annotation that verifies the function does X.
Verification passes, but the code does the wrong thing.
I think it provides best bang for buck when the annotation is "obviously correct" but the implementation is complex.
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.
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).
You might see if this nascent CLR backend to Rust can do what you need https://github.com/FractalFir/rustc_codegen_clr
Would it help with the bugs in the new and improved ubuntu coreutils?
It will prove the bugs were corrected implemented... :-) And that your mistaken specification 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...and that your wrong logic about how much centrifugal force your rocket will be able to stand on ascent was mathematically translated to proven correct code running the incorrect logic...
Jesus, I cant stand formal methods people...
I was picking mostly on the rust religion at first. But then I looked things up and ran into https://en.wikipedia.org/wiki/Rice%27s_theorem …
naive applications of this would lead you to believe no knowledge is possible, and that progress is not meaningful when liveness can’t be guaranteed.
it’s all rubbish, grandparent is a small mind who can’t figure out how it’s a step up from nothing.
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.
What formal correctness proof will detect that?
any of the quite many cost-aware logical frameworks. it’s SO. easy. to. do. you fools are just willfully ignorant on how to represent reasoning, despite alleging yourselves to be computer scientists?
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
Testers are not selling guarantees...
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.
Oh my my...
"Program testing can be used to show the presence of bugs, but never to show their absence"
Ah, but you can't stand those formal methods folks, why are you appealing to authority with Edsger Dijkstra?
You are trying to convince me that because you pressed "A" once on the vending machine and worked, you declare "A" is proven to dispense Coke...
> You are trying to convince me that because you pressed "A" once on the vending machine and worked, you declare "A" is proven to dispense Coke...
This thread is hilarious, thank you. You start off saying you "cant [sic] stand formal methods people" and now you're giving an example of why formal methods are useful. And you're appealing to authority using a man who was a major proponent of formal methods. What's your actual position on formal methods?
Have you considered a career is stand up comedy?
The quote from Dijkstra stands on its own...quoting a famous person stating something independently demonstrable, does not magically turn the statement into an appeal to authority :-))
>> a man who was a major proponent of formal methods.
No he was not, but you see, its irrelevant in the context of the argument you failed to defend. And Dijkstra fails your purity test.
He himself wrote that he saw "no specific virtue in being a formalist" and would use formal methods "when I feel they help."
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.
see also https://lean-lang.org/use-cases/aeneas/ https://github.com/AeneasVerif/aeneas (by Microsoft)
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?)
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.
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).
Reminds me of Whiley, which was developed by one of my university professors.
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.
https://mitpress.mit.edu/9780262546232/program-proofs/ - Dafny book, pretty good tutorial on the topic
https://learn.adacore.com/courses/intro-to-spark/chapters/01... - Free tutorial for SPARK
thanks!
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.
I like how they also neglected to mention that Verus was invented at Microsoft...
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?
This seems like a big deal
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.
They have separate machinery for concurrent code: https://verus-lang.github.io/verus/state_machines/intro.html
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.
>>The result is fast code that's more correct and secure than average.
Welcome to Rust
> 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?
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
That's indeed a weird feeling when going back to another language after having coded in rust. First you're happy not having to write any "unsafe" keyword. Then you're horrified for the very same reason.
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.
Because Rust is not Verus, and not all unsafe code needs formal-verification-level of rigorousness. Also, there are other verifiers as well.
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.
> 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....
So it moves from both "my implementation and specification is incorrect", to just "my specification is incorrect".
I don't understand this type of thinking. Proving what you can is still better. Don't let perfect be the enemy of good.
>> 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.
That means when one goes out of whack, someone will notice. E.g. let's say the mathematical property is correct, but someone optimizes some behavior. Without tests or verification that could break production or worse: not break it, but break security without anybody noticing.
That is worth the hassle for some applications.
> 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.
"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?
What exactly is your objection? Rust doesn't solve the halting problem? You can absolutely prove bounded resource use with eg SmallVec and arenas
Objection was against "memory safety" somehow having become "safety". Here is an epic tool that allows one to attach and formally prove assertions. Genuinely impressive and massively useful.
Yet the pitch is that it is needed for the "unsafe" unsafe code, to make it "safe". Not for all code, to make all code safe.