DEV Community: arxo

One Accident, Several Laws, One Answer

arxo — Wed, 07 Oct 2026 19:14:36 +0000

An insurer pays 730,000 tenge. The payment is twelve days late. Following the rules from the insurance statute to the Civil Code produces another 4,020 tenge—and a record of how that amount was reached.

The money has arrived. Has the insurer finished paying?

In this fictional motor-insurance case, the insurer receives the required documents on 22 July 2026 and pays 730,000 tenge on 24 August. Arxo computes the payment deadline as 12 August. Payment was late; under the stated calculation inputs, the late-payment penalty is 4,020 tenge.

Each part of that answer comes from somewhere different. The insurance statute supplies the payment period and the obligation to pay a penalty. The Civil Code supplies the rule for that penalty. A National Bank rate and an official calendar supply dated values. The case supplies the payment events and an explicit assumption needed for the arithmetic.

A single bank transfer has led us across several sources. The useful result is an answer whose steps can be inspected together.

Start with events

The example belongs to a collection of five fictional cases about Kazakhstan’s compulsory motor third-party liability insurance, known as OGPO VTS. The main case is deliberately small:

Input	Value
Required documents received	22 July 2026
Insurance payment amount	730,000 KZT
Actual payment date	24 August 2026
Annual-to-daily rate divisor	365, explicitly supplied
Calendar	The recorded official 2026 calendar

The 730,000-tenge insurance payment is an input in this example. The calculation begins after that amount has been established. It does not reconstruct repair costs from photographs or decide the disputed facts of the accident.

There is no input labelled “the insurer paid late.” That is one of the questions the rules must answer.

This distinction matters when building a legal application. If a person supplies the conclusion and the software merely repeats it, the central reasoning remains outside the computation. Here, the case supplies two events: receipt of documents and payment. The model must connect them through the applicable deadline.

A deadline has dependencies

Article 26(1) of the motor-insurance statute provides the general period used in this case: fifteen working days from receipt of the documents specified in Article 25.

For documents received on Wednesday, 22 July, the recorded calendar and counting policy place the deadline on Wednesday, 12 August. The payment on 24 August comes after it. The late-payment period runs from 13 through 24 August, twelve calendar days.

The two intervals use different clocks. Working days establish when payment falls due. Calendar days measure this period of delay. A calculation that treats both intervals as the same kind of duration can get the amount wrong even when its multiplication is correct.

The calendar is therefore part of the case’s supporting data. Someone checking the deadline needs the calendar used for the calculation, alongside the date and the rule.

The insurance law sends us to the Civil Code

Article 26(4) imposes a penalty for late payment and refers to Article 353 of the Civil Code for its procedure and amount. The payment-day calculation used here takes the National Bank base rate applicable on the day the obligation is performed.

In the recorded case, that annual rate is 16.75%. With the explicitly supplied divisor of 365, the arithmetic is:

730,000 KZT × 12 days × 0.1675 ÷ 365 = 4,020 KZT

The amount is exact for these inputs. The case also establishes that the obligation to pay the late-payment penalty is active.

The saved analysis below compares this case with payment on the deadline itself. Both have the same deadline, 12 August; payment on 24 August establishes lateness. Open the analysis to inspect the 4,020-tenge result and the penalty obligation. The interface is available in English; the case questions are in Russian.

Payment on the deadline and payment twelve days later

The implementation preserves the division of responsibility between sources. The insurance rule creates the obligation; the Civil Code provides the referenced basis; dated rate data supplies a value; an accrual calculation applies it. The connection between those parts does not introduce another legal rule of its own.

That is what makes the cross-reference useful to software. A reader can follow it. An executable model can carry a result across it while retaining its origin.

Remove one assumption

The divisor of 365 deserves its own line in the input table. Article 353’s payment-day rate provision does not specify the annual-to-daily conversion convention. This model requires that convention to be supplied explicitly.

Remove the divisor from the same case. The payment is still late: the dates and calendar are unchanged. But the model no longer derives a penalty amount.

That outcome keeps two questions separate:

Was payment late? Established.
What penalty amount follows from these inputs? No amount derived.

A zero in the second field would erase that distinction. So would silently inserting a familiar financial convention. The saved explanation identifies the amount rule as unestablished; it does not itself trace the missing divisor through every intermediate calculation. The paired cases show exactly which input was removed.

