AVoCat

Catala is a new programming language, designed to be understood by legal experts and to follow the structure of legislative texts, transforming law into code. We propose to explore the automatic verification of Catala programs, in order to obtain tools that for that tax and social security laws satisfy safety and correctness properties, generating concrete counter-examples where appropriate. These tools are intended for use by lawyers and IT specialists in administrations, who translate the law into computer code in order to apply it automatically on massive scales or for economic modeling purposes.