3 ms·

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 possib

by jdw64 17d ago

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?

Jtsummers 17d ago
https://verus-lang.github.io/verus/publications-and-projects/ 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. https://mitpress.mit.edu/9780262546232/program-proofs/ https://mitpress.mit.edu/9780262546232/program-proofs/ - Dafny book, pretty good tutorial on the topic https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html# https://learn.adacore.com/courses/intro-to-spark/chapters/01... - Free tutorial for SPARK
- jdw64 17d ago
  thanks!
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 16d ago
  I like how they also neglected to mention that Verus was invented at Microsoft...
  - hwayne 16d ago
    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.
    - anonymousDan 16d ago
      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?

by jdw64 17d ago

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?

Jtsummers 17d ago

https://verus-lang.github.io/verus/publications-and-projects/ 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. https://mitpress.mit.edu/9780262546232/program-proofs/ https://mitpress.mit.edu/9780262546232/program-proofs/ - Dafny book, pretty good tutorial on the topic https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html# https://learn.adacore.com/courses/intro-to-spark/chapters/01... - Free tutorial for SPARK

jdw64 17d ago
thanks!

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 16d ago
I like how they also neglected to mention that Verus was invented at Microsoft...
- hwayne 16d ago
  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.
  - anonymousDan 16d ago
    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?