How to integrate formal proofs into software development

ICSE paper presents techniques piloted by Amazon Web Services’ Automated Reasoning team.

Formal verification is the process of using automatic proof procedures to establish that a computer program will do what it’s supposed to. Given a mathematical specification of how a function is supposed to behave, and some assumptions about the environment where the code executes (e.g., how the operating system behaves and which inputs are reasonable), formal verification determines whether the code as written will ever, with any input that meets the assumptions, violate the specification.

Formal verification is known to produce more secure and less buggy code, but it’s rarely used on large commercial software projects. Developers working on deadline lack time to write careful function specifications — if they’re even familiar with the formal languages typically used for them. Verification teams, conversely, lack familiarity with the software under development; learning how every function in a commercial-scale program is supposed to behave can be prohibitively time consuming.

Embedded verification code.png
An example of how developers might embed function specifications in their code.

On the Amazon Web Services’ Automated Reasoning team, we’ve piloted several projects on integrating formal verification into the software development process. Some involve verification at the protocol level; some involve generating code directly from a verified specification; and some involve verification at the code level itself.

In a paper we’ll present at the International Conference on Software Engineering — which was to be held this week but has been postponed until July — we describe lessons learned from one of the code-level verification projects, which involved a large development initiative in 2019.

In the paper, we report that, thanks to our methodology, the number of verified lines of code, bugs found and fixed, verification “contracts” introduced by developers, and working code (i.e., non-proof code) contributed by the verification team all increased precipitously in the first eight months of the project.

Lines proven.png
Thousands of lines of code verified over the first eight months of a large AWS development project. The graph flatline indicates that we hit our target for this experiment.

Our method has six key components:

1. Function specification in a familiar programming language.

Writing function specifications typically requires a special-purpose formal language that can capture all of the logical relationships that might govern a function’s execution. With our method, both the verification team and the developer team instead specify functions in the language in which the code is being written — in this case, C. This approach sacrifices some expressive power: there are some logical relationships that C cannot capture. But we have found that ease of adoption more than makes up for the loss of expressivity.

2. Declarative function specification.

Most familiar programming languages — such as C — are imperative, meaning they describe functions as sequences of operations. For function specification, however, declarative syntax is more intuitive. For instance, the developer should be able to say (in slightly more formal terms), “This function doubles each value in an array”, rather than having to write out the procedure for stepping through the array and doubling values individually. With our method, the verification team provides a library of functions that enables developers to write such declarative specifications in a familiar imperative language.

3. Code-embedded specifications.

Most program functions are written as self-contained blocks of code. With our method, we allow the developer to write a function specification as a set of preconditions that precede each such block — which function inputs are invalid, for instance — and a set of postconditions after each such block — that an array has adequate memory allocated to it, for instance (see sample code, above). Usually, a developer writing a function is thinking through such operational parameters, anyway, so adding the specification is not a huge burden.

4. A proof model that uses a familiar “unit test” syntax.

Many developers are already familiar with writing “unit tests” for their code. Inserted into the code for a specific program function, the unit test cycles through a sequence of inputs to determine whether any cause errors. Our proof method uses a very similar syntax, except that, rather than a sequence of concrete inputs, it specifies a range of possible inputs. Such test code can automatically be converted into the type of mathematical expression that automated provers are designed to evaluate.

Bugs found.png
Number of bugs found over the first eight months of the project.

5. Bug repair.

The great advantage of formal verification is that it not only identifies bugs but indicates how to fix them, by pinpointing exactly which lines of code lead to violation of the function specification. We have found that one of the most effective means of selling developers on the utility of formal verification is for the verification team to not only identify bugs but provide code patches for them.

6. Continuous integration.

On large software projects, code is constantly being revised. As part of our method, we provide a back-end system that automatically re-runs the prover on new code as soon as it’s checked in to a repository, providing immediate feedback on whether the revision does or does not violate function specifications.

Continuous integration.png
The interface for our continuous-integration engine, indicating newly checked-in code that does (x’s) or does not (check marks) violate existing function specifications.

In the paper, we report the application of our methodology during development work on the AWS C Common Library, an open-source repository of functions used by several other AWS libraries, including widely used AWS software development kits.

Using our methodology, one full-time verification engineer and two interns, working together with the development team, were able to specify and verify (with some assumptions) 171 entry points (points in the program where the user can input data) over nine key modules of the library.

In ongoing work, we are expanding not only the code base to which we apply our methodology but also the range of functionality that our method can verify automatically. We are also evaluating best practices for long-term maintenance of provable code and for bringing new developers up to speed on existing provable code bases.

Related content

