In this blog post, we describe how we at SandboxAQ, together with Cryspen, formally verified key components of Sandwich—an open-source, unified API that simplifies the use of cryptographic libraries for developers, enabling crypto-agility.