Safety-Critical Tool Submission: VeriFast

[af-airbus]

What is the name of the tool?

VeriFast

What is a description of the tool, what it does, how it would be used?

Research prototype tool for modular formal verification of C, Rust and Java programs.

VeriFast is a tool for modular formal verification of the absence of undefined behavior in Rust1 programs that use unsafe blocks and the soundness of Rust modules that use unsafe blocks. It works by symbolically executing each function separately, using a separation logic representation of memory, starting from a symbolic state that represents an arbitrary program state that satisfies the function's precondition, and checking that each state at which the function returns satisfies the function's postcondition.

Link to the tool repo or homepage

https://github.com/verifast/verifast

What is your role/connection to this tool?

Other

Tool category

formal-verification