Towards Formal Specification-Driven Development for the Masses

Speaker: Dr. Son HO
Microsoft Azure Research

Title: Towards Formal Specification-Driven Development for the Masses

Date: Wednesday, 29 April 2026

Time: 4:00pm to 5:00pm

Venue: Room 2405 (via lift 17/18), HKUST

Abstract:

The recent explosion of AI generated code appears as a boon, as it relieves software engineers from tedious programming tasks, making complex software development accessible even to the profane. However, in a world where computer systems have become pervasive, the risk of catastrophic software failures is becoming an increasingly strong concern. Case in point, a single logical defect in the CrowdStrike Falcon platform caused a major worldwide outage a couple of years ago. As humans do not have the physical ability to review the flood of automatically generated code, leaving the door wide open to defects and vulnerabilities, the boon can quickly turn into a curse. Looking at even more recent events, if a company like Amazon is already experiencing outages because of AI assisted code, who knows what will happen tomorrow? We need to address this state of affairs by designing new ways of developing reliable software.

Addressing this challenge requires going beyond testing and code review: we need to have systematic guarantees about the code that gets deployed in production. Recent advances in programming languages and theorem proving might provide a solution. The Rust programming language, by providing memory safety *and* performance through its mechanism of ownership and borrows, is a first answer to putting guardrails on AI-generated code. The Lean theorem prover, with its extensible automation, is a strong candidate to scaling program verification, a set of techniques that leverage mathematical provers to ensure that programs behave according to well-defined mathematical specifications such as, e.g., the absence of crash. In this talk, I propose to combine Rust and Lean to develop *formal*, specification-driven development by scaling automated program verification.

More specifically, I will present the Aeneas toolchain, a formal verification framework that is being used on critical production code in several companies such as Microsoft or Google, and its application to the verification of SymCrypt, Microsoft's open source cryptographic library notably used by Windows and Azure Linux, and that runs on billions of devices. Aeneas crucially leverages Rust's ownership and borrows to translate a large subset of safe Rust to a pure, side-effect free model in Lean, thus abstracting away low-level details about memory and aliasing. Once in Lean, one can leverage a wide range of automation to prove that the Lean model, is, e.g., crash free or functionally correct. The result is a toolchain that is strongly amenable to AI automation: a single AI agent can use it to verify a complete, low-level cryptographic primitive implementation from scratch within a week. This has to be compared to months of expert human work as was traditionally the case in formal verification, and opens the door to the automated generation of formally verified software.

Biography:

Son Ho graduated from École polytechnique in 2017, before working as a research engineer at the ProvenRun company. He then pursued a PhD at Inria under the supervision of Karthikeyan Bhargavan and Jonathan Protzenko, which he successfully defended in late 2024. His dissertation received honorable mentions at both the Gilles-Kahn thesis award, given by the French Academy of Sciences, and the GDR-Security thesis award, given by the French Research Group on Computer Security. He is currently a visiting researcher at Microsoft Azure Research, where he works on securing software systems through program verification.