# Catala: A Programming Language for the Law

arXiv: https://arxiv.org/abs/2103.03198 · HTML: https://mlsanity.com/paper/2103.03198/

## Key facts

- Cited by 20 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Mar 2021.

## Built on by (most cited first, 20 of 20)

- [A Neurosymbolic Approach to Natural Language Formalization and Verification](https://mlsanity.com/paper/2511.09008/) (2025)
- [A Certified Proof Checker for Deep Neural Network Verification in Imandra](https://mlsanity.com/paper/2405.10611/) (2024)
- [Enhancing Logical Reasoning in Large Language Models to Facilitate Legal Applications](https://mlsanity.com/paper/2311.13095/) (2023)
- [Software Engineering Methods For AI-Driven Deductive Legal Reasoning](https://mlsanity.com/paper/2404.09868/) (2024)
- [Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning](https://mlsanity.com/paper/2606.16118/) (2026)
- [Can LLMs Identify Tax Abuse?](https://mlsanity.com/paper/2508.20097/) (2025)
- [Automated legal reasoning with discretion to act using s(LAW)](https://mlsanity.com/paper/2401.14511/) (2024)
- [Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline](https://mlsanity.com/paper/2604.18882/) (2026)
- [An NLG pipeline for a legal expert system: a work in progress](https://mlsanity.com/paper/2107.02421/) (2021)
- [Automating Defeasible Reasoning in Law](https://mlsanity.com/paper/2205.07335/) (2022)
- [Artificial intelligence and renegotiation of commercial lease contracts affected by pandemic-related contingencies from Covid-19. The project A.I.A.Co](https://mlsanity.com/paper/2210.09515/) (2022)
- [Envisioning a Human-AI collaborative system to transform policies into decision models](https://mlsanity.com/paper/2212.06882/) (2022)
- [Le Nozze di Giustizia. Interactions between Artificial Intelligence, Law, Logic, Language and Computation with some case studies in Traffic Regulations and Health Care](https://mlsanity.com/paper/2402.06487/) (2024)
- [Code-Driven Law NO, Normware SI!](https://mlsanity.com/paper/2410.17257/) (2024)
- [Rule-State Inference (RSI): A Bayesian Framework for Compliance Monitoring in Rule-Governed Domains](https://mlsanity.com/paper/2603.21610/) (2026)
- [GDPR Auto-Formalization with AI Agents and Human Verification](https://mlsanity.com/paper/2604.14607/) (2026)
- [By Their Fruits You Will Know Them: Comparing Formalizations of Law by the Decisions They Encode](https://mlsanity.com/paper/2605.25186/) (2026)
- [Time as Structure: Temporal Dependency Graphs for Verifiable Deadline Computation over Legal Documents](https://mlsanity.com/paper/2608.15270/) (2026)
- [Detecting Inconsistencies in Model Specifications with LLM-as-Verifier Reasoning](https://mlsanity.com/paper/2610.01847/) (2026)
- [Law And Order: Tax Law Autoformalization](https://mlsanity.com/paper/2610.02792/) (2026)

## Abstract (arXiv)

Law at large underpins modern society, codifying and governing many aspects of citizens' daily lives. Oftentimes, law is subject to interpretation, debate and challenges throughout various courts and jurisdictions. But in some other areas, law leaves little room for interpretation, and essentially aims to rigorously describe a computation, a decision procedure or, simply said, an algorithm. Unfortunately, prose remains a woefully inadequate tool for the job. The lack of formalism leaves room for ambiguities; the structure of legal statutes, with many paragraphs and sub-sections spread across multiple pages, makes it hard to compute the intended outcome of the algorithm underlying a given text; and, as with any other piece of poorly-specified critical software, the use of informal language leaves corner cases unaddressed. We introduce Catala, a new programming language that we specifically designed to allow a straightforward and systematic translation of statutory law into an executable implementation. Catala aims to bring together lawyers and programmers through a shared medium, which together they can understand, edit and evolve, bridging a gap that often results in dramatically incorrect implementations of the law. We have implemented a compiler for Catala, and have proven the correctness of its core compilation steps using the F* proof assistant. We evaluate Catala on several legal texts that are algorithms in disguise, notably section 121 of the US federal income tax and the byzantine French family benefits; in doing so, we uncover a bug in the official implementation. We observe as a consequence of the formalization process that using Catala enables rich interactions between lawyers and programmers, leading to a greater understanding of the original legislative intent, while producing a correct-by-construction executable specification reusable by the greater software ecosystem.