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.
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.
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 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.
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.
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).
I agree on paper, but in practice most verification annotations in real code require a PhD to understand.
To me, it’s essentially implementing the same code twice in two languages and checking the behavior matches.
If the same person implements both, what are the odds they implement the same bug in both?
Only verification annotations are generally even harder to read and write than the code itself, making it even more difficult to tell if you implemented the proof according to the spec, or just mirrored what the function actually does.
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).
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.
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".
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