22 September 2026

Rifat Jumagulov · How this is checked

Law as Function, Law as Data: What Catala and Arxo Compute When They Read the Same Regulation

Two formalizations of one Kazakh regulation agreed on 65 reference cases and 240 random ones. Catala returns a value; Arxo returns a proof. Where the agreement ends is where each paradigm begins.

Two independent formalizations of the same regulation, written in two different languages, agreed on every one of 65 reference cases and 240 randomly generated ones. That result is the starting point of this article, not its conclusion. Where two systems built on different foundations agree, the interesting question is what each of them computes beyond the point where the agreement ends.

Catala, developed at Inria, is the reference for engineering rigour in computational law. Its core compilation step is proven correct in the F* proof assistant, its compiler emits OCaml, Python, C and Java, and it has moved from research into administration: a proof of concept at the French tax authority (DGFiP) in 2023–2024, adoption by the French family-benefits fund (CNAF) as its reference technology for benefit calculation after a 2024–2025 experiment, a partnership convention signed in June 2026, and a 2026 proof of concept for agricultural aid at the ASP. In 2026 the project received the first Scientific Interdisciplinarity Award of the Collège des sociétés savantes académiques de France, the CNRS and France Universités.

Arxo Law is built on a different premise. In Catala, a statute becomes a function: inputs go in, a value comes out, and the compiler guarantees the value follows the annotated text. In Arxo, a statute becomes data: a package of norms with byte-pinned sources, deontic positions, priorities, interpretations and editions, which an engine executes to produce a proof graph rather than a value. Both premises are principled. They answer different questions, and this article uses one shared regulation to show where each question begins.

The parity experiment

The material is a Kazakh regulation: the Rules for Determining the Amount of Damage Caused to a Vehicle (Resolution No. 14 of the Board of the National Bank of the Republic of Kazakhstan, 28 January 2016). It is a compact by-law with the shape that formal methods handle best: thresholds, percentages, deadlines counted in working days, and a small set of conditions on inspections and documents.

The computational part of the Rules was implemented twice, independently, from the official text:

• in Catala 1.2.0, as six scopes covering total loss, part cost, choice of appraisers, admissibility of inspection, deadlines, and the final amount;
• in Arxo Law, as a package whose 67 rules cover the same points plus the parts of the regulation that a function cannot carry.

Expected outcomes for 65 reference cases were established by hand from the text and the 2026 official calendar, with a written justification for each. The same 65 cases were then run through Catala and through both Arxo evaluators (the Rust engine and the Python reference implementation), and a property-based run generated 240 further random cases across two seeds, checked against a Python oracle written directly from the text.

The single known semantic difference between the two languages was isolated on purpose. Catala stores money to the cent and rounds a money-times-decimal product; Arxo keeps money exact and rounds only where the text says so. The comparison was therefore fixed at whole tenge, which is also what the regulation itself requires of the final amount.

A second, smaller data point comes from France. Arxo's formalization of the rental-sector housing benefit (APL) was checked against the ten test cases published in Catala's own examples repository. All ten matched to the cent, and the intermediate quantities were verified in separate scenarios (13 September 2026).

The conclusion of both experiments is the same. Where a norm states an algorithm, both languages reproduce it faithfully and identically. Everything that follows is about what lies beyond the algorithm. The vehicle-damage experiment is public: both models, the 65 reference cases, the runners and the recorded results are at github.com/arxohq/arxo-catala-parity.

Axis 1: a value versus a certificate

The clearest architectural difference is what a single call returns.

A Catala scope returns a value: a number, a boolean, an optional. This is the right product for microsimulation, where a rules engine runs over millions of households and the only thing that matters is the number at the end. The Catala interpreter computed one total-loss case in about 16 microseconds in our measurement, and the compiled backends, which we did not benchmark, are designed to be faster still.

An Arxo call returns an evaluation document: a manifest of inputs, the results, a proof graph with every rule application and every fact it rested on, the deontic positions in force, any registered conflicts, the issues raised, and content hashes that make the whole document reproducible. On a trivial vector this document is about three kilobytes, and those bytes are what the two Arxo evaluators compare against each other. One such call cost about 0.4 milliseconds in the Rust engine and about 2.5 milliseconds in the Python reference implementation, on the same machine and the same regulation.

Catala is faster because it is doing a smaller job, and doing it very well. Arxo spends its time on fact storage, a fixed-point computation over the rules, canonical serialization and hashing, because the product is a certificate of how the answer was reached. The profile of the Rust engine shows where the cost goes: string comparison, map lookups and allocation account for most of it, the solver itself for under one percent. These are two different products, and the timing gap is the price of one of them, not an inefficiency in the other.

Measurement conditions: Apple Silicon, macOS 24.6, warm runs, 9 September 2026. Catala: the Gibel scope called 10,000 times inside one process, the cost of a single-call run subtracted. Arxo: the engine's test runner over the parity scenarios, the cost of a one-test run subtracted. Process start and model loading were about 40 ms for Catala and about 10 ms for the Rust engine.

Axis 2: default calculus versus four-valued support

Catala's core is the prioritized default calculus. Each variable is defined once by a base rule and a tree of exceptions with a static priority order. If exactly one exception applies, it wins; if none applies, the base rule holds; if two exceptions of equal priority apply, the program raises a conflict error and produces no value. The world is closed: a variable has exactly one value or the computation fails.

Arxo's core is a four-valued support relation with defeasible rules that preserve ambiguity. A query can be established (TRUE_ONLY), refuted (FALSE_ONLY), supported on both sides (BOTH), or unsupported (NEITHER). Silence is not negation: a fact that was never asserted does not make the opposite true.

For a lawyer these two models answer differently in two common situations.

