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.
“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.
“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.
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.
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.”
