10 ms·

Verified Rust for low-level systems code

284 points by gz09 2y ago

jimsimmons 2y ago
What exactly do SMT systems "solve" in cases like this? If I wrote a simple BFS or DFS and enumerated the search space how far would I get.. Is that not what TLA+ does in principle. I am surprised people prefer having a dependency of something like Z3 at compiler level.
- IshKebab 2y ago
  They try to find a counter-example to the constraints you have set up, or tell you that no such counter-example exists, in which case your program is correct. The counter-example is in the form of inputs to your program or function. It looks like the TLA+ Proof System does the same thing, but I believe you can also use TLA+ in "brute force all the states" mode. I haven't actually used it.
- sunshowers 2y ago
  SAT is an NP-complete problem. Doing an exhaustive search is very time-consuming. An SMT or SAT solver uses heuristics to make that process quicker for practical problems. It looks like there are some TLA+ implementations that do use SMT solvers under the hood.
- tkz1312 2y ago
  SMT solvers use a decision procedure known as CDCL(T). This uses a SAT solver at the core, which operates only on the core propositional structure of the input formula, and dispatches higher level constructs (e.g. functions, arrays, arithmetic) to specialized theory specific solvers. This is an extension of the CDCL (conflict driven clause learning) approach to SAT solving, which is a heuristic approach that uses information discovered about the structure of the problem to reduce the search space as it progresses. At a high level: 1. assign true or false to a random value 2. propagate all implications 3. if a conflict is discovered (i.e. a variable is implied to be both true and false): 1. analyze the implication graph and find the assignments that implied the conflict 2. Add a new constraint with the negation of the assignment that caused the conflict 3. backtrack until before the first assignment involved in the conflict was made The theory specific solvers use a diverse set of decision procedures specialized to their domain. The “Decision Procedures” book is an excellent overview: http://www.decision-procedures.org/ http://www.decision-procedures.org/
- oggy 2y ago
  TLA+ has also had an SMT-based backend, Apalache [1], for a few years now. In general, you encode your system model (which would be the Rust functions for Verus, the TLA model for Apalache) and your desired properties into an SMT formula, and you let the solver have a go at it. The deal is that the SMT language is quite expressive, which makes such encodings... not easy, but not impossible. And after you're done with it, you can leverage all the existing solvers that people have built. While there is a series of "standard" techniques for encoding particular program languages features into SMT (e.g., handling higher-order functions, which SMT solves don't handle natively), the details of how you encode the model/properties are extremely specific to each formalism, and you need to be very careful to ensure that the encoding is sound. You'd need to go and read the relevant papers to see how this is done. [1]: https://apalache.informal.systems https://apalache.informal.systems
IshKebab 2y ago
Interesting! Looks most similar to Creusot. The syntax is definitely nicer but wrapping your entire code in a macro surely is going to upset rust-analyzer?
- tsujamin 2y ago
  I’m not sure how rust-analyser works, but presumably you’d make the macro a no-op and just return the original tokens in debug builds
- jaybosamiya 2y ago
  A fork of rust-analyzer, called verus-analyzer, provides support for Verus syntax and actions (including new proof-specific actions) https://github.com/verus-lang/verus-analyzer/ https://github.com/verus-lang/verus-analyzer/
