Galois’s mission is to help make the critical systems that the world relies on more secure and trustworthy. Over the years, we’ve put our team’s deep expertise in software correctness, cryptography, digital engineering, and machine learning to work, providing formal assurance for complex systems in high stakes contexts for both government and commercial clients. From militaries to financial institutions to tech and industry giants, we’ve had the opportunity to work on some pretty amazing (and high impact) projects. Yet to date, perhaps the most exciting and impactful of these projects has been our ongoing work on cryptographic security for cloud-scale industrial companies like Amazon Web Services, Inc. (AWS) and Supranational. Cryptographic systems are at the core of any trustworthy networked system. Since 2015, Galois has worked with AWS to help ensure the security of some of the key cryptographic systems that protect their cloud. AWS is “architected to be the most secure global cloud infrastructure on which to build, migrate, and manage applications and workloads.” Supranational provides cryptographic infrastructure for the Ethereum blockchain. In 2020, Galois partnered with Supranational to provide formal verification for ‘blst’, a BLS signature library that serves as an important part of consensus protocols for next-gen blockchain technologies like Eth2 and Filecoin. Both cases involved the need for guaranteeing security and privacy, without compromising high performance standards. This is even tougher than it sounds. As technology grows more complex and interconnected, securing systems is becoming more and more difficult. In short, bigger codebases and more complicated systems mean bigger attack surfaces and potentially more vulnerabilities. As threats grow and systems become more compli