Verifast

Verifast is a formal verification tool for C, Rust, and Java programs.

References