US, WA, Seattle
We are a team of doers working passionately to apply cutting-edge advances in deep learning in the life sciences to solve real-world problems. As a Senior Applied Science Manager you will participate in developing exciting products for customers. Our team rewards curiosity while maintaining a laser-focus in bringing products to market. Competitive candidates are responsive, flexible, and able to succeed within an open, collaborative, entrepreneurial, startup-like environment. At the leading edge of both academic and applied research in this product area, you have the opportunity to work together with a diverse and talented team of scientists, engineers, and product managers and collaborate with others teams. Location is in Seattle, US Embrace Diversity Here at Amazon, we embrace our differences. We are committed to furthering our culture of inclusion. We have ten employee-led affinity groups, reaching 40,000 employees in over 190 chapters globally. We have innovative benefit offerings, and host annual and ongoing learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences. Amazon’s culture of inclusion is reinforced within our 14 Leadership Principles, which remind team members to seek diverse perspectives, learn and be curious, and earn trust Balance Work and Life Our team puts a high value on work-life balance. It isn’t about how many hours you spend at home or at work; it’s about the flow you establish that brings energy to both parts of your life. We believe striking the right balance between your personal and professional life is critical to life-long happiness and fulfillment. We offer flexibility in working hours and encourage you to find your own balance between your work and personal lives Mentor & Grow Careers Our team is dedicated to supporting new members. We have a broad mix of experience levels and tenures, and we’re building an environment that celebrates knowledge sharing and mentorship. Our senior members enjoy one-on-one mentoring and thorough, but kind, code reviews. We care about your career growth and strive to assign projects based on what will help each team member develop into a better-rounded engineer and enable them to take on more complex tasks in the future. Key job responsibilities • Manage high performing engineering and science teams • Hire and develop top-performing engineers, scientists, and other managers • Develop and execute on project plans and delivery commitments • Work with business, data science, software engineer, biological, and product leaders to help define product requirements and with managers, scientists, and engineers to execute on them • Build and maintain world-class customer experience and operational excellence for your deliverables
US, Virtual
The Amazon Economics Team is hiring Interns in Economics. We are looking for detail-oriented, organized, and responsible individuals who are eager to learn how to work with large and complicated data sets. Some knowledge of econometrics, as well as basic familiarity with Stata, R, or Python is necessary. Experience with SQL, UNIX, Sawtooth, and Spark would be a plus. These are full-time positions at 40 hours per week, with compensation being awarded on an hourly basis. You will learn how to build data sets and perform applied econometric analysis at Internet speed collaborating with economists, data scientists and MBAʼs. These skills will translate well into writing applied chapters in your dissertation and provide you with work experience that may help you with placement. Roughly 85% of interns from previous cohorts have converted to full time economics employment at Amazon. If you are interested, please send your CV to our mailing list at econ-internship@amazon.com.
US, WA, Seattle
Amazon internships are full-time (40 hours/week) for 12 consecutive weeks with start dates in May - July 2023. Our internship program provides hands-on learning and building experiences for students who are interested in a career in hardware engineering. This role will be based in Seattle, and candidates must be willing to work in-person. Corporate Projects (CPT) is a team that sits within the broader Corporate Development organization at Amazon. We seek to bring net-new, strategic projects to life by working together with customers and evolving projects from ZERO-to-ONE. To do so, we deploy our resources towards proofs-of-concept (POCs) and pilot programs and develop them from high-level ideas (the ZERO) to tangible short-term results that provide validating signal and a path to scale (the ONE). We work with our customers to develop and create net-new opportunities by relentlessly scouring all of Amazon and finding new and innovative ways to strengthen and/or accelerate the Amazon Flywheel. CPT seeks an Applied Science intern to work with a diverse, cross-functional team to build new, innovative customer experiences. Within CPT, you will apply both traditional and novel scientific approaches to solve and scale problems and solutions. We are a team where science meets application. A successful candidate will be a self-starter comfortable with ambiguity, strong attention to detail, and the ability to work in a fast-paced, ever-changing environment. As an Applied Science Intern, you will own the design and development of end-to-end systems. You’ll have the opportunity to create technical roadmaps, and drive production level projects that will support Amazon Science. You will work closely with Amazon scientists, and other science interns to develop solutions and deploy them into production. The ideal scientist must have the ability to work with diverse groups of people and cross-functional teams to solve complex business problems.
US, WA, Seattle
Amazon internships are full-time (40 hours/week) for 12 consecutive weeks with start dates in May - July 2023. Our internship program provides hands-on learning and building experiences for students who are interested in a career in hardware engineering. This role will be based in Seattle, and candidates must be willing to work in-person. Corporate Projects (CPT) is a team that sits within the broader Corporate Development organization at Amazon. We seek to bring net-new, strategic projects to life by working together with customers and evolving projects from ZERO-to-ONE. To do so, we deploy our resources towards proofs-of-concept (POCs) and pilot programs and develop them from high-level ideas (the ZERO) to tangible short-term results that provide validating signal and a path to scale (the ONE). We work with our customers to develop and create net-new opportunities by relentlessly scouring all of Amazon and finding new and innovative ways to strengthen and/or accelerate the Amazon Flywheel. CPT seeks an Applied Science intern to work with a diverse, cross-functional team to build new, innovative customer experiences. Within CPT, you will apply both traditional and novel scientific approaches to solve and scale problems and solutions. We are a team where science meets application. A successful candidate will be a self-starter comfortable with ambiguity, strong attention to detail, and the ability to work in a fast-paced, ever-changing environment. As an Applied Science Intern, you will own the design and development of end-to-end systems. You’ll have the opportunity to create technical roadmaps, and drive production level projects that will support Amazon Science. You will work closely with Amazon scientists, and other science interns to develop solutions and deploy them into production. The ideal scientist must have the ability to work with diverse groups of people and cross-functional teams to solve complex business problems.
US, CA, Palo Alto
The Amazon Search team creates powerful, customer-focused search solutions and technologies. Whenever a customer visits an Amazon site worldwide and types in a query or browses through product categories, Amazon Search services go to work. We design, develop, and deploy high performance, fault-tolerant distributed search systems used by millions of Amazon customers every day. We’re seeking a Principal Scientist with a deep expertise in Search Science. Your responsibilities will include everything from developing and prototyping innovative machine learning, and deep learning algorithms to implementing, testing, and supporting full solutions in a production environment. We are looking for innovators who can contribute to advancing search technology on what’s scientifically possible while remaining committed to creating world-class products. Joining this team, you’ll experience the benefits of working in a dynamic, entrepreneurial environment, while leveraging the resources of Amazon.com (AMZN), Earth's most customer-centric company one of the world's leading internet companies. We provide a highly customer-centric, team-oriented environment in our offices located in Palo Alto, California. Key job responsibilities As a hands-on leader of this team, you’ll be responsible for defining key research questions, identifying relevant data, adopting or proposing innovative machine learning solutions conducting rigorous experiments, publishing results and working with the engineering team to deploy these solutions. As a strategic leader, you will identify investment opportunities, develop long term strategies, and propose, prioritize and deliver on goals. You’ll also participate in organizational planning, hiring, mentorship and leadership development. You will be technically fearless and with a passion for building scalable science and engineering solutions. You will serve as a key scientific resource in full-cycle development (conception, design, implementation, testing to documentation, delivery, and maintenance). About the team Starting in 2009, the Visual Search & Augmented Reality team has thus far launched many visual search solutions on the Amazon App that use computer vision and machine learning/deep learning to help customers complete their shopping missions more easily; multiple internal teams at Amazon (devices, Kindle, Seller services, etc.) also use our libraries and APIs to deliver solutions to their own customers. We are a full stack shop, and our team capabilities cover the whole solution spectrum, ranging across applied science, large scale engineering services, product management, UX design, and mobile app development for iOS and Android.
US, MN, Minneapolis
AWS Central Economics is an interdisciplinary team on the cutting edge of economics, statistical analysis, and machine learning whose mission is to solve problems that have high risk with abnormally high returns. Our team leverages the strengths of our scientists to build solutions for some of the toughest business problems here at Amazon AWS. We are looking for an exceptionally talented, seasoned, and motivated Economist to manage a team of economists and data scientists to drive the science for AWS. Key job responsibilities Manage a team of economists and data scientists to deliver actionable economic analyses to business leaders, provide leadership on the economics and science used in the analyses, and engage with business leaders to identify challenges AWS faces that call for in-depth economic analyses and to ensure the analyses have their intended impact.
LU, Luxembourg
&ltHire Relocation Requisition - not for posting> Provides insights to leadership on improving Supply Chain cost and Speed by using Data Science and Analytics techniques. Build Dashboards and models to industrialize these findings at scale.
US, VA, Arlington
The People eXperience and Technology Central Science Team (PXTCS) uses economics, behavioral science, statistics, and machine learning to proactively identify mechanisms and process improvements which simultaneously improve Amazon and the lives, wellbeing, and the value of work to Amazonians. We are an interdisciplinary team that combines the talents of science and engineering to develop and deliver solutions that measurably achieve this goal. We are looking for economists who are able to work with business partners to hone complex problems into specific, scientific questions, and test those questions to generate insights. The ideal candidate will work with engineers and computer scientists to estimate models and algorithms on large scale data, design pilots and measure their impact, and transform successful prototypes into improved policies and programs at scale. We are looking for creative thinkers who can combine a strong technical economic toolbox with a desire to learn from other disciplines, and who know how to execute and deliver on big ideas as part of an interdisciplinary technical team. Ideal candidates will work closely with business partners to develop science that solves the most important business challenges. They will work in a team setting with individuals from diverse disciplines and backgrounds. They will serve as an ambassador for science and a scientific resource for business teams, so that scientific processes permeate throughout the HR organization to the benefit of Amazonians and Amazon. Ideal candidates will own the data analysis, modeling, and experimentation that is necessary for estimating and validating models. They will work closely with engineering teams to develop scalable data resources to support rapid insights, and take successful models and findings into production as new products and services. They will be customer-centric and will communicate scientific approaches and findings to business leaders, listening to and incorporate their feedback, and delivering successful scientific solutions. Key job responsibilities Use causal inference methods to evaluate the impact of policies on employee outcomes. Examine how external labor market and economic conditions impact Amazon's ability to hire and retain talent. Use scientifically rigorous methods to develop and recommend career paths for employees. A day in the life Work with teammates to apply economic methods to business problems. This might include identifying the appropriate research questions, writing code to implement a DID analysis or estimate a structural model, or writing and presenting a document with findings to business leaders. Our economists also collaborate with partner teams throughout the process, from understanding their challenges, to developing a research agenda that will address those challenges, to help them implement solutions. About the team We are a multidisciplinary team that combines the talents of science and engineering to develop innovative solutions to make Amazon Earth's Best Employer.
US, WA, Seattle
The People eXperience and Technology Central Science Team (PXTCS) uses economics, behavioral science, statistics, and machine learning to proactively identify mechanisms and process improvements which simultaneously improve Amazon and the lives, wellbeing, and the value of work to Amazonians. We are an interdisciplinary team that combines the talents of science and engineering to develop and deliver solutions that measurably achieve this goal. We are looking for economists who are able to apply economic methods to address business problems. The ideal candidate will work with engineers and computer scientists to estimate models and algorithms on large scale data, design pilots and measure their impact, and transform successful prototypes into improved policies and programs at scale. We are looking for creative thinkers who can combine a strong technical economic toolbox with a desire to learn from other disciplines, and who know how to execute and deliver on big ideas as part of an interdisciplinary technical team. Ideal candidates will work in a team setting with individuals from diverse disciplines and backgrounds. They will work with teammates to develop scientific models and conduct the data analysis, modeling, and experimentation that is necessary for estimating and validating models. They will work closely with engineering teams to develop scalable data resources to support rapid insights, and take successful models and findings into production as new products and services. They will be customer-centric and will communicate scientific approaches and findings to business leaders, listening to and incorporate their feedback, and delivering successful scientific solutions. Key job responsibilities Use causal inference methods to evaluate the impact of policies on employee outcomes. Examine how external labor market and economic conditions impact Amazon's ability to hire and retain talent. Use scientifically rigorous methods to develop and recommend career paths for employees. A day in the life Work with teammates to apply economic methods to business problems. This might include identifying the appropriate research questions, writing code to implement a DID analysis or estimate a structural model, or writing and presenting a document with findings to business leaders. Our economists also collaborate with partner teams throughout the process, from understanding their challenges, to developing a research agenda that will address those challenges, to help them implement solutions. About the team We are a multidisciplinary team that combines the talents of science and engineering to develop innovative solutions to make Amazon Earth's Best Employer.
US, WA, Seattle
Amazon is looking for talented Postdoctoral Scientists to join our global Science teams for a one-year, full-time research position. Postdoctoral Scientists will innovate as members of Amazon’s key global Science teams, including: AWS, Alexa AI, Alexa Shopping, Amazon Style, CoreAI, Last Mile, and Supply Chain Optimization Technologies. Postdoctoral Scientists will join one of may central, global science teams focused on solving research-intense business problems by leveraging Machine Learning, Econometrics, Statistics, and Data Science. Postdoctoral Scientists will work at the intersection of ML and systems to solve practical data driven optimization problems at Amazon scale. Postdocs will raise the scientific bar across Amazon by diving deep into exploratory areas of research to enhance the customer experience and improve efficiencies. Please note: This posting is one of several Amazon Postdoctoral Scientist postings. Please only apply to a maximum of 2 Amazon Postdoctoral Scientist postings that are relevant to your technical field and subject matter expertise. Key job responsibilities * Work closely with a senior science advisor, collaborate with other scientists and engineers, and be part of Amazon’s vibrant and diverse global science community. * Publish your innovation in top-tier academic venues and hone your presentation skills. * Be inspired by challenges and opportunities to invent cutting-edge techniques in your area(s) of expertise.