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.