Now make a different change: supply both 24 and 26 August as the single payment date for the same claim. Those assertions conflict with the field’s uniqueness requirement. The evaluation is marked NON_EXECUTABLE. Any amount retained in its diagnostic output must be read with that status; it is not an accepted answer to the conflicting case.

Move the case across a holiday

Another case in the collection moves receipt of documents to 19 October 2026 and payment to 10 November. In the recorded calendar, Republic Day falls on Sunday, 25 October, with the day off transferred to Monday, 26 October.

The deadline is 10 November. The alternative date, 9 November, is not established; payment on 10 November does not establish lateness. The saved analysis also contains the missing-divisor and conflicting-date variants.

A transferred holiday, a missing divisor, and conflicting payment dates

These are small changes to one case, but they exercise different parts of the reasoning: date calculation, sufficiency of inputs, and consistency of assertions. A single “valid” checkbox would lose information the reader needs.

The rest of the accident has its own sources

The deadline-and-penalty example sits within a wider motor-insurance model. Following a case from policy purchase to a dispute brings further sources into view:

Question	Where the model looks
What premium applies?	The insurance statute, bonus-malus rules and annual adjustment coefficients
How is vehicle damage assessed?	The vehicle-damage assessment rules
What payment limits apply?	The insurance statute and the relevant budget index
Was payment late, and what penalty follows?	The insurance statute, calendar, Civil Code and dated rate data
Can the claimant use a guarantee mechanism?	The Insurance Payments Guarantee Fund legislation
Can the dispute go to the insurance ombudsman?	The insurance legislation governing that procedure

These are branches with their own conditions. A dispute does not, by itself, establish eligibility for every procedure. A change in the insurer’s status calls for a fresh check of the guarantee conditions. The five cases shown here exercise the payment deadline and penalty branch.

A software package can connect provisions from several acts, while one act can contribute to several stages. Regulations, annual tables and calendars matter alongside statutes. Each rule and value retains its source as the case moves between them.

What one answer contains

For the main case, a useful answer keeps four results together: the deadline is 12 August; payment on 24 August was late; the stated inputs yield a 4,020-tenge penalty; the penalty obligation is active. It also preserves the facts, rules and assumptions behind those results.

The displayed analyses are saved evaluations. In a local check on 23 September 2026, all sixteen case-and-question evaluations in the captured collection matched their saved command-line evaluation documents byte for byte when run through the local WebAssembly engine. That checks reproduction on those fixed inputs; the legal interpretation and the evidence for the case remain separately reviewable.

Arxo executes the canon. Models formalize; Arxo executes and proves. In this example, the practical payoff is that a reviewer can follow the path from two payment events through a deadline and a statutory cross-reference to an additional obligation.

The bank transfer answers whether money arrived. The connected rules answer what that payment leaves owing.

Originally published on the Arxo blog.

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

arxo — Tue, 06 Oct 2026 18:32:33 +0000

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, 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 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.

What Is Rules as Code, With a Runnable Example

arxo — Mon, 05 Oct 2026 19:20:02 +0000

Rules as Code publishes a rule in a form a machine can execute, next to the text a person reads. Here is the definition, where the idea comes from, and a limitation period you can compute yourself.

Rules as Code is the practice of writing a rule — a statute, a regulation, an internal policy — in a form a computer can execute, alongside the natural-language text, so that both are drafted, tested and kept in step together. The same idea travels under other names: Law as Code, Legislation as Code, machine-consumable legislation, computational law. The goal is not to automate judgment. It is to make the logic of a rule explicit, so it can be tested before it applies to anyone and reproduced after it has.

A runnable rule looks like this: facts go in, a question is asked, and the answer comes back with the article it rests on. Below is one such rule, a limitation period from an international instrument, with the facts, the questions and the answers, and links to run it with your own dates.

Where the term comes from

In 2018 New Zealand's Service Innovation Lab ran a three-week discovery with Inland Revenue, the Ministry of Business, Innovation and Employment and the Parliamentary Counsel Office, testing the approach on two existing pieces of legislation. Its report, Better Rules for Government, gave the movement its name.

In October 2020 the OECD's Observatory of Public Sector Innovation published Cracking the Code: Rulemaking for humans and machines, which proposed that some government rules exist in a machine-consumable version alongside the natural-language one, and set out what that asks of drafters, lawyers and engineers.

