The risk of open source code: what the past still teaches us
The most consequential security failures in privacy software rarely come from anyone being careless. They come from properties that held in one place and quietly stopped holding in another.
In April 2014, a Google researcher found a bug in OpenSSL that had been in production for two years. Heartbleed allowed an attacker on the open internet to read 64 kilobytes of server memory at a time, again and again, for free. Private keys, session tokens, passwords. Whatever the server happened to be holding. Two-thirds of the web's HTTPS was exposed. Millions of individuals had their data exposed to malicious users, including medical information.
OpenSSL was open source. Plenty of people had read the code. Security firms had audited it. The bug remained undetected anyway, sat there for two years, and was eventually caught by researchers who happened to look in the right place.
The industry and community took Heartbleed seriously and built layer after layer of mitigation in response. Cleaner forks, memory-safe languages, better tooling, and more rigorous audits are all used to close security gaps between the design of protocols and their implementations. But some gaps have proved harder to close. In 2022, a team led by Royal Holloway published "Practically-exploitable Cryptographic Vulnerabilities in Matrix". It identified five distinct flaws in the end-to-end encryption protocol used by tens of thousands of organizations. Some were in the specification itself, as the design was unsound in ways that audits and code review had not caught. Matrix was patched, enhancing not only the protocol but the collective trust in it. Matrix had every safeguard the privacy industry has built up over a decade of hard-won lessons, and those safeguards remain essential. Unfortunately, they do not, on their own, close the gap between "audited and open source" and "provably correct."
Across the field, the response has been to add new layers of assurance. Signal's post-quantum work (PQXDH in 2023, the SPQR ratchet in 2025) is one of the most public examples, built with formal analysis in mind from the design stage onward, in collaboration with academic researchers and Cryspen. The proofs are part of the build pipeline, re-run on every code change, in the same repository as the protocol itself. The same shift is visible across the broader privacy-tech ecosystem, with cryptographic libraries increasingly written in memory-safe languages and verified at design time [ref].
Including formal guarantees in your security stack is the direction privacy-related software development is going. Audits and peer review are more necessary than ever, and open-source development potentially brings lots of eyes to critical software. But in the age of AI-enabled attackers, for protocols carrying some of the most sensitive operations, machine-checked proofs that re-run on every major change are no longer a luxury, they’re a necessity. Formal methods have quietly underpinned critical software for years, from cryptographic libraries to operating system kernels to the Signal Protocol itself. But now, with the help of AI, the same force that ships code a thousand times faster or finds new zero-days with a single prompt can be brought to bear on securing the critical infrastructure our society depends on.
If you build privacy software, the question worth sitting with is what your version of these guarantees and requirements looks like. Not whether you'll need formal verification eventually, but what shape it should take in your stack, and how soon.
