Verified software in production

CompCert is a formally verified optimizing C compiler. Its central theorem: the compiled machine code behaves identically to the source C program. Every optimization pass is proven to preserve semantics.

In the landmark Csmith study (Yang et al., 2011), researchers randomly generated C programs and compiled them with every major compiler. GCC and LLVM each produced hundreds of wrong-code bugs. CompCert produced zero. It was the only compiler where no miscompilations were found.

This matters because compiler bugs are invisible — they silently turn correct source code into incorrect binaries. CompCert is used commercially by Airbus for safety-critical avionics software under DO-178C certification.

Cedar is Amazon's open-source authorization policy language and engine. It powers Amazon Verified Permissions and handles over one billion automated-reasoning checks daily across AWS services.

Authorization is an ideal target for formal verification: it's a pure function (policy + request → permit or deny), it's security-critical, and incorrect decisions can expose sensitive data. Cedar uses a combination of differential random testing, SMT solvers, and Lean proofs to guarantee that authorization decisions are deterministic and correct.

Cedar demonstrates that formal verification isn't just for academic proofs — it's running in production at the scale of one of the world's largest cloud providers.

SymCrypt is Microsoft's core cryptographic library, used across Windows and Azure. It implements the fundamental cryptographic primitives — hashing, encryption, key exchange — that millions of systems depend on.

Microsoft is progressively verifying SymCrypt's implementations in Lean 4, producing machine-checked proofs that the code correctly implements its cryptographic specifications. This is particularly important because cryptographic code is rarely modified, universally depended upon, and catastrophic when wrong.

Cryptographic bugs don't crash your program — they silently compromise security. A single incorrect bit operation can reduce a 256-bit key to trivially breakable. Formal verification ensures that the mathematical properties of the algorithms are preserved exactly in the implementation.

Veil is a framework for verifying distributed protocols — consensus algorithms, replication protocols, and coordination mechanisms — in Lean 4. Distributed systems are notoriously hard to test because bugs emerge from specific interleavings of messages, network partitions, and timing that are nearly impossible to reproduce.

Veil found bugs in protocols that had previously been "verified" by two other tools, demonstrating that the rigor of the proof matters as much as the act of verification itself.

This work from NUS represents the frontier of what formal verification can cover: not just sequential code, but concurrent, distributed systems where the state space is effectively infinite.