Several tools carry the idea. OpenFisca, developed in France since 2011 and released as free software, models tax and benefit rules and is used to simulate the effect of new law on households and the budget. Catala, from Inria and presented at ICFP 2021, is a programming language whose code follows the structure of the statute it implements; while encoding French family benefits its authors found a bug in the official implementation. Blawx, by Jason Morris, is a web-based tool for encoding and testing rules with answer set programming. In Germany, the federal agency SPRIND runs Law as Code as a strategic project aimed at official, machine-readable publication of legal norms.

Most of this work targets tax and benefits: who is eligible, and for how much. Contract law, time limits and procedure appear less often. The example below is a time limit.

A runnable example: when does a limitation period expire?

Article 10.2 of the UNIDROIT Principles of International Commercial Contracts (2016 edition) sets two periods. The general limitation period is three years, beginning on the day after the day the obligee knows or ought to know the facts that let it exercise its right. The maximum period is ten years, beginning on the day after the day the right can be exercised.

Take a case. The obligee learned the facts on 10 March 2020. The right could be exercised from 15 January 2019. Here is the test that sits in the package modelling chapter 10, trimmed to the facts that matter; the full file also names the parties and the contract:

test "PICCL-01-GENERAL-AND-MAXIMUM-PERIODS" {
    given {
        context {
            deadline_policy PICC_LIMITATION;
            legal_time @2026-09-17;
            timezone "UTC";
        }
        assert "a2": obligee_knew_facts_on(entity_ref("urn:case:piccl:right-1"), @2020-03-10) { origin case_input; }
        assert "a3": right_exercisable_from(entity_ref("urn:case:piccl:right-1"), @2019-01-15) { origin case_input; }
        assert "a4": general_period(entity_ref("urn:case:piccl:right-1"), 3 calendar_year) { origin case_input; }
        assert "a5": maximum_period(entity_ref("urn:case:piccl:right-1"), 10 calendar_year) { origin case_input; }
    }
    evaluate truth(general_period_expires_on(entity_ref("urn:case:piccl:right-1"), @2023-03-11));
    expect truth_status == TRUE_ONLY;
    expect any_applied(GeneralPeriodOfThreeYears);
}

Run the case and ask four questions:

Question	Answer	Why
Is the exercise of this right subject to limitation at all?	Established	Article 10.1(1)
Does the general period expire on 11 March 2023?	Established	Article 10.2(1): three years beginning on the day after 10 March 2020
Does it expire on 10 March 2023?	Not established	No rule makes that day the last one
Does the maximum period expire on 16 January 2029?	Established	Article 10.2(2): ten years beginning on the day after 15 January 2019

The third row is the one to read twice. "Not established" is not "false". The text says the count begins on the day after, so the model says so, and a question about the 10th finds no rule that concludes it. A reader who expected the 10th learns the difference from the model, not from a footnote.

Now the second case: the period has expired, and the obligor has said nothing about it.

Question	Answer	Why
Is the right extinguished?	Established: it is not	Article 10.9(1)
Is its exercise barred?	Not established	Article 10.9(2): the obligor never asserted the expiry
May the obligee still set off?	Established	Article 10.10: until the expiry is asserted

Two answers that only look contradictory. The right survives, and its exercise is not barred either, because the bar needs an assertion that has not happened. Article 10.10 reads the same silence from the other side.

There is a third kind of answer. Where the Principles say "could not reasonably" or "fundamentally", the model does not decide. It returns a request for the tribunal's finding, with the article that calls for it. That is what the text asks for, and the answer says so in the same place it would otherwise give a result.

Run it yourself.

Change one fact and watch the answer: the two cases above, article by article.
Bring your own dates: articles 10.2 and 10.4 computed in your browser, including acknowledgement, proceedings and impediments.
Verify an answer someone sent you: a saved calculation is run again in your browser, from the same bytes.
Connect an agent: claude mcp add --transport http picc https://mcp.arxo.io/mcp/picc, or npx -y @arxo/mcp-picc for a local server.
Read the source: github.com/arxohq/arxo-unidroit-picc, all 210 articles in seven packages.

What an executable rule carries

Five things travel with every answer above, and they are what makes a rule executable rather than merely encoded.

