Catala is not at all about "proving the law" formally (I'm not even sure what it would mean?). It's about having a formal language to translate law into that both matches the way law is usually written ("default logic") and allows to make numerical computations on. This can typically be used to implement tax or benefits law so that it is way easier to check that the algorithm computing taxes/benefits is correct compared to the actual state of the art of using general purpose programming languages.
If you're interested in this topic, I very warmly recommend the book You're not a rock by Mark Freeman. There are also episodes of podcasts around with interesting interventions from him.
The way I usually pitch the book is that Mark is not an MD, or a scientific expert on the topic, but he is a patient who's been through it, is very interested, and explains to you how it worked for him, and what he knows about the topic like a friend would. There are some mistakes, some things are a bit awkwardly explain, but the book is overall a tremendous read for anyone interested in anything dealing with anxiety, ocd, or more generally a mind too keen on spinning in a wheel.