sdsd 2y ago
Noob question from someone with little real CS experience, when the README for this project says: > verifying the correctness of code What is the difference between "verifying" the correctness of code, as they say here, vs "proving" the correctness of code, as I sometimes see said elsewhere? Also, is there a good learning resource on "proving" things about code for working programmers without a strong CS / math background? Edit: I'm also very curious why "zero knowledge" proofs are so significant, and why this is so relevant. Eg I heard people talking about this and don't really understand why it's so cool: x.com/ZorpZK
- dumbo-octopus 2y ago
  Verifying and proving are used synonymously, as made clear later in the opening paragraph. As for zero knowledge proofs, there is little practical use, significance, or relevance to them due to the overhead involved and the lack of a "killer app", so to speak. But they're conceptually interesting.
  - vlovich123 2y ago
    Whenever I hear people talk about the lack of practicality of some mathematical construct, I always remember G H Hardy who worked on number theory at the turn of the century. One of his famous quotes I love is: > I have never done anything 'useful.' No discovery of mine has made, or is likely to make, directly or indirectly, for good or ill, the least difference to the amenity of the world. Despite his self-proclaimed focus on pure mathematics, Hardy's work, particularly in number theory, has had profound applications in cryptography and other fields. I agree about the overhead. The costs have come down significantly already but they still remain a few orders of magnitude too large. That being said, it’s killer app is cloud compute. Right now the only way to amortize the cost of HW is to run it on someone else’s computer, which brings along with it all sorts of security and privacy risks. Well-performing ZK proofs (which we don’t know if it exists / it may be a long time before we figure out how to do it) would let you do cloud computing securely without worrying about vulnerabilities in your cloud provider’s network. Like all cryptography, it’s a double-edged sword because the same techniques would let websites deliver code for your machine to execute that you have no knowledge of what it’s doing.
dist1ll 2y ago
One of the main contributors gave an excellent talk [0] on Verus at the Rust meetup in Zürich. I was really impressed how clean this "ghost" code fits into programs (reminded me a bit of Ada). [0] https://www.youtube.com/watch?v=ZZTk-zS4ZCY https://www.youtube.com/watch?v=ZZTk-zS4ZCY
TachyonicBytes 2y ago
Is there any relationship between this and Kani[1]? Do they work differently? [1] https://github.com/model-checking/kani https://github.com/model-checking/kani
- mmoskal 2y ago
  Model checkers typically only explore a bounded number of states which is efficient at bug finding and often doesn't require additional annotations in the program. Automatic (SMT-based) verifiers like Verus, Dafny, F* (and my VCC :) require you to annotate most every function and loop but give you broad guarantees about the correctness of the program. Tools based on interactive provers (like Coq or Lean) typically require more guidance from the user but can guarantee even more complex properties.
im3w1l 2y ago
This looks really cool. One thing I think would be really useful for people is some instructions / examples of how to add proofs for an existing codebase. So maybe an example could be a bare-bones gui app with a single textbox, that does an http request to some resource (having data that is unknown at compile-time and potentially untrusted is a very common thing) and fetches an array, which is bubble-sorted and displayed in the box. The bubble sort has some intentional bug (maybe due to some off by one error, the last element remains untouched). There are unit-tests that somehow don't trigger the bug (worrying that your tests are incomplete would be a primary motivator to go for proofs). It could then show how to replace the unit tests with a proof, in the process discovering the bug and fixing it. The example wouldn't need to go into huge detail about the proof code itself as it is potentially advanced, instead it would focus on the nitty-gritty details of adding the proof, like how the interface between proved mathematical code and non-proved io code works, what command line to run to prove&build, and finally a zip archive with all of that, that you can play around with. Edit: Actually just reading from stdin and writing to stdout is probably good enough.
ComputerGuru 2y ago
For those that are interested but perhaps not aware of this similar project, Dafny is a "verification-aware programming language" that can compile to rust: https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny
- algorithmsRcool 2y ago
  Always cool to see Dafny mentioned! Shameless plug: I just wrote a beginner's introduction to Dafny a few days ago. https://www.linkedin.com/pulse/getting-started-dafny-your-first-formal-proof-alfred-white-puucc/ https://www.linkedin.com/pulse/getting-started-dafny-your-fi...
jph 2y ago
If you want a small stepping stone toward Versus, you can add Rust debug_assert for preconditions and postconditions; the Rust compiler strips these out of production builds by default. Example from the Versus tutorial with verification: fn octuple(x1: i8) -> (x8: i8) requires -16 <= x1, x1 < 16, ensures x8 == 8 * x1, { let x2 = x1 + x1; let x4 = x2 + x2; x4 + x4 } Example using debug_assert with runtime checks: fn octuple(x1: i8) -> i8 { debug_assert(-16 <= x1); debug_assert(x1 < 16); let x2 = x1 + x1; let x4 = x2 + x2; let x8 = x4 + x4; debug_assert(x8 == 8 * x1); x8 }
- diarrhea 2y ago
  I wish more people used asserts like that. Such a wonderful tool for documentation. It complements the type system and testing really well.
