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, applies programming-language theory to computational law. Its default-calculus-to-lambda-calculus compilation step is mechanized in the F* proof assistant, and its compiler targets OCaml, Python, C and Java. Legal fidelity still depends on review of the formalization alongside the source text.
Arxo Law is built on a different premise. In Catala, a statute becomes a function: inputs go in, a value comes out, and the verified compilation step preserves the formal specification. 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 duties, provenance and edition metadata outside the computational comparison.
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.
| Check (9 September 2026) | Result |
|---|---|
| 65 reference cases, Catala against expectations | 65 of 65 |
| 65 reference cases, both Arxo evaluators | all pass, results byte-identical between evaluators |
| 240 random cases, oracle vs Catala | 240 of 240 |
| 240 random cases, oracle vs Arxo engine | 240 of 240 |
| 20 targeted mutations of the Arxo model | 20 of 20 killed by the test suite |
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. For the tested cases, both formalizations reproduce the expected computational outcomes. This does not establish equivalence for every possible input. 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 a natural product for microsimulation, where a rules engine runs over millions of households. 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.
The measurements compare different outputs and different execution paths; they are not a controlled benchmark of the languages. 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. In this profile of the Rust engine, string comparison, map lookups and allocation account for most of the cost, and the solver itself for under one percent.
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 lies outside our computational model
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 we scoped that model to computational outcomes. 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,
powerappeared in 189 corpus files andimmunityin 54;priority, the declared resolution of conflicts by rank and specialty, in 321;interpretation, competing readings of one text, in 127;presumptionin 127 andfictionin 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 our Catala model 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. This proof covers the specified core translation; it is not an end-to-end proof of every compiler backend or of the legal interpretation. 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 verifies a translation step from the formal specification; the other checks a certificate against the covered semantics. Neither proves that a formalization captures every legal meaning of the source. 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.
| Question | Catala | Arxo Law |
|---|---|---|
| What is a norm? | A function from inputs to a value | A datum: text, provenance, rules, positions |
| What does a call return? | A value | An evaluation document with proof and hashes |
| How are conflicts handled? | Error at run time | Preserved as BOTH in the answer |
| What does silence mean in these models? | Absence or false, by field |
NEITHER, distinct from negation |
| Where is trust anchored? | Verified core compilation step (F*) | Pinned sources and certificate checking for the monotone fragment |
| Best fit | Mass calculation of tax and benefits | Individual cases, compliance, disputes, procedure |
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
The tested computational slice agrees: 65 reference cases and 240 random cases produced the expected outcomes in both formalizations. The 20 mutation checks apply to the Arxo model only.
The practical design choice is what a caller needs beyond that result: a value, or an evaluation document that also records provenance, editions, duties and competing derivations. The experiment makes that choice concrete without establishing that either language is universally better.
To inspect or reproduce the comparison, start with the public parity repository: it contains both models, the reference cases, runners and recorded results.
Sources
- Merigoux, Chataing and Protzenko, Catala: A Programming Language for the Law, ICFP 2021.
- Catala source and releases.
- Arxo–Catala parity experiment.
- What Is Rules as Code?.
Originally published on the Arxo blog. Measurements and implementation counts above are dated snapshots, not claims about later releases.
Top comments (0)