Case study: Formally Verifying a Cryptographic Library That Secures Billions in Digital Assets​

TSupranational’s blst library actively secures more than $15 billion in digital assets, including those on the Ethereum 2 and Filecoin blockchains. Supranational carefully developed its code and initiated third-party audits. But Supranational wanted to take security one step further – formally verifying the entire blst library to have the highest level of software assurance.

For that, they decided to partner with Galois.

Galois is a global leader in software assurance and formal verification. Our verification capabilities and tools enabled us to create proofs of the blst library’s code. Many verification approaches end up altering a company’s source code, making it difficult to both update the code and ensure its correctness.

We have developed a way to prove blst’s codebase correct without requiring any changes to the code itself. This enabled Supranational the best of both worlds: blst can be carefully tuned by experts, but it is guaranteed to behave exactly as it was intended – keeping billions of dollars in digital tokens secure.