4 ms·

Developing provably correct Rust code with Verus

2 points by Betelbuddy 1mo ago

sourdecor 29d ago
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 https://news.ycombinator.com/item?id=12357976
- japgolly 28d ago
  [dead]
- pjmlp 28d ago
  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.
  - igornotarobot 28d ago
    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.
  - kreneskyp 28d ago
    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 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.
    - pjmlp 27d ago
      Thanks for sharing, always like to learn about this stuff.
- jgalt212 28d ago
  > 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.
  - zozbot234 28d ago
    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.
  - digilypse 28d ago
    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.
    - jgalt212 27d ago
      > Isn’t the value in being able to verify the design before implementing? Fair enough, but to be truly safe you really need the whole pipeline connected. model -> validation -> emitted code.
kobahiro 29d ago
[flagged]
jdw64 28d ago
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?
- Jtsummers 28d ago
  https://verus-lang.github.io/verus/publications-and-projects/ 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/ 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_Overview.html# https://learn.adacore.com/courses/intro-to-spark/chapters/01... - Free tutorial for SPARK
  - jdw64 28d ago
    thanks!
- kite42 28d ago
  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.
  - anonymousDan 28d ago
    I like how they also neglected to mention that Verus was invented at Microsoft...
    - 28d ago
canadiantim 28d ago
This seems like a big deal
jongjong 28d ago
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.
- gr_norm 28d ago
  > 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-engine-formally-verifying-the-hypervisor-in-the-aws-nitro-system https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng....
- stevenhuang 28d ago
  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.
homarp 28d ago
see also https://lean-lang.org/use-cases/aeneas/ https://lean-lang.org/use-cases/aeneas/ https://github.com/AeneasVerif/aeneas https://github.com/AeneasVerif/aeneas (by Microsoft)
m00dy 28d ago
>>The result is fast code that's more correct and secure than average. Welcome to Rust
- Ohentis 27d ago
  I mean... rust alone doesn't have this feature. And many languages have a "slap z3 onto it" tool.
m00dy 28d ago
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.
m00dy 28d ago
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.
- gregwebs 28d ago
  They have separate machinery for concurrent code: https://verus-lang.github.io/verus/state_machines/intro.html https://verus-lang.github.io/verus/state_machines/intro.html
Meneth 28d ago
"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth.
nottorp 28d ago
Would it help with the bugs in the new and improved ubuntu coreutils?
- Betelbuddy 28d ago
  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...
  - nottorp 28d ago
    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 https://en.wikipedia.org/wiki/Rice%27s_theorem …
    - cmrx64 28d ago
      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.
      - svieira 28d ago
        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".
        nottorp 28d ago
lukeify 28d ago
Reminds me of Whiley, which was developed by one of my university professors.
bcjdjsndon 28d ago
> 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?
- ijustlovemath 28d ago
  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
  - bsaul 28d ago
    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.
  - bcjdjsndon 28d ago
    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.
    - Jtsummers 28d ago
      > 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.
    - ijustlovemath 28d ago
      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.
112233 28d ago
> 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?
- ijustlovemath 28d ago
  What exactly is your objection? Rust doesn't solve the halting problem? You can absolutely prove bounded resource use with eg SmallVec and arenas
  - 112233 28d ago
    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.
63 28d ago
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 https://github.com/rust-lang/miri [1]https://github.com/model-checking/kani https://github.com/model-checking/kani [2]https://github.com/creusot-rs/creusot https://github.com/creusot-rs/creusot
- gregwebs 28d ago
  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.
  - gregwebs 28d ago
    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.
MeetingsBrowser 28d ago
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!
- afdbcreid 28d ago
  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.
  - MeetingsBrowser 28d ago
    > 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.
    - rcxdude 28d ago
      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).
freethinky 28d ago
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).
- genxy 28d ago
  You might see if this nascent CLR backend to Rust can do what you need https://github.com/FractalFir/rustc_codegen_clr https://github.com/FractalFir/rustc_codegen_clr
reddit_clone 28d ago
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?)
- Jtsummers 28d ago
  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 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).

2 points by Betelbuddy 1mo ago

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 https://news.ycombinator.com/item?id=12357976

japgolly 28d ago
[dead]
pjmlp 28d ago
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.
- igornotarobot 28d ago
  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.
- kreneskyp 28d ago
  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 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.
  - pjmlp 27d ago
    Thanks for sharing, always like to learn about this stuff.
jgalt212 28d ago
> 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.
- zozbot234 28d ago
  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.
- digilypse 28d ago
  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.
  - jgalt212 27d ago
    > Isn’t the value in being able to verify the design before implementing? Fair enough, but to be truly safe you really need the whole pipeline connected. model -> validation -> emitted code.

kobahiro 29d ago

[flagged]

jdw64 28d ago

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?

Jtsummers 28d ago
https://verus-lang.github.io/verus/publications-and-projects/ 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/ 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_Overview.html# https://learn.adacore.com/courses/intro-to-spark/chapters/01... - Free tutorial for SPARK
- jdw64 28d ago
  thanks!
kite42 28d ago
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.
- anonymousDan 28d ago
  I like how they also neglected to mention that Verus was invented at Microsoft...
  - 28d ago

canadiantim 28d ago

This seems like a big deal

jongjong 28d ago

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.

gr_norm 28d ago
> 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-engine-formally-verifying-the-hypervisor-in-the-aws-nitro-system https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng....
stevenhuang 28d ago
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.

homarp 28d ago

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

m00dy 28d ago

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

Ohentis 27d ago
I mean... rust alone doesn't have this feature. And many languages have a "slap z3 onto it" tool.

m00dy 28d ago

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.

m00dy 28d ago

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.

gregwebs 28d ago
They have separate machinery for concurrent code: https://verus-lang.github.io/verus/state_machines/intro.html https://verus-lang.github.io/verus/state_machines/intro.html

Meneth 28d ago

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

nottorp 28d ago

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

Betelbuddy 28d ago
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...
- nottorp 28d ago
  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 https://en.wikipedia.org/wiki/Rice%27s_theorem …
  - cmrx64 28d ago
    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.
    - svieira 28d ago
      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".
      - nottorp 28d ago

lukeify 28d ago

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

bcjdjsndon 28d ago

> 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?

ijustlovemath 28d ago
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
- bsaul 28d ago
  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.
- bcjdjsndon 28d ago
  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.
  - Jtsummers 28d ago
    > 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.
  - ijustlovemath 28d ago
    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.

112233 28d ago

> 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?

ijustlovemath 28d ago
What exactly is your objection? Rust doesn't solve the halting problem? You can absolutely prove bounded resource use with eg SmallVec and arenas
- 112233 28d ago
  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.

63 28d ago

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 https://github.com/rust-lang/miri [1]https://github.com/model-checking/kani https://github.com/model-checking/kani [2]https://github.com/creusot-rs/creusot https://github.com/creusot-rs/creusot

gregwebs 28d ago
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.
- gregwebs 28d ago
  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.

MeetingsBrowser 28d ago

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!

afdbcreid 28d ago
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.
- MeetingsBrowser 28d ago
  > 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.
  - rcxdude 28d ago
    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).

freethinky 28d ago

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

genxy 28d ago
You might see if this nascent CLR backend to Rust can do what you need https://github.com/FractalFir/rustc_codegen_clr https://github.com/FractalFir/rustc_codegen_clr

reddit_clone 28d ago

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

Jtsummers 28d ago
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 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).