Bootstrapping the Verified Software Stack (theorem.dev)

A recent initiative aims to establish a verified software stack, leveraging the nixpkgs bootstrapping chain as a model for ensuring the reliability of software systems. The project highlights the potential of AI-enabled formal verification, noting that significant improvements in model performance, doubling every two months, could enable the verification of 95% of machine code in the nixpkgs ecosystem by 2027 for an estimated cost of $134 million. This is striking when contrasted with the projected annual damages from cybercrime, which exceed $500 billion. The method focuses on verifying software at the binary level to ensure that real bugs are identified, rather than artifacts of modeling. This approach facilitates the verification of interdependent libraries efficiently, allowing a majority of packages to leverage verified components without incurring redundant costs. The project's success relies on collaborative efforts across the software ecosystem, encouraging contributions from developers, model builders, and formal verification experts to create a robust and scalable verified software environment.