Checking the Checkers and Auditing the Ironwood FV

Cryptographic software is error-prone and failures are catastrophic,
therefore formal verification is a powerful and increasingly
practical tool for greatly improving the assurances of our cryptographic software.
But who verifies the formal verification?
Formal verification itself is software too,
what is proved, under which assumptions and its relation to the real-world implementation lie beyond the scope of the machine-checked proof.
In this post, we want to give some insights into our three-week audit of the Ironwood formalization
and some of the common pitfalls that formal verification more broadly can encounter.