- zozbot234 2y ago
  One issue with the existing Verus syntax is that it requires wrapping the whole code in a proc-macro. Other Rust proof/verification/DbC tools such as Creusot use attribute-based syntax instead, which generally seems to be a bit more lightweight and idiomatic for Rust. Hopefully it will become available in future Verus releases.
- lkrubner 2y ago
  Your Versus example is how I write my Clojure code, with post and pre conditions on most of the functions. And the JVM has a flag that makes it easy to strip that out for production builds.
- thesuperbigfrog 2y ago
  You could also try the "contracts" crate: https://docs.rs/contracts/latest/contracts/ https://docs.rs/contracts/latest/contracts/
  - nextaccountic 2y ago
    and you can use MIRAI, that takes the contracts defined by this crate and check them at compile time or, use prusti, that has contracts with a similar syntax checked at compile time as well
lsuresh 2y ago
We've used Verus to write formally verified Kubernetes controllers. Basically, we can prove liveness properties of the form "eventually, the controller will reconcile the cluster to the requested desired state". As you can imagine, there is a lot of subtlety and nuance to even specifying correctness here (think rapid changes to the desired state requirement, asynchrony, failures and what not). Code: https://github.com/vmware-research/verifiable-controllers/ https://github.com/vmware-research/verifiable-controllers/, with a corresponding paper due to appear at OSDI 2024.
- Thaxll 2y ago
  What does it do more than unit tests?
  - lsuresh 2y ago
    Full-system verification is more powerful than unit tests. You can prove an implementation of a distributed system is free of entire classes of bugs, modulo your specification. The reason is that there is simply no way to practically write tests to cover enough out of all possible executions of a distributed system. Think arbitrary interleavings of message arrivals, failures, restarts and events affecting every single entity in the distributed system. We built a framework on top of Verus (called Anvil) that allowed us to write a top-level specifications of the form "If the ZooKeeper operator says it can reconcile a ZK cluster according to a 'spec', it will eventually bring up a ZK instance running on spec.num_replicas pods, managed by a stateful set etc.". We can then make sure the implementation of our ZK operator, repeatedly trying to executing a control loop to reconcile the current and desired states of the ZK instance it is managing, delivers on that specification. Using verification here allows us to be sure that our ZK operator is correct even in the face of failures, asynchrony, series of edits to the required desired state (think repeatedly asking the operator to switch between 3 and 10 replicas), and more. This stuff is honestly impossible to write tests for (and unsurprisingly, no open-source Kubernetes operator we've seen tests for such cases extensively). That said, we still need to use traditional testing to be sure our assumptions about the boundary between verified and unverified code is correct (e.g., think of the Kubernetes API itself, assumptions about built-in controllers etc). The precursor to our use of verification in this context was, in fact, a system we built to do automatic reliability testing: https://www.usenix.org/system/files/osdi22-sun.pdf https://www.usenix.org/system/files/osdi22-sun.pdf -- even that work found a lot of safety and liveness bugs, but I feel it barely scratched the surface of what we could do with verification. So while the tooling still has a long way to go, I personally hope full-system verification becomes mainstream someday.
nullorempty 2y ago
Hm, so you write the code twice :)
- jpc0 2y ago
  You make implicit assumptions you had during development explicit through code or comments which doesn't actually effect runtime execution speed since it only runs in debug/compile time. There's a place for formal verification, usually in places where a bug causes death or significant financial loss.
- PhilipRoman 2y ago
  You're not wrong, but formal verification is still useful for multiple reasons: 1. Cases where specification is much less complex than implementation, like proving a sorting algorithm - the spec is very simple, forall integer i,j : i<j ==> result[i]<=result[j] plus the requirement that elements may not be removed or added 2. Ability to eliminate checks for improved performance (not sure if this applies to Rust yet, but it works great with Frama-C). 3. "Unit tests" for entire classes of behavior, not just specific inputs. Even if you cannot write a formal specification for a huge complex protocol, you can incrementally add asserts which cover much more area than simple unit tests.
