One note though: Verus and the tool Software Foundations works with (Coq) take different approaches to proving things.
Verus attempts to prove properties automatically using something called an SMT solver, which is an automated system for solving constraints. Coq on the other hand, requires you to manually prove much more, offering a more limited set of automations for proving things.
Both have their advantages and disadvantages, namely that automation is great when it works and annoying when it doesn't.
(Another side note: Zero Knowledge Proofs (ZKPs) are kind of something different. A great many people who work in formal verification/proof don't touch ZKPs at all (ex: me). They are better thought about as a cryptography primitive)
One note though: Verus and the tool Software Foundations works with (Coq) take different approaches to proving things.
Verus attempts to prove properties automatically using something called an SMT solver, which is an automated system for solving constraints. Coq on the other hand, requires you to manually prove much more, offering a more limited set of automations for proving things.
Both have their advantages and disadvantages, namely that automation is great when it works and annoying when it doesn't.
(Another side note: Zero Knowledge Proofs (ZKPs) are kind of something different. A great many people who work in formal verification/proof don't touch ZKPs at all (ex: me). They are better thought about as a cryptography primitive)