We've used Verus to write formally verified Kubernetes controllers.<p>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).<p>Code: <a href="https://github.com/vmware-research/verifiable-controllers/">https://github.com/vmware-research/verifiable-controllers/</a>, with a corresponding paper due to appear at OSDI 2024.
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.<p>Example from the Versus tutorial with verification:<p><pre><code> 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
}
</code></pre>
Example using debug_assert with runtime checks:<p><pre><code> 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
}</code></pre>
Noob question from someone with little real CS experience, when the README for this project says:<p>> verifying the correctness of code<p>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?<p>Also, is there a good learning resource on "proving" things about code for working programmers without a strong CS / math background?<p>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
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: <a href="https://github.com/dafny-lang/dafny">https://github.com/dafny-lang/dafny</a>
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.<p>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.<p>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.<p>Edit: Actually just reading from stdin and writing to stdout is probably good enough.
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).<p>[0] <a href="https://www.youtube.com/watch?v=ZZTk-zS4ZCY" rel="nofollow">https://www.youtube.com/watch?v=ZZTk-zS4ZCY</a>
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.
Is there any relationship between this and Kani[1]? Do they work differently?<p>[1] <a href="https://github.com/model-checking/kani">https://github.com/model-checking/kani</a>
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?
Could someone familiar with Verus comment on the power and expressiveness of Verus vs. Lean4<p>I understand Verus is an SMT based verification tool, and Lean is both an interactive prover and SMT based tool.<p>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.
What exactly do SMT systems "solve" in cases like this?<p>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.<p>I am surprised people prefer having a dependency of something like Z3 at compiler level.
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?