- MaxBarraclough 2y ago
  In a toy example like min/max functions, yes, the spec and the implementation look very similar. For more substantial problems that won't be the case, e.g. a sorting function.
lifeinthevoid 2y ago
Is there some way to implement this so that the resulting code is still valid Rust code that can be compiled using vanilla Rust tools?
- IshKebab 2y ago
  It is valid Rust... but only because it wraps everything in a proc macro. Creusot does it in a different way using attributes, which IMO is a better approach because it means normal tooling works, though it does have much worse syntax.
camkego 2y ago
Could someone familiar with Verus comment on the power and expressiveness of Verus vs. Lean4 I understand Verus is an SMT based verification tool, and Lean is both an interactive prover and SMT based tool. But my understanding in the area of formal verification is limited, and it would be good to get an opinion from someone well versed in formal methods for software.
- staunton 2y ago
  Lean is similar to Coq. You could - state and prove things about (e.g.) C code, like the "Software Foundations" book does for Coq. However, nobody seems to be doing this with Lean and the tools are missing. - write programs in Lean4 and prove things about them. Some people are doing this a tiny little bit. - formalize pure math and publish papers about that. This is what Lean4 (and Coq) is mostly used for. The kinds of things Lean/Coq are able to practically state and prove are more general. Maybe you don't need that generality for real-world programs though.
berkeleynerd 2y ago
How does Versus compare to SPARK? Are they of the same general class of verifier? How is Versus different other than a verifier for Rust rather than a verifier for Ada?
eggy 2y ago
Is there a Rust standard yet like there is for C/C++, Common Lisp, and Ada/SPARK2014? Without that, it is a moving target compared to the verification tools that have been developed for say, Ada/SPARK2014. Not to mention the legacy of Ada/SPARK2014 in high-integrity, safety-critical applications from bare metal up.
- woile 2y ago
  https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ This?
  - eggy 2y ago
    I was following this ever since I had read about AdaCore collaborating with Ferrous Systems on this, however, it is for the compiler. If they created a published Rust standard specific to their compiler then maybe, but I think there needs to be a general Rust standard comparable to other PL standards to start to encroach on the Ada/SPARK2014 world and a whole lot of real-world apps over time.

284 points by gz09 2y ago

What exactly do SMT systems "solve" in cases like this? If I wrote a simple BFS or DFS and enumerated the search space how far would I get.. Is that not what TLA+ does in principle. I am surprised people prefer having a dependency of something like Z3 at compiler level.

IshKebab 2y ago
They try to find a counter-example to the constraints you have set up, or tell you that no such counter-example exists, in which case your program is correct. The counter-example is in the form of inputs to your program or function. It looks like the TLA+ Proof System does the same thing, but I believe you can also use TLA+ in "brute force all the states" mode. I haven't actually used it.
sunshowers 2y ago
SAT is an NP-complete problem. Doing an exhaustive search is very time-consuming. An SMT or SAT solver uses heuristics to make that process quicker for practical problems. It looks like there are some TLA+ implementations that do use SMT solvers under the hood.
tkz1312 2y ago
SMT solvers use a decision procedure known as CDCL(T). This uses a SAT solver at the core, which operates only on the core propositional structure of the input formula, and dispatches higher level constructs (e.g. functions, arrays, arithmetic) to specialized theory specific solvers. This is an extension of the CDCL (conflict driven clause learning) approach to SAT solving, which is a heuristic approach that uses information discovered about the structure of the problem to reduce the search space as it progresses. At a high level: 1. assign true or false to a random value 2. propagate all implications 3. if a conflict is discovered (i.e. a variable is implied to be both true and false): 1. analyze the implication graph and find the assignments that implied the conflict 2. Add a new constraint with the negation of the assignment that caused the conflict 3. backtrack until before the first assignment involved in the conflict was made The theory specific solvers use a diverse set of decision procedures specialized to their domain. The “Decision Procedures” book is an excellent overview: http://www.decision-procedures.org/ http://www.decision-procedures.org/
oggy 2y ago
TLA+ has also had an SMT-based backend, Apalache [1], for a few years now. In general, you encode your system model (which would be the Rust functions for Verus, the TLA model for Apalache) and your desired properties into an SMT formula, and you let the solver have a go at it. The deal is that the SMT language is quite expressive, which makes such encodings... not easy, but not impossible. And after you're done with it, you can leverage all the existing solvers that people have built. While there is a series of "standard" techniques for encoding particular program languages features into SMT (e.g., handling higher-order functions, which SMT solves don't handle natively), the details of how you encode the model/properties are extremely specific to each formalism, and you need to be very careful to ensure that the encoding is sound. You'd need to go and read the relevant papers to see how this is done. [1]: https://apalache.informal.systems https://apalache.informal.systems

