by
Daniel King
![](https://blog.adacore.com/uploads/_300x300_crop_center-center_none/hex_code_blue.jpg)
Avoiding Vulnerabilities in Crypto Code with SPARK
Writing secure software in C is hard. It takes just one missed edge case to lead to a serious security vulnerability, and finding such edge cases is difficult. This blog post discusses a recent vulnerability in a popular SHA-3 library and how the same problems were avoided in my own SHA-3 library written in SPARK.