The text is pinned. Each article an answer cites is a fragment of the published text, fixed by a hash of its content. The model is written from that text and points back into it.
Time is a parameter. Every question carries a date. The edition in force on that date answers, and a question asked of the 2024 text and of the 2026 text can get different results with the same facts.
Silence and judgment are answers. "Not established" means no rule concludes it. "For the tribunal" comes back as a typed request, naming the article that requires the finding.
The answer reproduces. An answer document holds the request, the chain of reasoning down to the articles, and the hashes of the model and the result. The verify page above runs it again and either matches or shows where it does not.
The rule has tests. On 21 September 2026 the corpus of executable canons held 21,948 scenario files like the one above. They are written in one language and fail the way a broken unit test fails. The Law Has Unit Tests walks through one.

The same mechanics beyond the law

A statute, a standard, a rulebook and a textbook share one shape: an authoritative text with an edition and a provenance, applied to facts. Law came first because it is the most demanding case, not because the mechanics stop there.

Take the FIDE Laws of Chess, in force since 1 January 2023. Article 7.5.5 says that after a player's first completed illegal move the arbiter gives two minutes to the opponent, and that a second completed illegal move by the same player loses the game, unless the position is such that the opponent cannot checkmate by any possible series of legal moves, in which case the game is drawn.

Here is the case as the arbiter would record it: White has completed two illegal moves, and the record is complete on whether Black can still mate.

case SecondIllegal {
    assert "player": fide.laws.chess::player_of(entity_ref("urn:example:chess:game"), entity_ref("urn:example:chess:white")) { origin case_input; }
    assert "complete-mate-facts": fide.laws.chess::checked_player(entity_ref("urn:example:chess:white")) { origin case_input; }
    assert "illegal-count": fide.laws.chess::completed_illegal_move_count(entity_ref("urn:example:chess:white"), 2) { origin case_input; }
}

Case	Question	Answer
Two illegal moves, mate still possible	Is the game lost by White?	Established, by the rule on the second illegal move
Two illegal moves, no possible mate	Is the game lost by White?	Not established
Two illegal moves, no possible mate	Is the game drawn?	Established
A piece touched, no finding on intent	Must White move it?	A request to the arbiter: Article 4 turns on the intention, and the record does not state it

The board, the legality of a move and the possibility of mate are facts of the record. Arxo does not play chess. It applies the Laws to what the arbiter wrote down, and it names the arbiter where the Laws do.

The Laws of Chess sit in the same corpus as the Principles and are served at the same public endpoint, https://mcp.arxo.io/mcp. Next to them: the IFAB Laws of the Game, with the goalkeeper's time limit across two editions; three HTTP RFCs and what happens to a Content-Length header; the CSS cascade from W3C, and which declaration wins. Each is modelled from its pinned text in the same language, and each answers with the section it rests on.

Questions people ask

Is Rules as Code the same as Law as Code? The same idea under two names. Rules as Code comes from the public-sector community around the New Zealand and OECD work and covers policy and regulation as well as statute. Law as Code is the name used in Germany and in much of the academic literature. Computational law is the broader academic term.

Does it replace lawyers or courts? No. It computes what follows from the text on the facts supplied. Where the text calls for an assessment, "reasonable", "fundamental", "intended", the answer is a request for that assessment, addressed to the tribunal or the arbiter, with the article that requires it.

What tools exist? OpenFisca for tax and benefit simulation; Catala, a language whose code follows the structure of the statute; Blawx, a visual tool over answer set programming; and Arxo, where the text is pinned by content, the edition is chosen by date, the answer reproduces by hash, and an AI agent can connect over MCP.

Can I use it from Claude, Cursor or Claude Code? Yes. One command adds the Principles as a server: claude mcp add --transport http picc https://mcp.arxo.io/mcp/picc. The MCP page lists the other endpoints and what an agent can ask.

Originally published on Arxo Writings.

The Law Has Unit Tests

arxo — Mon, 05 Oct 2026 19:13:34 +0000

A test of a statute looks like a test of code, with three differences: silence is a passing result, a test can expect a question instead of an answer, and every test carries a date.

Here is a test. If you have ever written one for software, you have read this file before:

// Law 12.2, 2024/25 edition: the goalkeeper held the ball for nine seconds.
// Date of law 1 September 2024: the 2024/25 book applies.
test "ifab-01-gk-nine-seconds-2024-25" {
    given {
        context { legal_time @2024-09-01; timezone "UTC"; }
        assert "a0": goalkeeper_within_own_penalty_area(match, i1) { origin case_input; }
        assert "a1": goalkeeper_control_seconds(match, i1, 9.0) { origin case_input; }
    }
    evaluate truth(indirect_free_kick_offence(match, i1));
    expect truth_status == TRUE_ONLY;
}

Given, when, then. Two facts from the match report, one question to the Laws of the Game, one expected answer. The file sits in the tests/ folder of the package that models the IFAB Laws of the Game, next to the rules it exercises. Run it, and Arxo executes the model of Law 12 against these facts and compares the answer with the expectation.

This is not a metaphor. On 21 September 2026 the corpus of executable canons holds 21,948 such scenario files: contract law, civil codes, insurance statutes, the UN Charter, chess and football, the CSS cascade. They are written in one language, they run under one engine, and they fail the same way a broken unit test fails.

The interesting part is where a test of a law stops behaving like a test of code.

1. Silence is a passing result

In software, a function that returns nothing has a bug. In law, a norm that says nothing about your facts is the correct outcome, and a test has to be able to expect it.

The Declaration by United Nations of 1 January 1942 binds each signatory to employ its full resources against the Axis members "with which such government is at war". The Soviet Union signed. It was at war with Germany and not at war with Japan. Does the Declaration oblige the USSR against Japan?

test "un-test-pair-not-at-war" {
    given {
        context { legal_time @1942-01-01; timezone "Europe/London"; }
        assert "un-war-de2": at_war(UnionOfSovietSocialistRepublics, Germany) { origin case_input; }
    }
    evaluate truth(employs_full_resources_against(UnionOfSovietSocialistRepublics, Japan));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;
}

The expected answer is NEITHER: the proposition is neither established nor refuted. The computation finished (COMPUTED), nothing went wrong, and the Declaration is simply silent for this pair. The model does not turn missing facts into "false", because the world of a case is open: nobody asserted that the USSR was at war with Japan, and nobody asserted that it was not.

The same expectation appears in commercial law. Under the UNIDROIT Principles, a non-performance is fundamental if it was intentional, unless the non-performing party would suffer disproportionate loss. A scenario with an intentional breach and a disproportionate loss expects NEITHER for "fundamental non-performance": the intention does not carry the day, and no other ground was pleaded.

A test framework that only knows true and false cannot express this. The test language for canons has to, or half of the law becomes untestable.

2. A test can expect a question

Some elements of a norm are not facts. "Deliberately played the ball", "disproportionate loss", "obvious goal-scoring opportunity": the text hands these to a person with authority to decide. A model that guessed them would be wrong by design. So the model asks, and a test can expect the asking.

Law 11 of football: a player in an offside position receives the ball from an opponent. Whether the opponent deliberately played it, or the ball merely rebounded, is the referee's judgement. Without that judgement the question "offside offence?" has no answer yet, and the test says so:

test "ifab-07-offside-rebound-requires-judgment" {
    given {
        context { legal_time @2026-09-01; timezone "UTC"; }
        assert "a0": part_in_opponents_half(match, i3, p1) { origin case_input; }
        assert "a2": part_nearer_goal_line_than_second_last_opponent(match, i3, p1) { origin case_input; }
        assert "a4": ball_came_from_opponent(match, i3) { origin case_input; }
        assert "a5": played_or_touched_the_ball(match, i3, p1) { origin case_input; }
    }
    evaluate truth(offside_offence(match, i3, p1));
    expect evaluation_status == REQUIRES_JUDGMENT;
    expect judgment_request(opponent_deliberately_played_the_ball, MatchReferee);
}

The expectation is precise: the evaluation stops with the status "requires judgement", and the open question is this predicate, addressed to this organ, the match referee. Not "the model was unsure". The next scenario in the same folder adds the referee's answer, marked origin adjudicated rather than origin case_input, and expects a definite result with zero open questions.

The same channel runs through the commercial canons. In the UNIDROIT scenario on fundamental non-performance by deprivation, the expected status is TRUE_ONLY for the fundamental character and REQUIRES_JUDGMENT, because the question of disproportionate loss under Article 7.3.1(2)(e) has not been put to the tribunal. Two expectations on one answer, and both must hold.