IshKebab 2y ago

Interesting! Looks most similar to Creusot. The syntax is definitely nicer but wrapping your entire code in a macro surely is going to upset rust-analyzer?

tsujamin 2y ago
I’m not sure how rust-analyser works, but presumably you’d make the macro a no-op and just return the original tokens in debug builds
jaybosamiya 2y ago
A fork of rust-analyzer, called verus-analyzer, provides support for Verus syntax and actions (including new proof-specific actions) https://github.com/verus-lang/verus-analyzer/ https://github.com/verus-lang/verus-analyzer/

sdsd 2y ago

Noob question from someone with little real CS experience, when the README for this project says: > verifying the correctness of code What is the difference between "verifying" the correctness of code, as they say here, vs "proving" the correctness of code, as I sometimes see said elsewhere? Also, is there a good learning resource on "proving" things about code for working programmers without a strong CS / math background? Edit: I'm also very curious why "zero knowledge" proofs are so significant, and why this is so relevant. Eg I heard people talking about this and don't really understand why it's so cool: x.com/ZorpZK

dumbo-octopus 2y ago
Verifying and proving are used synonymously, as made clear later in the opening paragraph. As for zero knowledge proofs, there is little practical use, significance, or relevance to them due to the overhead involved and the lack of a "killer app", so to speak. But they're conceptually interesting.
- vlovich123 2y ago
  Whenever I hear people talk about the lack of practicality of some mathematical construct, I always remember G H Hardy who worked on number theory at the turn of the century. One of his famous quotes I love is: > I have never done anything 'useful.' No discovery of mine has made, or is likely to make, directly or indirectly, for good or ill, the least difference to the amenity of the world. Despite his self-proclaimed focus on pure mathematics, Hardy's work, particularly in number theory, has had profound applications in cryptography and other fields. I agree about the overhead. The costs have come down significantly already but they still remain a few orders of magnitude too large. That being said, it’s killer app is cloud compute. Right now the only way to amortize the cost of HW is to run it on someone else’s computer, which brings along with it all sorts of security and privacy risks. Well-performing ZK proofs (which we don’t know if it exists / it may be a long time before we figure out how to do it) would let you do cloud computing securely without worrying about vulnerabilities in your cloud provider’s network. Like all cryptography, it’s a double-edged sword because the same techniques would let websites deliver code for your machine to execute that you have no knowledge of what it’s doing.

dist1ll 2y ago

One of the main contributors gave an excellent talk [0] on Verus at the Rust meetup in Zürich. I was really impressed how clean this "ghost" code fits into programs (reminded me a bit of Ada). [0] https://www.youtube.com/watch?v=ZZTk-zS4ZCY https://www.youtube.com/watch?v=ZZTk-zS4ZCY

TachyonicBytes 2y ago

Is there any relationship between this and Kani[1]? Do they work differently? [1] https://github.com/model-checking/kani https://github.com/model-checking/kani

mmoskal 2y ago
Model checkers typically only explore a bounded number of states which is efficient at bug finding and often doesn't require additional annotations in the program. Automatic (SMT-based) verifiers like Verus, Dafny, F* (and my VCC :) require you to annotate most every function and loop but give you broad guarantees about the correctness of the program. Tools based on interactive provers (like Coq or Lean) typically require more guidance from the user but can guarantee even more complex properties.

im3w1l 2y ago

