Date: Thursday, April 30 2026 – 14h00
Place: B013 (Salle Bob)
Title: Actor Programming and Verification: Specification-Guided Verification and Programming with LLM for Concurrent and Distributed Systems
Actor model of computation (which will soon celebrate its 50th birthday) is introduced by Carl Hewitt at MIT’s AI Lab, and has panned over 30 years for modelling communicating agents. It influenced multi-agent systems, network protocols (such as SOAP), concurrent object programming languages and mathematical models such as logics and concurrent processes. The first part of this talk is to explain how protocol-guided specifications from concurrent actor models are useful for preventing concurrent and communication bugs in distributed systems. Then the second part of this talk will give how this framework is used for actor based language, Rust. However, a talk is very general, so the listeners do not require any knowledge of Rust.
Rust is a modern systems language focused on performance and reliability. Rust is the most beloved programming language since 2016 according to the annual survey by Stack Overflow. Thanks to its efficiency and memory safety, it is now one of the most popular languages of large-scale concurrent applications such as Servo, a browser engine by Firefox, Stratis, a file system manager for Fedora, and Microsoft Azure. Complementing Rust’s promise to provide “fearless concurrency”, developers frequently exploit asynchronous message passing. Unfortunately, sending and receiving messages in an arbitrary order to maximise computation-communication overlap (a popular optimisation in message-passing applications) opens up a Pandora’s box of subtle concurrency bugs. To guarantee deadlock-freedom by construction, we present the toolchain for Rust based on distributed protocol-based specifications and verifications.
I talk about implementation of decentralised distributed Federate Learning protocols in the Rust toolchain and applications of LLM for messaging optimisations.