A fact is missing. In the Catala model we wrote, a missing input is either an omitted optional that flows through as absence, or a boolean that defaults to false. In Arxo, the query is NEITHER, and the evaluation document says which premise was not established. Missing evidence and established negation are distinct statuses, and the mutation suite includes a test that breaks if they are ever conflated.

Two norms compete. In Catala, a conflict is an error at run time, which is the correct behaviour for a system that must always produce a payment amount. In Arxo, the conflict is preserved in the answer as BOTH, with both derivations in the proof graph. That is how a formalization records a genuine defect in the text or a gap in the conflict-of-laws rules instead of silently picking a side. The Lean mechanization of the semantics proves this as a theorem: when two defeasible derivations rest on incomparable grounds, both survive.

Neither choice is a limitation of the other. Catala's closed world is what makes a mass-payment engine trustworthy. Arxo's open world is what makes a single disputed case explainable.

Axis 3: what a function cannot carry

The vehicle-damage Rules contain more than a computation. They impose ten duties and one liberty on insurers, appraisers and victims: to inspect within a deadline, to deliver a report, to allow a second inspection, to choose an appraiser. They also delegate one quantity, depreciation, to an external methodology that the Rules do not contain, and they count deadlines in working days against the official state calendar.

These parts of the regulation did not enter the Catala comparison, because the function model has no slot for them. They are first-class in Arxo:

• Deontic positions. Duty, liberty, power and immunity are declarations with a lifecycle: a duty arises, is performed, is breached or lapses inside a window. As of 9 September 2026, power appeared in 189 corpus files and immunity in 54; priority, the declared resolution of conflicts by rank and specialty, in 321; interpretation, competing readings of one text, in 127; presumption in 127 and fiction in 16.
• The calendar as pinned data. Working days are computed against a byte-pinned snapshot of the official 2026 calendar with its holiday transfers, carried into the evaluation document by hash. A case dated outside the snapshot's coverage is reported as out of calendar range rather than guessed. In the Catala program we wrote, working days were derived by folding over a list of dates supplied as input, which is entirely adequate for a fixed year and is not the same thing as a verifiable reference to the state calendar.
• Editions in time. A query is evaluated on the date of the event against the edition of each norm in force on that date. The regulation's own amendment history is part of the package, and an answer states which edition it applied.
• Quantities with units. A mileage in the wrong unit is a type error, not a silent conversion. In Catala the unit lives in the field name.

Catala's authors chose a function model deliberately, and the choice has paid off in exactly the domain it was made for. Tax and benefit calculation needs a value; it rarely needs to know which party is currently in breach of which duty. Private-law disputes, regulatory compliance and procedural law need the second thing at least as often as the first.

Axis 4: two kinds of trust

Both systems make a verification claim. The claims are about different links in the chain.

Catala trusts the compiler. The law text and its formalization live in one literate file, and the crucial translation from the default calculus to a lambda calculus with exceptions is mechanized in F*, with type preservation and a simulation result. The guarantee is that the generated OCaml, Python, C or Java does not distort the annotated specification. What the annotation says about the law is a matter for legal review of the literate file.

Arxo trusts the text and checks the proof. Provenance is part of the language: every source, edition and publication carries a content hash, and the compiler rejects any quoted fragment that is not an exact substring of the pinned official publication. The evaluation document then carries a proof graph, and an independent checker written in Lean 4 (21 modules, 91 theorems and lemmas, no sorry, toolchain 4.33.0, counted 19 September 2026) verifies that certificate against the least model of the monotone fragment of the semantics. The checker does not compare the two Arxo evaluators with each other; it checks each one's output against the specification. Its first run over the corpus found a dangling-reference defect that both evaluators shared and that byte-for-byte comparison could never have surfaced.

Compiler correctness and certificate checking are complementary. One says "the code you deployed is the specification you wrote"; the other says "the answer you received follows from the sources you pinned". A mature discipline of computational law will want both.

Discussion: a taxonomy, not a ranking

The parity experiment suggests a simple way to place the two systems.

The two paradigms also meet in the middle. Arxo's code-generation backends print the purely computational slice of a package into a standalone TypeScript, Python or Go module that runs without the rules engine, returning answer and status without the proof (40 of 43 executed conformance vectors matched on 14 September 2026, with no divergence across the three targets; the remaining vectors were refused by the plan with a named reason). That slice is, in effect, the part of a package that Catala would also express, and it is a natural interchange point between the two worlds: computable cores could travel from one language to the other, while deontics, editions and proof stay where they are modelled.

Conclusion

Catala established that programming-language theory applies to statute law, and it did so with a standard of rigour the field now measures itself against. On a shared regulation, Arxo Law reproduces Catala's results exactly, case for case and mutation for mutation, and then continues into the parts of the regulation that a function cannot express: who owes what to whom, what the text says on the date of the event, what happens when two norms collide, and how a reader can check the answer against the official publication.

Arxo executes the canon. Models formalize; Arxo executes and proves. Catala compiles the calculable core of the law with a verified compiler. The future of rules as code is not a choice between the two but a division of labour that the parity experiment makes concrete.

Sources: Merigoux, Chataing, Protzenko, "Catala: A Programming Language for the Law", ICFP 2021 (arXiv:2103.03198); Catala releases (github.com/CatalaLang/catala/releases, 1.2.0 of 2 June 2026, 1.2.1 of 6 July 2026); Programme Apollo, Inria, project page for Catala (apollo.inria.fr/projets/catala); CNAF press release of 8 June 2026 on the CNAF–Inria convention; Université Paris-Saclay news on the 2026 Scientific Interdisciplinarity Award; Arxo, "What Is Rules as Code" (blog.arxo.io/what-is-rules-as-code).