This looks really cool. One thing I think would be really useful for people is some instructions / examples of how to add proofs for an existing codebase. So maybe an example could be a bare-bones gui app with a single textbox, that does an http request to some resource (having data that is unknown at compile-time and potentially untrusted is a very common thing) and fetches an array, which is bubble-sorted and displayed in the box. The bubble sort has some intentional bug (maybe due to some off by one error, the last element remains untouched). There are unit-tests that somehow don't trigger the bug (worrying that your tests are incomplete would be a primary motivator to go for proofs). It could then show how to replace the unit tests with a proof, in the process discovering the bug and fixing it. The example wouldn't need to go into huge detail about the proof code itself as it is potentially advanced, instead it would focus on the nitty-gritty details of adding the proof, like how the interface between proved mathematical code and non-proved io code works, what command line to run to prove&build, and finally a zip archive with all of that, that you can play around with. Edit: Actually just reading from stdin and writing to stdout is probably good enough.

ComputerGuru 2y ago

For those that are interested but perhaps not aware of this similar project, Dafny is a "verification-aware programming language" that can compile to rust: https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny

algorithmsRcool 2y ago
Always cool to see Dafny mentioned! Shameless plug: I just wrote a beginner's introduction to Dafny a few days ago. https://www.linkedin.com/pulse/getting-started-dafny-your-first-formal-proof-alfred-white-puucc/ https://www.linkedin.com/pulse/getting-started-dafny-your-fi...

jph 2y ago

If you want a small stepping stone toward Versus, you can add Rust debug_assert for preconditions and postconditions; the Rust compiler strips these out of production builds by default. Example from the Versus tutorial with verification: fn octuple(x1: i8) -> (x8: i8) requires -16 <= x1, x1 < 16, ensures x8 == 8 * x1, { let x2 = x1 + x1; let x4 = x2 + x2; x4 + x4 } Example using debug_assert with runtime checks: fn octuple(x1: i8) -> i8 { debug_assert(-16 <= x1); debug_assert(x1 < 16); let x2 = x1 + x1; let x4 = x2 + x2; let x8 = x4 + x4; debug_assert(x8 == 8 * x1); x8 }

diarrhea 2y ago
I wish more people used asserts like that. Such a wonderful tool for documentation. It complements the type system and testing really well.
zozbot234 2y ago
One issue with the existing Verus syntax is that it requires wrapping the whole code in a proc-macro. Other Rust proof/verification/DbC tools such as Creusot use attribute-based syntax instead, which generally seems to be a bit more lightweight and idiomatic for Rust. Hopefully it will become available in future Verus releases.
lkrubner 2y ago
Your Versus example is how I write my Clojure code, with post and pre conditions on most of the functions. And the JVM has a flag that makes it easy to strip that out for production builds.
thesuperbigfrog 2y ago
You could also try the "contracts" crate: https://docs.rs/contracts/latest/contracts/ https://docs.rs/contracts/latest/contracts/
- nextaccountic 2y ago
  and you can use MIRAI, that takes the contracts defined by this crate and check them at compile time or, use prusti, that has contracts with a similar syntax checked at compile time as well

lsuresh 2y ago

We've used Verus to write formally verified Kubernetes controllers. Basically, we can prove liveness properties of the form "eventually, the controller will reconcile the cluster to the requested desired state". As you can imagine, there is a lot of subtlety and nuance to even specifying correctness here (think rapid changes to the desired state requirement, asynchrony, failures and what not). Code: https://github.com/vmware-research/verifiable-controllers/ https://github.com/vmware-research/verifiable-controllers/, with a corresponding paper due to appear at OSDI 2024.

