Public administrations are steadily digitalizing all their procedures. In particular, computational laws – such as taxes and social benefits – are increasingly implemented within computers, enabling scalable, automated computations. These implementations have four key features: (i) they are critical software as they can have tremendous negative impact on citizens and states upon failure (e.g., the Phoenix pay system for civil servants in Canada, or the Louvois system for French military); (ii) they require interdisciplinary collaboration between lawyers and computer scientists to be correct; (iii) they are updated regularly by legal changes that can happen on yearly cycles; (iv) they have a long lifespan, counted at least in decades, as most changes are incremental. This talk will provide an overview of works bringing formal methods to legal implementations, using techniques ranging from compilation to automated verification. We will also discuss the impact our community can have on public administrations.

Research Scientist at Inria since Sep. 2022.