Code verifications / provers

C code + ACSL annotations --( Frama-C )--> "WhyML" Why3 format Proofs  --( Why3 analyser )--> proven code

• ACSL By Example (good learning point with plenty of exmaples) Towards a Verified C Standard Library

https://www.mimuw.edu.pl/~alx/konstruowanie/ACSL-by-Example.pdf

• Frama-C code analyser (Framework for Modular Analysis of C programs)

https://frama-c.com/
 https://frama-c.com/html/documentation.html 

https://frama-c.com/2016/11/22/Frama-C-and-ACSL-are-on-GitHub.html

• Why3 / WhyML :

http://why3.lri.fr/

http://why3.lri.fr/doc/starting.html