On: Coq-of-rust: Formal verification tool for Rust

[Pelayu]

Does anyone know of any good resources explaining how a theorem prover like Coq is actually used to prove safety properties of software? All the resources I’ve found thus far have been more in the pure mathematics domain, and not so much about applying it to software.

[lheck → Pelayu]

Colleagues of mine are using it to verify concurrent programs: https://iris-project.org/tutorial-material.html

[SubjectToChange → Pelayu]

Software Foundations is quite a comprehensive series on program verification.