Comment by kite42
12 hours 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.
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?