Usage of Formal Verification in Industry/ Industrial Producs

file.txt

This is an list of advanced PL research / FV research or the use of FV research or implementation of FV in the industry. This will be upgrated timely. 

-----------------------------------------------------------------------------------------------------------------

Starter: Who is verifying their cryptographic protocols? https://galois.com/blog/2021/05/who-is-verifying-their-cryptographic-protocols/  

1) Static Analysis at Scale: An Instagram Story ->  https://instagram-engineering.com/static-analysis-at-scale-an-instagram-story-8f498ab71a0c

2) Zoncolan: How Facebook uses static analysis to detect and prevent security issues -> https://engineering.fb.com/security/zoncolan/

3) Proving security with automated reasoning -> https://www.allthingsdistributed.com/2019/06/proving-security-at-scale-with-automated-reasoning.html

4) Using EasyCrypt and Jasmin for post-quantum verification -> https://blog.cloudflare.com/post-quantum-easycrypt-jasmin/
5) Design and Verification of the Arm Confidential Compute Architecture https://www.usenix.org/conference/osdi22/presentation/li 
6) Wireguard Formal Verification https://www.wireguard.com/formal-verification/ 
7) Avoiding Vulnerabilities in Crypto Code with SPARK https://blog.adacore.com/avoiding-vulnerabilities-in-crypto-code-with-spark
8) An Analysis of Signal's PQXDH https://cryspen.com/post/pqxdh/ 
9) Formal Verification of Ethereum 2.0 Part 1: Fixing the Array-Out-of-Bound Runtime Error https://consensys.io/blog/formal-verification-of-ethereum-2-0-part-1-fixing-the-array-out-of-bound-runtime-error  
10) 

added some other links including the latest article I found from LinkedIn