8 ms·
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 fr
by kite42 17d 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 17d agoI like how they also neglected to mention that Verus was invented at Microsoft...
- hwayne 17d agoNot 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.
- anonymousDan 17d agoI 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?