Legal statutes can contain descriptions of algorithmic decision processes. In that regard, certain domains of the law are thus more “algorithmic” than others. For instance, tax law is about the computation of the amount of taxes owed by an individual, depending on her income and family situation. More interestingly, these legally-defined algorithms are usually enforced by computer programs called legal expert systems, that government agencies or large organizations have been using for decades. Merigoux et al. [2021] cast light on the issues related to the maintenance and production of these legal expert systems, and their faithfulness to their corresponding legislative specification. To tackle those issues, a novel domain-specific language, Catala, was described and formalized in the same paper. By design, Catala programs closely follow the logical structure of legal statutes. Thus, Catala enables a pair programming and literate programming methodology that raises the level of assurance of legal expert systems, while providing a usable toolchain amenable for production deployments.

In this paper, we sketch a system to expand the Catala toolchain into a proof platform for verifying low-level and high-level properties about Catala programs. This system would be based on proof by refinement, a methodology that seeks to simplify the program using semantics-preserving rewritings. Our objective is to enable verification of whole-program properties that could improve our level of assurance about the coherence of the law or its intent as laid out by the legislator.