Civil codes use it too. In the Code civil case below, the harmful act, the damage and the causal link are on file: liability under article 1240 comes back as a question for the judge, because it needs a finding of fault, while prescription on the same facts is established, because it needs only dates.

La faute reste au juge

3. Every test carries a date

The file at the top of this article expects an indirect free kick. Its neighbour holds the same two facts and expects a corner kick:

// The same incident on 1 September 2026: the 2026/27 book applies.
test "ifab-02-gk-nine-seconds-2026-27" {
    given {
        context { legal_time @2026-09-01; timezone "UTC"; }
        assert "a0": goalkeeper_within_own_penalty_area(match, i1) { origin case_input; }
        assert "a1": goalkeeper_control_seconds(match, i1, 9.0) { origin case_input; }
    }
    evaluate truth(restart_awarded(match, i1, corner_kick));
    expect truth_status == TRUE_ONLY;
}

Nothing in the package was edited between the two tests. Both rules live in the model, each pinned to the edition of the Laws that contains it, each edition with its window of force:

@source(LOTG_2425_LAW_12)
rule GoalkeeperSixSecondsIndirectFreeKick(m, i, secs) strict {
    when goalkeeper_within_own_penalty_area(m, i)
        and goalkeeper_control_seconds(m, i, secs)
        and (secs > 6.0);
    then indirect_free_kick_offence(m, i);
}

@source(LOTG_2526_LAW_12, LOTG_2627_LAW_12)
rule GoalkeeperEightSecondsCornerKick(m, i, secs) strict {
    when goalkeeper_within_own_penalty_area(m, i)
        and goalkeeper_control_seconds(m, i, secs)
        and (secs > 8.0);
    then restart_awarded(m, i, corner_kick);
}

The date of law in the test selects the edition; the edition selects the rule. Of the 21,948 scenarios in the corpus, 19,358 name a date of law explicitly. A test without a date would be a test of "the law in general", and there is no such thing.

Tests are written from the text, not from the model

A unit test that was generated from the implementation tests nothing: it will agree with whatever the code does. The same trap exists for law, and it is easier to fall into, because the model is often the first precise reading of the text anyone has produced.

So the rule for canons is the rule for good test suites: the expectation comes from the source, and it is frozen. A change in the model has to break scenarios; it never rewrites them. When a scenario and the model disagree, the text is opened, the reading is settled, and the losing side is fixed.

An example of what the text can hide. Article 19(4) of the Kazakh compulsory motor insurance law adds a coefficient of 0.8 "for other towns and settlements in the regions listed in paragraph 3". The table in paragraph 3 lists regions, and it also lists Almaty, Astana and Shymkent, which are cities of republican significance, not regions. A scenario written from the text for "Almaty, other settlement" expects the coefficient not to apply. A scenario written from the table would expect the opposite. Three independent readers of the text agreed with the first expectation, and that is the one the package holds.

Continuous integration for a bill

Once a statute has a test suite, the question every engineer asks becomes available to a legislator: what does this change break?

Arxo answers it with an impact report. Take the current model of an act and the model of the draft amendment, run every scenario and every declared goal against both, and compare:

which norms changed in meaning, counted on the structure of the rules rather than on their wording, so that a reworded label with the same logic is reported as no change;
which scenarios changed their outcome, with the answer before and after;
which goals the act declares still hold, and which one held before the amendment and fails after it;
which of the amended norms are executed by no scenario at all.

That last line is the one a legislator will not get from a reading. The report names it plainly: for those norms, "outcome unchanged" is an absence of observation, not a conclusion. The test suite of a statute has coverage, and the coverage has holes, and the holes are listed.

The same report runs on the axis of time instead of the axis of drafts: two dates of law, one act, and the scenarios show what the passage of an edition changed for the cases people actually brought.

Where to look

The UNIDROIT Principles of International Commercial Contracts are published as executable packages at github.com/arxohq/arxo-unidroit-picc. Each package carries its tests/ folder; the scenarios on fundamental non-performance quoted above are in the termination file of the non-performance package. Open one, read the facts, and if you believe the Principles answer differently, send the counterexample as an issue in the same repository. That is how a scenario enters the suite.

Originally published on Arxo Writings.