Our Report On AI-Enabled Tools For Scaling Formal Verification
Scaling Human Understanding and Review Capacity
At Atlas Computing, we focus on advancing humanity’s understanding and enhancing review capacity through innovative technologies. We’re excited to share our latest report, which outlines the tools that we think are needed to understand the software that runs our world, as well as all the software that AI systems will generate in the coming years. The report, titled "AI-Assisted Code Specification, Synthesis, and Verification," outlines a widely-applicable strategy and lists the modular tools that we believe will dramatically facilitate the use of formal verification.
Formal verification (FV) is the gold standard for security and stability to ensure that software is behaving as intended. However, the traditional FV processes are labor-intensive and costly, often limiting their application to only the most critical subsystems, but we believe advances in AI will make formal verification the dominant form of software development in the near future. In the report, we elaborate on the potential and current limitations of formal verification (FV), outline existing formalization workflows, and describe the 12 modular projects that can automate steps in those workflows. We recommend the 2-page executive summary at the start of the document for more information, but you can see the main diagram below. The report was created in collaboration with the Topos Institute, funded by Protocol Labs and the Survival and Flourishing Fund.
Next Step: Prototyping
We are actively looking for funders, potential users, and talented engineers/researchers to join us in this exciting endeavor. If you are interested in funding our work, becoming a user of our tools, or contributing to the research and development efforts, please reach out to us at hello@atlascomputing.org
Your support and participation can help us accelerate the development and adoption of these innovative tools, ultimately contributing to a safer and more secure digital world. Together, we can scale human understanding and review capacity, making formal verification an integral part of software development.
We (the authors) received a question about the diagram on pg 22 on "Underspecification, Misspecification, Overspecification": In Underspecification, why is the circle for Formal Spec larger than the circle for User Intent if the formal spec is smaller than the user intent?
This is a good question, and we apologize that our diagram (and accompanying description) is confusing.
When we were drawing this diagram, we thought of the circles as representing sets of solutions that are captured by the specs, rather than the set of conditions listed in the specs. For example, in Underspecification, the formal spec captures lots of solutions which do not fit the actual user intent.
Hope this clarification clears up any confusion.