Rustan Leino, senior principal applied scientist, is seen standing in a lily field, he is smiling toward the camera
Rustan Leino is a senior principal applied scientist in the Automated Reasoning Group at Amazon Web Services. He specializes in program verification, the science of mathematically proving that a software program always functions correctly.

Rustan Leino provides proof that software is bug-free

As a senior principal applied scientist at Amazon Web Services, Leino is continuing his career as a leading expert in program verification.

In Rustan Leino’s ideal world, computer software always works as intended. In the real world, though, he knows that software engineers are people like him — they make mistakes as they write code. Some of these mistakes escape detection. As a result, the world is full of buggy software.

Leino is a senior principal applied scientist in the Automated Reasoning Group at Amazon Web Services (AWS) in Seattle. He specializes in program verification, the science of mathematically proving that a software program always functions correctly. The process of program verification, he noted, is expensive in terms of the hours spent on it — including training. Because of that, it’s done selectively.

Automated reasoning at Amazon
Meet Amazon Science’s newest research area.

“Software that is very important is a great place for verification, and AWS has many pieces of its infrastructure where you just don’t want any mistakes,” he said. “If you want to send a rocket to Mars, you get one chance. You really want it to work. AWS is a little bit like that — you really want it to work.”

Leino spent more than 20 years in industrial research labs studying and developing methods and programming languages for program verification. He joined AWS in 2017 for the opportunity to apply program verification in a setting with real-world impact while continuing to conduct research.

“It is a very happy place for me and a good match with the sorts of things I have expertise in and that AWS wants to do,” he said.

Programming math

Unbeknownst to Leino, he was on the road to a career in program verification as a pre-teen in the early 1980s. He loved math and found a parallel interest in the logic of computer programming. He spent hours each day writing gaming software in the programming language Basic. When he entered the University of Texas at Austin (UT Austin) for his undergraduate degree, he knew he wanted to study computers.

“I don’t think I really knew what computer science was other than it involved programming, but there was a richness to computer science that was revealed to me in college,” he said. “There was one class I took that had to do with program verification, and I really liked it.”

Program verification is a way to catch the mistakes software engineers make when they write programs. At one level, automated program verification tools work in a similar fashion to the way a spell checker works in a word processor.

Rustan Leino on writing verified software for production

“But in the word-processing sense, there’s no equivalent tool of something that says, ‘I’m trying to get my program to do the following,’ or, ‘I’m trying to make sure that my program always makes this particular property hold,’” Leino explained.

Such properties, he explained, are called invariants. To enforce invariants, programmers write specifications — that is, definitions of what a program is supposed to do. Program verification tools called verifiers compare a software program with its invariant specifications and try to find discrepancies or bugs.

“If you can mathematically prove that the program always lives up to those specifications — the things that you’re trying to establish — then you say that you verify the program, or you prove the program correct,” Leino said.

From industry to academia and back

Upon graduation from UT Austin in 1989, Leino got a job as a software developer at Microsoft, where he worked on the Windows operating system. While he was there, he became convinced that formally proving program correctness was going to become more important as computers grew increasingly interconnected.

At the time, program verification was confined to academic and industrial research labs. Leino went to the California Institute of Technology to study it, earning a master's and PhD in computer science along the way.

“When I think back to that, what on earth did I know about research at that time? I don’t know, but somehow in my head, I thought this is what I really wanted to do,” he recalled.

Rustan Leino is seen giving a speech at a wedding, he is holding a microphone and is looking to the side
Rustan Leino says his tenure with AWS has helped move "from using Dafny in research projects to using it in projects with industrial impact."
Sweet Face Photography

During an internship at the Digital Equipment Corporation (DEC), he worked with the late Greg Nelson, a computer scientist who was a pioneer in program verification. DEC hired Leino out of graduate school, and he, Nelson, and their colleagues developed tools such as the Extended Static Checker for Java, a verifier that checks for errors in programs written in Java.

“When a mentor believes in you and lets you develop what you’re good at, it really makes a huge difference,” Leino said of his time working with Nelson. “He did that for me.”

Leino returned to Microsoft in 2001 to join the company’s research lab. There, he developed the intermediate verification language Boogie, which is a building block for many modern program verifiers. Boogie also underpins the programming language Dafny, which Leino developed as a framework to do program verification from the ground up, instead of awkwardly bolting tools onto existing languages.

