In this blog post, we present the formal verification effort we started to show the absence of bugs in the ⚈ Smoo.th library, a library for optimized 〰️ elliptic curve operations in Solidity. We are using our tool coq-of-solidity to make this non-trivial verification using the generic proof assistant 🐓 Coq.
The Smoo.th library is interesting as elliptic curves are at the core of many cryptographic protocols, including authentication protocols, and having a generic and fast implementation simplifies the development of dApps in environments with missing pre-compiled (like L1s) or missing circuits (like zero-knowledge layers).
From a verification point of view, it is very challenging as it combines low-level operations (hand-optimized Yul code with bit shifts, inlined functions, ...) with higher-level reasoning on elliptic curves and arithmetic 💪.