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, Santa Clara
Machine learning (ML) has been strategic to Amazon from the early years. We are pioneers in areas such as recommendation engines, product search, eCommerce fraud detection, and large-scale optimization of fulfillment center operations. The Generative AI team helps AWS customers accelerate the use of Generative AI to solve business and operational challenges and promote innovation in their organization. As an applied scientist, you are proficient in designing and developing advanced ML models to solve diverse challenges and opportunities. You will be working with terabytes of text, images, and other types of data to solve real-world problems. You'll design and run experiments, research new algorithms, and find new ways of optimizing risk, profitability, and customer experience. We’re looking for talented scientists capable of applying ML algorithms and cutting-edge deep learning (DL) and reinforcement learning approaches to areas such as drug discovery, customer segmentation, fraud prevention, capacity planning, predictive maintenance, pricing optimization, call center analytics, player pose estimation, event detection, and virtual assistant among others. AWS Sales, Marketing, and Global Services (SMGS) is responsible for driving revenue, adoption, and growth from the largest and fastest growing small- and mid-market accounts to enterprise-level customers including public sector. The AWS Global Support team interacts with leading companies and believes that world-class support is critical to customer success. AWS Support also partners with a global list of customers that are building mission-critical applications on top of AWS services. Key job responsibilities The primary responsibilities of this role are to: Design, develop, and evaluate innovative ML models to solve diverse challenges and opportunities across industries Interact with customer directly to understand their business problems, and help them with defining and implementing scalable Generative AI solutions to solve them Work closely with account teams, research scientist teams, and product engineering teams to drive model implementations and new solutions About the team Diverse Experiences AWS values diverse experiences. Even if you do not meet all of the qualifications and skills listed in the job description, we encourage candidates to apply. If your career is just starting, hasn’t followed a traditional path, or includes alternative experiences, don’t let it stop you from applying. Why AWS? Amazon Web Services (AWS) is the world’s most comprehensive and broadly adopted cloud platform. We pioneered cloud computing and never stopped innovating — that’s why customers from the most successful startups to Global 500 companies trust our robust suite of products and services to power their businesses. Inclusive Team Culture Here at AWS, it’s in our nature to learn and be curious. Our employee-led affinity groups foster a culture of inclusion that empower us to be proud of our differences. Ongoing events and learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences, inspire us to never stop embracing our uniqueness. Mentorship & Career Growth We’re continuously raising our performance bar as we strive to become Earth’s Best Employer. That’s why you’ll find endless knowledge-sharing, mentorship and other career-advancing resources here to help you develop into a better-rounded professional. Work/Life Balance We value work-life harmony. Achieving success at work should never come at the expense of sacrifices at home, which is why flexible work hours and arrangements are part of our culture. When we feel supported in the workplace and at home, there’s nothing we can’t achieve in the cloud. We are open to hiring candidates to work out of one of the following locations: San Francisco, CA, USA | Santa Clara, CA, USA
US, NY, New York
We are looking for a motivated and experienced Senior Data Scientist with experience in Machine Learning (ML), Artificial Intelligence (AI), Big Data, and Service Oriented Architecture with deep understanding in advertising businesses, to be part of a team of talented scientists and engineers to innovate, iterate, and solve real world problem with cutting-edge AWS technologies. In this role, you will take a leading role in defining the problem, innovating the ML/AI solutions, and information the tech roadmap. You will join a cross-functional, fun-loving team, working closely with scientists and engineers in a daily basis. You will innovate on behalf of our customers by prototyping, delivering functional proofs of concept (POCs), and partnering with our engineers to productize and scale successful POCs. If you are passionate about creating the future, come join us as we have fun, and make history. Key job responsibilities - Define and execute a research & development roadmap that drives data-informed decision making for marketers and advertisers - Establish and drive data hygiene best practices to ensure coherence and integrity of data feeding into production ML/AI solutions - Collaborate with colleagues across science and engineering disciplines for fast turnaround proof-of-concept prototyping at scale - Partner with product managers and stakeholders to define forward-looking product visions and prospective business use cases - Drive and lead of culture of data-driven innovations within and outside across Amazon Ads Marketing orgs About the team Marketing Decision Science provides science products to enable Amazon Ads Marketing to deliver relevant and compelling guidance across marketing channels to prospective and active advertisers for success on Amazon. We own the product, technology and deployment roadmap for AI- and analytics-powered products across Amazon Ads Marketing. We analyze the needs, experiences, and behaviors of Amazon advertisers at petabytes scale, to deliver the right marketing communications to the right advertiser at the right team to help them make the data-informed advertising decisions. Our science-based products enable applications and synergies across Ads organization, spanning marketing, product, and sales use cases. We are open to hiring candidates to work out of one of the following locations: New York, NY, USA
US, WA, Bellevue
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 previous cohorts have converted to full time scientist employment at Amazon. If you are interested, please send your CV to our mailing list at econ-internship@amazon.com. We are open to hiring candidates to work out of one of the following locations: Bellevue, WA, USA
US, WA, Seattle
Are you excited about developing models to revolutionize automation, robotics and computer vision? Are you looking for opportunities to build and deploy them on real problems at truly vast scale? At Amazon Fulfillment Technologies and Robotics we are on a mission to build high-performance autonomous systems that perceive and act to further improve our world-class customer experience - at Amazon scale. We are looking for scientists, engineers and program managers for a variety of roles. The Amazon Robotics software team is seeking a collaborative Applied Scientist to focus on computer vision machine learning models. This includes building multi-viewpoint and time-series computer vision systems. It includes building large-scale models using data from many different tasks and scenes. This work spans from basic research such as cross domain training, to experimenting on prototype in the lab, to running wide-scale A/B tests on robots in our facilities. Key job responsibilities * Research vision - Where should we be focusing our efforts * Research delivery – Proving/dis-proving strategies in offline data or in the lab * Production studies - Insights from production data or ad-hoc experimentation. A day in the life Amazon offers a full range of benefits that support you and eligible family members, including domestic partners and their children. Benefits can vary by location, the number of regularly scheduled hours you work, length of employment, and job status such as seasonal or temporary employment. The benefits that generally apply to regular, full-time employees include: 1. Medical, Dental, and Vision Coverage 2. Maternity and Parental Leave Options 3. Paid Time Off (PTO) 4. 401(k) Plan If you are not sure that every qualification on the list above describes you exactly, we'd still love to hear from you! At Amazon, we value people with unique backgrounds, experiences, and skillsets. If you’re passionate about this role and want to make an impact on a global scale, please apply! We are open to hiring candidates to work out of one of the following locations: Seattle, WA, USA
US, WA, Bellevue
Looking for your next challenge? North America Sort Centers (NASC) are experiencing growth and looking for a skilled, highly motivated Data Scientist to join the NASC Engineering Data, Product and Simulation Team. The Sort Center network is the critical Middle-Mile solution in the Amazon Transportation Services (ATS) group, linking Fulfillment Centers to the Last Mile. The experience of our customers is dependent on our ability to efficiently execute volume flow through the middle-mile network. Key job responsibilities The Senior Data Scientist will design and implement solutions to address complex business questions using simulation. In this role, you will apply advanced analysis techniques and statistical concepts to draw insights from massive datasets, and create intuitive simulations and data visualizations. You can contribute to each layer of a data solution – you work closely with process design engineers, business intelligence engineers and technical product managers to obtain relevant datasets and create simulation models, and review key results with business leaders and stakeholders. Your work exhibits a balance between scientific validity and business practicality. On this team, you will have a large impact on the entire NASC organization, with lots of opportunity to learn and grow within the NASC Engineering team. This role will be the first dedicated simulation expert, so you will have an exceptional opportunity to define and drive vision for simulation best practices on our team. To be successful in this role, you must be able to turn ambiguous business questions into clearly defined problems, develop quantifiable metrics and deliver results that meet high standards of data quality, security, and privacy. About the team NASC Engineering’s Product and Analytics Team’s sole objective is to develop tools for under the roof simulation and optimization, supporting the needs of our internal and external stakeholders (i.e Process Design Engineering, NASC Engineering, ACES, Finance, Safety and Operations). We develop data science tools to evaluate what-if design and operations scenarios for new and existing sort centers to understand their robustness, stability, scalability, and cost-effectiveness. We conceptualize new data science solutions, using optimization and machine learning platforms, to analyze new and existing process, identify and reduce non-value added steps, and increase overall performance and rate. We work by interfacing with various functional teams to test and pilot new hardware/software solutions. We are open to hiring candidates to work out of one of the following locations: Bellevue, WA, USA
IN, KA, Bangalore
Alexa is the voice activated digital assistant powering devices like Amazon Echo, Echo Dot, Echo Show, and Fire TV, which are at the forefront of this latest technology wave. To preserve our customers’ experience and trust, the Alexa Sensitive Content Intelligence (ASCI) team creates policies and builds services and tools through Machine Learning techniques to detect and mitigate sensitive content across Alexa. We are looking for an experienced Senior Applied Scientist to build industry-leading technologies in attribute extraction and sensitive content detection across all languages and countries. An Applied Scientist will be a tech lead for a team of exceptional scientists to develop novel algorithms and modeling techniques to advance the state of the art in NLP or CV related tasks. You will work in a hybrid, fast-paced organization where scientists, engineers, and product managers work together to build customer facing experiences. You will collaborate with and mentor other scientists to raise the bar of scientific research in Amazon. Your work will directly impact our customers in the form of products and services that make use of speech, language, and computer vision technologies. We are looking for a leader with strong technical experiences a passion for building scientific driven solutions in a fast-paced environment. You should have good understanding of NLP models (e.g. LSTM, transformer based models) or CV models (e.g. CNN, AlexNet, ResNet) and where to apply them in different business cases. You leverage your exceptional technical expertise, a sound understanding of the fundamentals of Computer Science, and practical experience of building large-scale distributed systems to creating reliable, scalable, and high-performance products. In addition to technical depth, you must possess exceptional communication skills and understand how to influence key stakeholders. You will be joining a select group of people making history producing one of the most highly rated products in Amazon's history, so if you are looking for a challenging and innovative role where you can solve important problems while growing as a leader, this may be the place for you. Key job responsibilities You'll lead the science solution design, run experiments, research new algorithms, and find new ways of optimizing customer experience. You set examples for the team on good science practice and standards. Besides theoretical analysis and innovation, you will work closely with talented engineers and ML scientists to put your algorithms and models into practice. Your work will directly impact the trust customers place in Alexa, globally. You contribute directly to our growth by hiring smart and motivated Scientists to establish teams that can deliver swiftly and predictably, adjusting in an agile fashion to deliver what our customers need. A day in the life You will be working with a group of talented scientists on researching algorithm and running experiments to test scientific proposal/solutions to improve our sensitive contents detection and mitigation. This will involve collaboration with partner teams including engineering, PMs, data annotators, and other scientists to discuss data quality, policy, and model development. You will mentor other scientists, review and guide their work, help develop roadmaps for the team. You work closely with partner teams across Alexa to deliver platform features that require cross-team leadership. About the hiring group About the team The mission of the Alexa Sensitive Content Intelligence (ASCI) team is to (1) minimize negative surprises to customers caused by sensitive content, (2) detect and prevent potential brand-damaging interactions, and (3) build customer trust through appropriate interactions on sensitive topics. The term “sensitive content” includes within its scope a wide range of categories of content such as offensive content (e.g., hate speech, racist speech), profanity, content that is suitable only for certain age groups, politically polarizing content, and religiously polarizing content. The term “content” refers to any material that is exposed to customers by Alexa (including both 1P and 3P experiences) and includes text, speech, audio, and video. We are open to hiring candidates to work out of one of the following locations: Bangalore, KA, IND
US, WA, Seattle
Innovators wanted! Are you an entrepreneur? A builder? A dreamer? This role is part of an Amazon Special Projects team that takes the company’s Think Big leadership principle to the extreme. We focus on creating entirely new products and services with a goal of positively impacting the lives of our customers. No industries or subject areas are out of bounds. If you’re interested in innovating at scale to address big challenges in the world, this is the team for you. Here at Amazon, we embrace our differences. We are committed to furthering our culture of inclusion. We have thirteen employee-led affinity groups, reaching 40,000 employees in over 190 chapters globally. We are constantly learning through programs that are local, regional, and global. Amazon’s culture of inclusion is reinforced within our 16 Leadership Principles, which remind team members to seek diverse perspectives, learn and be curious, and earn trust. Our team highly values work-life balance, mentorship and career growth. We believe striking the right balance between your personal and professional life is critical to life-long happiness and fulfillment. We care about your career growth and strive to assign projects and offer training that will challenge you to become your best. We are open to hiring candidates to work out of one of the following locations: Seattle, WA, USA
US, MA, North Reading
We are looking for experienced scientists and engineers to explore new ideas, invent new approaches, and develop new solutions in the areas of Controls, Dynamic modeling and System identification. Are you inspired by invention? Is problem solving through teamwork in your DNA? Do you like the idea of seeing how your work impacts the bigger picture? Answer yes to any of these and you’ll fit right in here at Amazon Robotics. We are a smart team of doers that work passionately to apply cutting edge advances in robotics and software to solve real-world challenges that will transform our customers’ experiences in ways we can’t even imagine yet. We invent new improvements every day. We are Amazon Robotics and we will give you the tools and support you need to invent with us in ways that are rewarding, fulfilling and fun. Key job responsibilities Applied Scientists take on big unanswered questions and guide development team to state-of-the-art solutions. We want to hear from you if you have deep industry experience in the Mechatronics domain and : * the ability to think big and conceive of new ideas and novel solutions; * the insight to correctly identify those worth exploring; * the hands-on skills to quickly develop proofs-of-concept; * the rigor to conduct careful experimental evaluations; * the discipline to fast-fail when data refutes theory; * and the fortitude to continue exploring until your solution is found We are open to hiring candidates to work out of one of the following locations: North Reading, MA, USA | Westborough, MA, USA
GB, London
Are you excited about applying economic models and methods using large data sets to solve real world business problems? Then join the Economic Decision Science (EDS) team. EDS is an economic science team based in the EU Stores business. The teams goal is to optimize and automate business decision making in the EU business and beyond. An internship at Amazon is an opportunity to work with leading economic researchers on influencing needle-moving business decisions using incomparable datasets and tools. It is an opportunity for PhD students and recent PhD graduates in Economics or related fields. We are looking for detail-oriented, organized, and responsible individuals who are eager to learn how to work with large and complicated data sets. Knowledge of econometrics, as well as basic familiarity with Stata, R, or Python is necessary. Experience with SQL would be a plus. As an Economics Intern, you will be working in a fast-paced, cross-disciplinary team of researchers who are pioneers in the field. You will take on complex problems, and work on solutions that either leverage existing academic and industrial research, or utilize your own out-of-the-box pragmatic thinking. In addition to coming up with novel solutions and prototypes, you may even need to deliver these to production in customer facing products. Roughly 85% of previous intern cohorts have converted to full time scientist employment at Amazon. We are open to hiring candidates to work out of one of the following locations: London, GBR
GB, London
Are you excited about applying economic models and methods using large data sets to solve real world business problems? Then join the Economic Decision Science (EDS) team. EDS is an economic science team based in the EU Stores business. The teams goal is to optimize and automate business decision making in the EU business and beyond. An internship at Amazon is an opportunity to work with leading economic researchers on influencing needle-moving business decisions using incomparable datasets and tools. It is an opportunity for PhD students and recent PhD graduates in Economics or related fields. We are looking for detail-oriented, organized, and responsible individuals who are eager to learn how to work with large and complicated data sets. Knowledge of econometrics, as well as basic familiarity with Stata, R, or Python is necessary. Experience with SQL would be a plus. As an Economics Intern, you will be working in a fast-paced, cross-disciplinary team of researchers who are pioneers in the field. You will take on complex problems, and work on solutions that either leverage existing academic and industrial research, or utilize your own out-of-the-box pragmatic thinking. In addition to coming up with novel solutions and prototypes, you may even need to deliver these to production in customer facing products. Roughly 85% of previous intern cohorts have converted to full time scientist employment at Amazon. We are open to hiring candidates to work out of one of the following locations: London, GBR