The research and scientific communities found Dafny useful for tackling a raft of specification challenges. Leino used it to teach program verification to computer scientists, noting that the built-in verification tools encourage programmers to write correct code. Over time, he added more functionalities to Dafny to address other specification challenges of interest to the research community.

“One day I woke up and realized this Dafny thing, it really can do a lot,” he said.

Applied science at AWS

AWS recruited Leino to apply his research on program verification to the Java programs that are mission critical for both internal and external AWS customers. The company saw the value of program verification for its customers and was willing to invest in the science behind it, Leino said.

What’s exciting is that we have now moved the needle from using Dafny in research projects to using it in projects with industrial impact.
Rustan Leino

A few years ago, he was working on a project at AWS that appeared well suited to the capabilities of Dafny. Since then, he’s been working on Dafny full time.

“What’s exciting is that we have now moved the needle from using Dafny in research projects to using it in projects with industrial impact,” Leino said.

For example, his team worked with an engineering group to use Dafny in writing the open-source AWS Encryption Software Development Kit (SDK) for the .NET developer platform. The AWS Encryption SDK is a client-side encryption library that simplifies the tasks of encrypting and decrypting data in cloud applications.

“It’s tricky to apply encryption correctly,” noted Leino. “If customers are going to rely on this library, then it makes sense to go beyond the already rigorous testing that software engineers always do. Program verification steps up the game by providing proofs that the library holds certain properties.”

The specification for one part of the library, for example, holds that when plaintext data is encrypted and broken down into smaller packets for transfer on a wire from one place to another, then the reassembly of these packets on the other side will correctly result in the original plaintext.

“We have proved that works, that there are no mistakes in the assembly/reassembly algorithms,” Leino said. In unverified software, he explained, encryption keys could be applied in the wrong order during assembly, which would make reassembly impossible.

This proof, he added, could give AWS customers greater confidence in applications built with the tool. While there might be other pieces of software in the application that have not gone through the rigor of program verification and thus could have bugs, the piece of the application related to how encryption is applied and packets are assembled is verified correct.

A mentor for the ages

Program verification remains an active area of academic research, with new questions emerging as the discipline becomes more widely embraced. Leino is immersed in that research community and, in that capacity, regularly invites interns to work alongside him. Over the course of his career, 35 have accepted the invitation.

“I tend to work very closely with my interns,” he said. “Most interns I would meet with every day, and many of these 35 interns, we would work probably for an hour or so every day.”

That was the experience of Gaurav Parthasarathy, a PhD student in the programming methodology group in the department of computer science at ETH Zurich in Switzerland who interned with Leino during the summer of 2022. His research focuses on strengthening Boogie, the verification tool that Leino developed and used to build Dafny.

“Once a week we had longer discussions at the white board. It was often him presenting something or me presenting my progress and then us trying to brainstorm how we could solve certain problems,” Parthasarathy said.

Leino said he would often leave these discussions energized to experiment himself, devoting several hours to programming in search of solutions to problems. He looks for a similar passion in his interns.

“Most of the projects that I do involve a lot of programming. We don’t hire science interns to do programming, that’s not the point,” Leino said. “The point is to explore whatever ideas you have. To try them out, you have to do a lot of programming. And so, for me personally, it has always worked out better when programming is something the interns do very fluidly.”

Leino’s passion for programming, experimentation, and discussing the minutiae of program verification ad nauseum struck a chord with Parthasarathy.

“I always thought that if you’re an engineer or a scientist in industry, and you reach Rustan’s age, you move into a management position and you might lose a bit of the passion,” Parthasarathy said. “Rustan showed me that this does not have to be the case. He’s still implementing core features that are really hard to implement — he might be the only one that can even do it. He’s a real scientist at heart.”

Research areas

Related content

