Hello everyone. I studied RIOT OS crypto library for my Masters project during 2022-23. I studied the application of formal verification techniques for detecting run-time errors in the crypto library C code of RIOT. It was for detection of runtime errors using ACSL statements (and not about proving the correctness of the algorithms) and proving the statements in Frama-C using WP. I also studied about the RIOT-fp project and the various new approaches being used there. I would be glad if you find it interesting and go through it. Any advice or inputs would be welcome. I used Allan Blanchard’s book for reference. I have uploaded the files with the annotated assertions in GitHub. Am I allowed to upload the annotated code on GitHub? If not please inform me I’ll take it down. Thank You.