What is the name of the tool?
Verus
Add a concise description of the tool. Please refrain from marketing claims and stick to what the tool is, does, and how it would be used?
Verus is a tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions of the code. Rather than adding run-time checks, Verus instead relies on powerful solvers to prove the code is correct. Verus currently supports a subset of Rust (which we are working to expand), and in some cases, it allows developers to go beyond the standard Rust type system and statically check the correctness of code that, for example, manipulates raw pointers.
Link to the tool repo or homepage
https://github.com/verus-lang/verus
License of the tool
MIT
What is your role/connection to this tool?
Creator/Maintainer (open source)
Optional name of the tool vendor
Verus Team
Optional liability provided by the tool vendor
No response
List any standards the tool is qualified for
No response
Tool category
formal-verification
What is the name of the tool?
Verus
Add a concise description of the tool. Please refrain from marketing claims and stick to what the tool is, does, and how it would be used?
Verus is a tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions of the code. Rather than adding run-time checks, Verus instead relies on powerful solvers to prove the code is correct. Verus currently supports a subset of Rust (which we are working to expand), and in some cases, it allows developers to go beyond the standard Rust type system and statically check the correctness of code that, for example, manipulates raw pointers.
Link to the tool repo or homepage
https://github.com/verus-lang/verus
License of the tool
MIT
What is your role/connection to this tool?
Creator/Maintainer (open source)
Optional name of the tool vendor
Verus Team
Optional liability provided by the tool vendor
No response
List any standards the tool is qualified for
No response
Tool category
formal-verification