US, CA, Palo Alto
Amazon is the 4th most popular site in the US. Our product search engine, one of the most heavily used services in the world, indexes billions of products and serves hundreds of millions of customers world-wide. We are working on a new initiative to transform our search engine into a shopping engine that assists customers with their shopping missions. We look at all aspects of search CX, query understanding, Ranking, Indexing and ask how we can make big step improvements by applying advanced Machine Learning (ML) and Deep Learning (DL) techniques. We’re seeking a thought leader to direct science initiatives for the Search Relevance and Ranking at Amazon. This person will also be a deep learning practitioner/thinker and guide the research in these three areas. They’ll also have the ability to drive cutting edge, product oriented research and should have a notable publication record. This intellectual thought leader will help enhance the science in addition to developing the thinking of our team. This leader will direct and shape the science philosophy, planning and strategy for the team, as we explore multi-modal, multi lingual search through the use of deep learning . We’re seeking an individual that can enhance the science thinking of our team: The org is made of 60+ applied scientists, (2 Principal scientists and 5 Senior ASMs). This person will lead and shape the science philosophy, planning and strategy for the team, as we push into Deep Learning to solve problems like cold start, discovery and personalization in the Search domain. Joining this team, you’ll experience the benefits of working in a dynamic, entrepreneurial environment, while leveraging the resources of Amazon [Earth's most customer-centric internet company]. We provide a highly customer-centric, team-oriented environment in our offices located in Palo Alto, California.
JP, 13, Tokyo
Our mission is to help every vendor drive the most significant impact selling on Amazon. Our team invent, test and launch some of the most innovative services, technology, processes for our global vendors. Our new AVS Professional Services (ProServe) team will go deep with our largest and most sophisticated vendor customers, combining elite client-service skills with cutting edge applied science techniques, backed up by Amazon’s 20+ years of experience in Japan. We start from the customer’s problem and work backwards to apply distinctive results that “only Amazon” can deliver. Amazon is looking for a talented and passionate Applied Science Manager to manage our growing team of Applied Scientists and Business Intelligence Engineers to build world class statistical and machine learning models to be delivered directly to our largest vendors, and working closely with the vendors' senior leaders. The Applied Science Manager will set the strategy for the services to invent, collaborating with the AVS business consultants team to determine customer needs and translating them to a science and development roadmap, and finally coordinating its execution through the team. In this position, you will be part of a larger team touching all areas of science-based development in the vendor domain, not limited to Japan-only products, but collaborating with worldwide science and business leaders. Our current projects touch on the areas of causal inference, reinforcement learning, representation learning, anomaly detection, NLP and forecasting. As the AVS ProServe Applied Science Manager, you will be empowered to expand your scope of influence, and use ProServe as an incubator for products that can be expanded to all Amazon vendors, worldwide. We place strong emphasis on talent growth. As the Applied Science Manager, you will be expected in actively growing future Amazon science leaders, and providing mentoring inside and outside of your team. Key job responsibilities The Applied Science Manager is accountable for: (1) Creating a vision, a strategy, and a roadmap tackling the most challenging business questions from our leading vendors, assess quantitatively their feasibility and entitlement, and scale their scope beyond the ProServe team. (2) Coordinate execution of the roadmap, through direct reports, consisting of scientists and business intelligence engineers. (3) Grow and manage a technical team, actively mentoring, developing, and promoting team members. (4) Work closely with other science managers, program/product managers, and business leadership worldwide to scope new areas of growth, creating new partnerships, and proposing new business initiatives. (5) Act as a technical supervisor, able to assess scientific direction, technical design documents, and steer development efforts to maximize project delivery.
US, NY, New York
Amazon Advertising is one of Amazon's fastest growing and most profitable businesses. As a core product offering within our advertising portfolio, Sponsored Products (SP) helps merchants, retail vendors, and brand owners succeed via native advertising, which grows incremental sales of their products sold through Amazon. The SP team's primary goals are to help shoppers discover new products they love, be the most efficient way for advertisers to meet their business objectives, and build a sustainable business that continuously innovates on behalf of customers. Our products and solutions are strategically important to enable our Retail and Marketplace businesses to drive long-term growth. We deliver billions of ad impressions and millions of clicks and break fresh ground in product and technical innovations every day! The Supply team (within Sponsored Products) is looking for an Applied Scientist to join a fast-growing team with the mandate of creating new ad experiences that elevate the shopping experience for hundreds of millions customers worldwide. The Applied Scientist will take end-to-end ownership of driving new product/feature innovation by applying advanced statistical and machine learning models. The role will handle petabytes of unstructured data (images, text, videos) to extract insights into what metadata can be useful for us to highlight to simplify purchase decisions, and propose new experiences that increase shopper engagement. Why you love this opportunity Amazon is investing heavily in building a world-class advertising business. This team is responsible for defining and delivering a collection of advertising products that drive discovery and sales. Our solutions generate billions in revenue and drive long-term growth for Amazon’s Retail and Marketplace businesses. We deliver billions of ad impressions, millions of clicks daily, and break fresh ground to create world-class products. We are highly motivated, collaborative, and fun-loving team with an entrepreneurial spirit - with a broad mandate to experiment and innovate. Key job responsibilities As an Applied Scientist on this team you will: Build machine learning models and perform data analysis to deliver scalable solutions to business problems. Perform hands-on analysis and modeling with very large data sets to develop insights that increase traffic monetization and merchandise sales without compromising shopper experience. Work closely with software engineers on detailed requirements, technical designs and implementation of end-to-end solutions in production. Design and run A/B experiments that affect hundreds of millions of customers, evaluate the impact of your optimizations and communicate your results to various business stakeholders. Work with scientists and economists to model the interaction between organic sales and sponsored content and to further evolve Amazon's marketplace. Establish scalable, efficient, automated processes for large-scale data analysis, machine-learning model development, model validation and serving. Research new predictive learning approaches for the sponsored products business. Write production code to bring models into production. A day in the life You will invent new experiences and influence customer-facing shopping experiences to help suppliers grow their retail business and the auction dynamics that leverage native advertising; this is your opportunity to work within the fastest-growing businesses across all of Amazon! Define a long-term science vision for our advertising business, driven fundamentally from our customers' needs, translating that direction into specific plans for research and applied scientists, as well as engineering and product teams. This role combines science leadership, organizational ability, technical strength, product focus, and business understanding.
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 are seeking a Principal Scientist with deep expertise in Search. Your responsibility will be to advance the state-of-the-art for search science that leads to world-class products that impact Amazon's customers. Key job responsibilities You will be responsible for defining key research directions, adopting or inventing new machine learning techniques, conducting rigorous experiments, publishing results, and ensuring that research is translated into practice. You will develop long-term strategies, persuade teams to adopt those strategies, propose goals and deliver on them. You will 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 This is a position on Core Ranking and Experimentation team in Palo Alto, CA. The team works on a variety of topics in search ranking and relevance, such as multi-objective optimization, personalization, and fast online experimentation. We work closely with teams in various parts of the stack to ensure that our science is translated to customer facing products.
US, WA, Bellevue
Amazon is looking for a passionate, talented, and inventive Applied Scientists with a strong machine learning background to help build industry-leading Speech and Language technology. Our mission is to provide a delightful experience to Amazon’s customers by pushing the envelope in Automatic Speech Recognition (ASR), Machine Translation (MT), Natural Language Understanding (NLU), Machine Learning (ML) and Computer Vision (CV). As part of our AI team in Amazon AWS, you will work alongside internationally recognized experts to develop novel algorithms and modeling techniques to advance the state-of-the-art in human language technology. Your work will directly impact millions of our customers in the form of products and services that make use of speech and language technology. You will gain hands on experience with Amazon’s heterogeneous speech, text, and structured data sources, and large-scale computing resources to accelerate advances in spoken language understanding. We are hiring in all areas of human language technology: ASR, MT, NLU, text-to-speech (TTS), and Dialog Management, in addition to Computer Vision.
IN, KA, Bangalore
Amazon is investing heavily in building a world class advertising business and we are responsible for defining and delivering a collection of self-service performance advertising products that drive discovery and sales. Our products are strategically important to our Retail and Marketplace businesses driving long term growth. We deliver billions of ad impressions and millions of clicks daily and are breaking fresh ground to create world-class products. The ATT team, based in Bangalore, is responsible for ensuring that ads are compliant to world-wide advertising policies and are of high quality, leading to higher conversion for the advertisers and providing a great experience for the shoppers. Machine learning, particularly multi-modal data understanding, is fundamental to the way we drive our business, meet our goals and satisfy our customers. ATT team invests in researching and developing state of art models that analyze various type of ad assets – text, audio, images and videos - to ensure compliance to advertising policies. We also help advertisers create more successful ads by creating ML models to assist ad generation as well as to provide data-driven interpretable insights. Key job responsibilities Major responsibilities · Deliver key goals to enhance advertiser experience and protect shopper trust by innovative use of computer vision, NLP and statistical techniques · Drive core business analytics and data science explorations to inform key business decisions and algorithm roadmap · Establish scalable, efficient, automated processes for large scale data analyses, model development, model validation and model implementation · Hire and develop top talent in machine learning and data science and accelerate the pace of innovation in the group · Work proactively with engineering teams and product managers to evangelize new algorithms and drive the implementation of large-scale complex ML models in production
US, WA, Seattle
We are seeking a talented applied researcher to join the Search team responsible for developing reinforcement learning systems for Amazon's shopping experience and delivering it to millions of customers. We believe that shopping on Amazon should be simple, delightful, and full of "wow" moments for everyone.
US, NY, New York
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 Python is necessary, and experience with SQL and UNIX 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, scientists, and product managers. 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. About the team Amazon's Weblab team enables experimentation at massive scale to help Amazon build better products for customers. A/B testing is in Amazon's DNA and we're at the core of how Amazon innovates on behalf of customers.
US, WA, Seattle
Amazon Advertising is one of Amazon's fastest growing and most profitable businesses, responsible for defining and delivering a collection of advertising products that drive discovery and sales. As a core product offering within our advertising portfolio, Sponsored Products (SP) helps merchants, retail vendors, and brand owners succeed via native advertising, which grows incremental sales of their products sold through Amazon. The SP team's primary goals are to help shoppers discover new products they love, be the most efficient way for advertisers to meet their business objectives, and build a sustainable business that continuously innovates on behalf of customers. Our products and solutions are strategically important to enable our Retail and Marketplace businesses to drive long-term growth. We deliver billions of ad impressions and millions of clicks and break fresh ground in product and technical innovations every day! As an Applied Science Manager in Machine Learning, you will: Directly manage and lead a cross-functional team of Applied Scientists, Data Scientists, Economists, and Business Intelligence Engineers. Develop and manage a research agenda that balances short term deliverables with measurable business impact as well as long term investments. Lead marketplace design and development based on economic theory and data analysis. Provide technical and scientific guidance to team members. Rapidly design, prototype and test many possible hypotheses in a high-ambiguity environment, making use of both quantitative and business judgment Advance the team's engineering craftsmanship and drive continued scientific innovation as a thought leader and practitioner. Develop science and engineering roadmaps, run annual planning, and foster cross-team collaboration to execute complex projects. Perform hands-on data analysis, build machine-learning models, run regular A/B tests, and communicate the impact to senior management. Collaborate with business and software teams across Amazon Ads. Stay up to date with recent scientific publications relevant to the team. Hire and develop top talent, provide technical and career development guidance to scientists and engineers within and across the organization. Why you will love this opportunity: Amazon is investing heavily in building a world-class advertising business. This team defines and delivers a collection of advertising products that drive discovery and sales. Our solutions generate billions in revenue and drive long-term growth for Amazon’s Retail and Marketplace businesses. We deliver billions of ad impressions, millions of clicks daily, and break fresh ground to create world-class products. We are a highly motivated, collaborative, and fun-loving team with an entrepreneurial spirit - with a broad mandate to experiment and innovate. Impact and Career Growth: You will invent new experiences and influence customer-facing shopping experiences to help suppliers grow their retail business and the auction dynamics that leverage native advertising; this is your opportunity to work within the fastest-growing businesses across all of Amazon! Define a long-term science vision for our advertising business, driven from our customers' needs, translating that direction into specific plans for research and applied scientists, as well as engineering and product teams. This role combines science leadership, organizational ability, technical strength, product focus, and business understanding. Team video ~ https://youtu.be/zD_6Lzw8raE
US, CA, Palo Alto
The Amazon Search team creates powerful, customer-focused search and advertising 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. Our Search Relevance team works to maximize the quality and effectiveness of the search experience for visitors to Amazon websites worldwide. Amazon’s large scale brings with it unique problems to solve in designing, testing, and deploying relevance models. We are seeking a strong applied Scientist to join the Experimentation Infrastructure and Methods team. This team’s charter is to innovate and evaluate ranking at Amazon Search. In practice, we aim to create infrastructure and metrics, enable new experimental methods, and do proof-of-concept experiments, that enable Search Relevance teams to introduce new features faster, reduce the cost of experimentation, and deliver faster against Search goals. Key job responsibilities You will build search ranking systems and evaluation framework that extend to Amazon scale -- thousands of product types, billions of queries, and hundreds of millions of customers spread around the world. As a Senior Applied Scientist you will find the next set of big improvements to ranking evaluation, get your hands dirty by building models to help understand complexities of customer behavior, and mentor junior engineers and scientists. In addition to typical topics in ranking, we are particularly interested in evaluation, feature selection, explainability. A day in the life Our primary focus is improving search ranking systems. On a day-to-day this means building ML models, analyzing data from your recent A/B tests, and guiding teams on best practices. You will also find yourself in meetings with business and tech leaders at Amazon communicating your next big initiative. About the team We are a team consisting of software engineers and applied scientists. Our interests and activities span machine learning for better ranking, experimentation, statistics for better decision making, and infrastructure to make it all happen efficiently at scale.