Thaxll 2y ago
What does it do more than unit tests?
- lsuresh 2y ago
  Full-system verification is more powerful than unit tests. You can prove an implementation of a distributed system is free of entire classes of bugs, modulo your specification. The reason is that there is simply no way to practically write tests to cover enough out of all possible executions of a distributed system. Think arbitrary interleavings of message arrivals, failures, restarts and events affecting every single entity in the distributed system. We built a framework on top of Verus (called Anvil) that allowed us to write a top-level specifications of the form "If the ZooKeeper operator says it can reconcile a ZK cluster according to a 'spec', it will eventually bring up a ZK instance running on spec.num_replicas pods, managed by a stateful set etc.". We can then make sure the implementation of our ZK operator, repeatedly trying to executing a control loop to reconcile the current and desired states of the ZK instance it is managing, delivers on that specification. Using verification here allows us to be sure that our ZK operator is correct even in the face of failures, asynchrony, series of edits to the required desired state (think repeatedly asking the operator to switch between 3 and 10 replicas), and more. This stuff is honestly impossible to write tests for (and unsurprisingly, no open-source Kubernetes operator we've seen tests for such cases extensively). That said, we still need to use traditional testing to be sure our assumptions about the boundary between verified and unverified code is correct (e.g., think of the Kubernetes API itself, assumptions about built-in controllers etc). The precursor to our use of verification in this context was, in fact, a system we built to do automatic reliability testing: https://www.usenix.org/system/files/osdi22-sun.pdf https://www.usenix.org/system/files/osdi22-sun.pdf -- even that work found a lot of safety and liveness bugs, but I feel it barely scratched the surface of what we could do with verification. So while the tooling still has a long way to go, I personally hope full-system verification becomes mainstream someday.

nullorempty 2y ago

Hm, so you write the code twice :)

jpc0 2y ago
You make implicit assumptions you had during development explicit through code or comments which doesn't actually effect runtime execution speed since it only runs in debug/compile time. There's a place for formal verification, usually in places where a bug causes death or significant financial loss.
PhilipRoman 2y ago
You're not wrong, but formal verification is still useful for multiple reasons: 1. Cases where specification is much less complex than implementation, like proving a sorting algorithm - the spec is very simple, forall integer i,j : i<j ==> result[i]<=result[j] plus the requirement that elements may not be removed or added 2. Ability to eliminate checks for improved performance (not sure if this applies to Rust yet, but it works great with Frama-C). 3. "Unit tests" for entire classes of behavior, not just specific inputs. Even if you cannot write a formal specification for a huge complex protocol, you can incrementally add asserts which cover much more area than simple unit tests.
MaxBarraclough 2y ago
In a toy example like min/max functions, yes, the spec and the implementation look very similar. For more substantial problems that won't be the case, e.g. a sorting function.

lifeinthevoid 2y ago

Is there some way to implement this so that the resulting code is still valid Rust code that can be compiled using vanilla Rust tools?

IshKebab 2y ago
It is valid Rust... but only because it wraps everything in a proc macro. Creusot does it in a different way using attributes, which IMO is a better approach because it means normal tooling works, though it does have much worse syntax.

camkego 2y ago

Could someone familiar with Verus comment on the power and expressiveness of Verus vs. Lean4 I understand Verus is an SMT based verification tool, and Lean is both an interactive prover and SMT based tool. But my understanding in the area of formal verification is limited, and it would be good to get an opinion from someone well versed in formal methods for software.

staunton 2y ago
Lean is similar to Coq. You could - state and prove things about (e.g.) C code, like the "Software Foundations" book does for Coq. However, nobody seems to be doing this with Lean and the tools are missing. - write programs in Lean4 and prove things about them. Some people are doing this a tiny little bit. - formalize pure math and publish papers about that. This is what Lean4 (and Coq) is mostly used for. The kinds of things Lean/Coq are able to practically state and prove are more general. Maybe you don't need that generality for real-world programs though.

berkeleynerd 2y ago

How does Versus compare to SPARK? Are they of the same general class of verifier? How is Versus different other than a verifier for Rust rather than a verifier for Ada?

eggy 2y ago

Is there a Rust standard yet like there is for C/C++, Common Lisp, and Ada/SPARK2014? Without that, it is a moving target compared to the verification tools that have been developed for say, Ada/SPARK2014. Not to mention the legacy of Ada/SPARK2014 in high-integrity, safety-critical applications from bare metal up.

woile 2y ago
https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ This?
- eggy 2y ago
  I was following this ever since I had read about AdaCore collaborating with Ferrous Systems on this, however, it is for the compiler. If they created a published Rust standard specific to their compiler then maybe, but I think there needs to be a general Rust standard comparable to other PL standards to start to encroach on the Ada/SPARK2014 world and a whole lot of real-world apps over time.