The Translator Writes the Rule

A real sentence of United States tax law reads: "The aggregate amount treated as acquisition indebtedness for any period shall not exceed $1,000,000 ($500,000 in the case of a married individual filing a separate return)" (26 U.S.C. § 163(h)(3)(B)(ii)). For taxable years after 2017, the current text substitutes $750,000 and $375,000. The older figures are the ones that were litigated.

Bruce Voss and Charles Sophy, unmarried co-owners of two homes, each claimed interest on more than $1.1 million of debt, the acquisition limit plus the home equity limit. The Tax Court held in 2012 that the limit applies per residence. In August 2015 the Ninth Circuit reversed, two judges to one, and held that it applies per taxpayer. The majority said that "the statute is silent as to how the debt limits should apply in co-owner situations", and that the provisions limit the aggregate amount "but neither says to whom or what the limits apply". The dissent called the statute "ambiguous" and would have deferred to the IRS (Voss v. Commissioner, 9th Cir., 2015). In 2016 the IRS announced that it "will follow the Voss opinion" (Action on Decision 2016-02).

Now imagine encoding that sentence in 2013. A program that compares a number with a limit has to say whose number. It can answer the question the Ninth Circuit answered two years later, or it can make the answer someone else's input. It cannot avoid the question.

Thesis. Turning a legal sentence into an executable rule includes deciding what the sentence means, and every check that looks only at the translation certifies whichever reading arrived. Catala's authors already know this and built a working method around it, a lawyer in the room. Cheap machine translation makes that lawyer the first cost to cut. The missing control is that a translation should ship with a rejected reading, the inputs on which the two differ, and the name of whoever decided.

Disclosure of interest: I build AI systems for law firms, and I wrote LegalLean, which this chapter compares with Catala and finds wanting in several respects. All statements about § 163(h) are about US federal law.

What Catala does, as its authors describe it

Catala is a domain-specific language for "deriving faithful-by-construction algorithms from legislative texts" (Catala repository). Its scope is deliberate. The founding paper concerns computational law, where "human appreciation, judgement or interpretation are not generally expected", and tax, family benefits and pensions are its examples (Merigoux, Chataing and Protzenko, ICFP 2021). Merigoux's co-author Liane Huttner has said that the project "should not be used for the penal code or the civil code" (Huttner and Merigoux, interview).

Its semantic core is a default term, written ⟨e₁, ..., eₙ | j :- c⟩: exceptions, a justification and a consequence. Each exception is evaluated. Two or more defined exceptions raise a conflict error. Exactly one defined exception gives the result. With none defined, a true justification gives the consequence and a false one gives the empty value. The paper calls this "a restricted form of prioritized default logic", in which each definition carries its own static tree of priorities, and credits Sarah Lawsky's argument that this flavour of default logic suits the law. Lawsky's case is in (Lawsky, "A Logic for Statutes", Florida Tax Review vol. 21). The compilation step from the default calculus to a language with exceptions is proved correct in F★, with the limit the authors state themselves: "the proof does not take into account all language features".

The method matters as much as the logic. "We do not expect lawyers to write Catala code by themselves", the paper says. A programmer and a lawyer pair-program on a file holding the legal text and the code together, and the lawyer reviews. Its one user study had 18 law graduate students, and the authors say it lacks "the rigor of a scientific user study". The production-side evidence is better. The same paper reports that "we uncover a bug in the official implementation of the French benefits". Merigoux's replication of the French housing benefit took 22 pair-programming sessions totalling 50 hours and produced about 7,000 lines, and "the majority of the time was spent on actually deciphering and understanding the text of the law" (Merigoux, experience report, ProLaLa 2023). The Catala book now puts that share at 70% to 90% of project time, and has a warning box titled "Prioritizing exceptions is a legal act of interpretation" (The Catala Book). A paper on tooling for Catala says that "translations of legal texts into code amount to legal interpretations, which can be erroneous" (Goutagny, Fromherz and Monat, CUTECat, ESOP 2025). Merigoux, Alauzen and Slimani catalogue what programmers decide without noticing as imprecision, simplification and invisibilisation (Rules, Computation and Politics, 2023). The book also records that the team does not think publishing law directly as executable code is desirable, given its effect on the rule of law.

So the sentence in my title is not a discovery.

The deployment record needs care, because the sources do not agree on one word. Inria's programme page describes experiments producing proofs of concept at the French tax authority (2023 to 2024) and at the family benefits agency CNAF (2024 to 2025), after which CNAF "adopte Catala comme technologie de référence" (adopts it as its reference technology) (Inria Apollo). CNAF's press release of 8 June 2026 says Catala was chosen as "une technologie structurante pour les futurs chantiers" (a structuring technology for future projects) (CNAF and Inria). The EU's software catalogue says Catala "is used in production by the French tax authority" (Interoperable Europe). I could not find a primary source that states the scope of that production use. What the sources do establish is that public bodies have tried Catala on real benefits and tax, and that one has chosen it. I have found no public-body use of LegalLean, which is a research artefact.

Four corrections to my own work

Reading these sources against my earlier essays produced four corrections, in rising order of seriousness.

1. A wrong link. The LegalLean and Legal Reasoning Needs a Wind Tunnel essays both linked Catala to arXiv 2110.05001. That paper concerns a soft robotic arm. The Catala paper is arXiv 2103.03198, and I corrected both links on 02/11/2026.
2. Flattery that was also wrong. LegalLean's paper says Catala is "a production-grade DSL used by the French state" that "compiles to verified OCaml". The first phrase claims more than I had read, as the previous section shows. The second claims more than the Catala paper does: the core compilation step is proved in F★, the proof does not cover every feature, and the authors chose not to use the extracted code in the compiler.
3. A claim about what Catala does not ask. Wind Tunnel says that Catala's compiler "does not ask what happens when the same rule is expressed differently". That is true of paraphrase testing. Yet the team has built tools that ask the neighbouring question, which is what happens when one sentence has two admissible computations. Monat, Fromherz and Merigoux define a date expression as ambiguous when rounding it in different modes gives different results, establish properties of the semantics in F★, and run a static analysis over the housing benefit code to find ambiguous cases (ESOP 2024). That is the shape of the theorem below, done first, and done on a real program.
4. My own encoding took the wrong reading and told nobody. LegalLean's § 163(h) case study tests the home equity limit with debt.amount ≤ homeEquityLimit status, one debt at a time. The word "aggregate" did not survive, and neither did the question in Voss. Worse, exceeding the limit returns formal False, the constructor my essay describes as needing no human determination. Voss and Sophy had a $300,000 line of credit. A check against an unmodified copy of the case study proves that the encoding returns formal False for a line of that size in 2007 (the single-filer status is my simplification). The courts treated the limit as a cap on the amount that counts, with interest deductible on debt up to it. The Ninth Circuit says that together the two "can deduct interest payments on up to $2.2 million", and the IRS says it will allow each taxpayer to deduct interest "on indebtedness of up to" the limits.

This does not touch monotonicity_break_general, whose hypotheses include being within the limit, and the paper does stress that LegalLean verifies the encoding and not the statute. But the type I advertised as "the boundary between what a machine can certify and what requires a human" put a translator's error on the machine side. FormalisationBoundary marks where the law is vague. Nothing in it prompts a translator to mark a choice or catches a slip. The paper's faithfulness audit lists three simplifications, and this is not one of them. That essay's open-core section also describes the production route as an automated layer that converts statutes using language models, which is the arrangement this chapter warns about.

One sentence, two translations

The Ashdown instruction, the book's invented example, supplies a sentence to run, a line in the firm's intake rules:

The intake agent may send a document externally if the client has consented, unless the document is privileged, except with a partner's sign-off.

What does the last clause attach to? One competent reader says the sign-off lifts the privilege bar, and the ordinary requirement for consent then applies. Another says the sign-off is a permission in its own right: a partner has taken responsibility, and the document goes.

The trees below use my small model of Catala's default term, in Lean. It restricts justifications to Booleans and consequences to constants, and it is my reading of the published semantics, not the Catala compiler. This block compiles, from lean/BuildingInSteel/Translator.lean:

/-- Reading U. The sign-off undercuts the privilege exclusion and asserts nothing.
    With the exclusion gone, the consent rule decides again. In Catala terms, the
    sign-off is part of the condition on the exclusion. -/
def readingU (f : Facts) : Default Bool :=
  .node [.node [.node [] (f.privileged && !f.signoff) false] f.consent true] true false

/-- Reading R. The sign-off rebuts the exclusion and asserts a permission of its own,
    as the top of a chain of exceptions: default no, consent yes, privileged no,
    sign-off yes. -/
def readingR (f : Facts) : Default Bool :=
  .node [.node [.node [.node [] f.signoff true] f.privileged false] f.consent true] true false

Reading R in Catala's surface syntax looks roughly as follows. This is a design sketch following the book's label and exception syntax. I have not run it through the Catala compiler.

scope Intake:
  label base definition may_send equals false
  label consent exception base definition may_send
    under condition client_consented consequence equals true
  label privilege exception consent definition may_send
    under condition document_privileged consequence equals false
  exception privilege definition may_send
    under condition partner_signed consequence equals true

Here is the theorem the chapter exists for. It compiles, from the same file:

theorem readings_differ_iff (f : Facts) :
    eval (readingU f) ≠ eval (readingR f) ↔ (f.signoff = true ∧ f.consent = false) := by

It is general over all eight inputs and is proved by checking them. It could have been false. A narrower right-hand side looks natural, since the clause seems to be about privilege, but the difference does not need a privileged document. Reading R lets a sign-off carry a non-privileged document out without consent too, because the top exception does not look at privilege.

In the recurring case the client withdraws consent at tick 5. ashdown_witness computes the outcome at tick 6 for the privileged advice with a partner's sign-off: reading U refuses and reading R sends. ashdown_agree_before_withdrawal shows that at tick 4 they agree. So the translator's choice decides whether a partner's signature survives a client's withdrawal, a question Yesterday's Permission treats as one of time, and which here is hidden in the attachment of a clause.

The rest of the inventory, each compiled in that file with propext as its only axiom, or propext and Quot.sound for two_unmarried_owners_differ:

• both_readings_total, general over all inputs: neither reading ever produces a conflict or an empty result. In this model a check for conflicts or uncovered cases has nothing to report on either.
• agree_without_signoff, general over consent and privilege: no test lacking a sign-off can separate them.
• reading_U_reinstates: on a privileged document with a sign-off, the answer under U equals the consent rule's answer. Read as arguments, the exclusion defeats the consent rule, the sign-off defeats the exclusion, and the consent rule is back. My tree reaches that answer by writing the sign-off into the exclusion's condition, so the theorem states the outcome and does not model the defeat.
• reading_R_ignores_consent: under R, a sign-off settles the answer whatever consent and privilege are.
• siblings_conflict_iff, general: a third version, with the exclusion and the sign-off as unprioritised exceptions to the consent rule, conflicts exactly when both fire.
• siblings_not_neutral, computed, and undecided_conflict_iff and undecided_agrees, general: see Silence has an honest encoding below.
• equal_exceptions_still_conflict and firing_exception_wins, over all trees of the stated shape. The first matches CUTECat's note that two raised exceptions conflict "even if they lead to the same result".
• For the real sentence, simplified to one limit: voss_witness computes, for two unmarried owners, a cap of $1,000,000 under the per-residence reading and $2,000,000 under the per-taxpayer reading. two_unmarried_owners_differ proves that any residence with at least two unmarried owners separates them, over every list of further owners. sole_owner_agree proves that a sole owner cannot separate them, married or not, and separate_spouses_agree computes the same for spouses filing separately, the one co-ownership case the sentence names. The per-residence function is my simplification of the Tax Court's position to a ceiling on the total.
• per_debt_loses_aggregate computes that two $700,000 loans pass a per-debt test and fail the aggregate one. This is the shape of my LegalLean mistake, not a reading anyone argued for, and per_debt_agrees_on_one_loan shows why one-loan tests would never catch it.

A test suite of sole owners and separately filing spouses cannot separate the two readings of § 163(h)(3)(B)(ii), and a suite of one-loan cases cannot expose my per-debt error.

Three things follow.

Well-definedness cannot pick. The properties the Catala team sets out to prove first are absence of conflicts and coverage of all cases (Delaët, Merigoux and Fromherz, ProLaLa 2022), and in my model both readings have them. CUTECat generates test cases covering branches and finds conflicts, which is valuable and is a different job. It would meet neither reading as a defect, because neither has one by that measure.

Catala's alarm rings only for a translator who has not yet chosen. Catala's conflict error is its best feature against silent interpretation. Write the two exceptions side by side, as in siblings, and the program aborts on the input where they collide, with the book calling that "an invitation to call the lawyer". LegalLean's isDeductible has nothing like it. The repository's generic solve, which the paper does not present, comes closer: when every undefeated rule shares one priority level, it returns boundary, for a human authority. But a translator who writes the chain has already picked a priority, and the alarm stays silent, as solve does when priorities differ. Writing them side by side is no guarantee either, since the alarm covers the collision the translator wrote down and not the disagreement the sentence contains. The book calls the chain the most usual pattern in legal texts. A pair writes the chain after the conversation with the lawyer. Nothing makes a language model wait for that conversation.

Silence has an honest encoding. Merigoux's report records a real collision in French housing benefit, a room within a larger unit that is also shared with flatmates. Asked which rule applied, the responsible administrative office replied: "As this situation is far from reality, it has not been dealt with." He calls this a delayed form of decision that clashes with the nature of computer programs, and says the best option could be for the program to crash and instruct a human review. Formalising loses what that silence was doing: it left the question open for someone with standing to close it. Readings U and R each destroy that. siblings does not restore it: siblings_not_neutral shows it sends a signed, unprivileged document without consent, as R does, and aborts a consented, privileged, signed document on which U and R agree. Declining to rank two exceptions is not declining to choose between two readings. The honest encoding is undecided, which undecided_conflict_iff proves aborts exactly where U and R differ, and undecided_agrees proves gives their common answer everywhere else. It can only be written once someone has named both readings. Where nobody with authority has decided, I think that abort is the correct translation, and this is the one place where I would rather have a crash than a theorem.

How defeat theorists would write this

Reading U is an undercutter and reading R a rebutter, in John Pollock's distinction as the Stanford Encyclopedia reports it, and Henry Prakken's framework for structured arguments separates attacks on an inference from attacks on a conclusion (Prakken, 2010). U attacks the exclusion's applicability and concludes nothing. R asserts the opposite of the exclusion and wins on priority. The outcome reinstatement predicts holds under U, as reading_U_reinstates shows, though the tree has no defeat relation from which to derive it. The inductive type of trees cannot contain a cycle of priority, so that is true by construction and needs no theorem.

Defeasible logic says this more directly than my trees. Its defeaters "are rules that cannot be used to draw any conclusions. Their only use is to prevent some conclusions" (Antoniou, Billington, Governatori and Maher, 2001). As a sketch I have not run: consent ⇒ send, privileged ⇒ ¬send, with the second rule superior to the first. Reading U adds consent, signoff ⇒ send, superior to the exclusion. Reading R adds signoff ⇒ send, also superior. The translations differ by one premise, which is easier to see than my nesting, though this U asserts send where my tree's U asserts nothing; the outcomes match. And the logic offers a behaviour my trees lack: signoff ❀ send, a defeater superior to the exclusion, stops ¬send from being concluded but, because only strict and defeasible rules can counterattack in that paper's proof theory, leaves send unproved too. That is a refusal to decide with no abort. The deontic versions of that logic also separate obligation from permission, which my Boolean does not: my false conflates "forbidden" with "no rule permits it", and that collapse is a translator's choice I am making without a theorem to show for it.

My model also takes every fact as given. It does not say who must prove the sign-off, or what happens when nobody knows whether consent was withdrawn. Prakken and Sartor treat burdens of production, persuasion and tactical burden as things a logic of presumptions has to characterise (Prakken and Sartor). I have not modelled them, so each tree is a thinner object than the sentence.

Open texture is a different thing again. H. L. A. Hart's "penumbra of debatable cases in which words are neither obviously applicable nor obviously ruled out" (Hart, 1958) concerns whether a word reaches a case. Nothing is vague about "$1,000,000". The doubt in Voss is a silence about what a limit quantifies over, and the doubt in Ashdown is structural. That is why LegalLean's boundary type, built for vagueness, did not catch it. A translator's choice does not become valid law by compiling. Who Gets to Write the Specification? maps those secondary rules onto specification systems. The Ninth Circuit could settle the reading in its circuit and the IRS could acquiesce for itself. A pair inside an agency carries the agency's delegated authority, which is why the Catala book wants the legal department in the team. A vendor's translator carries none, and its choice merely runs.

Compiling a statute and proving things about it

"Why not just use Catala?" is the right question, and for computing a benefit or a tax the answer is that you should.

The narrow technical answer to what Lean adds is this. two_unmarried_owners_differ quantifies over every list of owners, and equal_exceptions_still_conflict over every remaining exception. A Catala assertion is an expression attached to a scope that "should always be true", used for checks and tests on the scope. Universal statements in the Catala ecosystem live in F★ and in solvers: the compiler repository has a Z3 backend for verification conditions on the absence of empty and conflict errors (Catala, compiler/verification), and the proof platform paper aims at connections to several backends. So the capability exists there, spread across tools with different trust bases, and I am not claiming Catala cannot do it. On my eight-input example a truth table or Z3 finds the witness just as well. What Lean gives is one kernel that checks the encoding and the theorems about it, with a proof term anyone can re-check, including statements comparing translations rather than running one. That is a complement to a language built for lawyers, and a modest one. Its price is that it is not written for lawyers to review.

What exists and what is proposed

The proposal. A machine-produced translation of a legal sentence does not merge until it has three things attached: a second reading, produced independently; the set of inputs on which the two differ, computed as a theorem, a product program or a solver query; and a record of who chose, under what authority and on what date, or an explicit abort where no one with authority has chosen. The rejected reading stays in the repository as an executable artefact, so that when a court rules as in Voss the switch is a change of one recorded decision. A Catala test scope could hold all of this today, and the book already asks teams to document the ambiguities they found and how they resolved them. What I add is making that record a build condition, because a comment is prose and nothing fails when it is missing.

Prior art. The nearest work is the date-ambiguity analysis above and the Catala book's practice of documenting choices. Witt, Huggins, Governatori and Buckley ran three legally trained coders over parts of the Australian Copyright Act 1968 for two weeks. After a meeting to agree key atoms, the terms rules are built from, average atom similarity was 57.64% in the second week against 4.27% in the first, while rule similarity was 1.01% against 0%, or 38.72% against 16.85% after manual cleaning, chiefly of syntax, and the coders "made a range of divergent interpretive choices that necessitated legal evaluation" (Witt et al., 2023). They warn that three participants, encoding different provisions each week, cannot support general findings. Agreed atoms and cleaned syntax still left most rules unshared. Lawsky writes that formalising "won't eliminate" tax law's ambiguities, and that the Catala approach helps highlight them (Lawsky, Coding the Code, 2022). Her A Logic for Statutes, cited above for its logic, formalises § 163(h) itself and flags a different ambiguity in this same limit: whether the $1 million is part of the definition of acquisition indebtedness or a limit on how much of it there may be. She says the issue "has been extensively litigated" and that drafters who formalised "would have had to decide". That is my thesis at the drafting stage. Machine translation is also past the hypothetical stage. Lorenzo, Pietromatera and Holzenberger built a benchmark for generating Catala from legal text with language models, and write that Catala "forces the programmer to commit to one interpretation", trading multiple readings for the ability "to thoroughly represent one interpretation" (NLLP 2025). Horner, Mateis, Governatori and Ciabattoni, on language models producing defeasible deontic logic, write that "each encoding is an interpretation" (arXiv 2506.08899). Neither evaluation measures how often a model chooses without saying so, which is the gap the gate addresses. Grimmelmann treats programs as texts with legal-style layers of meaning (Grimmelmann, 2023). Layman Allen was arguing for symbolic logic in drafting in 1957 (Allen, Yale Law Journal); I have confirmed that citation and have not read the article.

Goodhart. Require a second reading and you will get one, cheaply and useless. A model asked for an alternative can produce a strawman that differs on an absurd input, so the box is ticked and the real ambiguity stays. Two translators drawn from one model family may share blind spots, and I have no measurement of that. The difference set is only as good as the imagination behind the second reading: my per-debt error is a reading nobody would have proposed as an alternative, and it would have got past any gate that compares argued positions. So measure the gate by what it has caught that a court or a lawyer later confirmed, not by how many witnesses it has logged. A witness count is the metric to refuse.

Objections

"Programmers have always interpreted statutes. Nothing here is new." Mostly right, as the section on Catala shows. What has changed is the price of skipping the conversation. Merigoux's 50 hours, most of them spent deciphering the text, were the control. Verdict: the phenomenon is old, and removing the human who noticed it is recent. I would drop the claim if a controlled study showed language-model translators flagging interpretive choices as often as a lawyer and programmer pair.

"Your Ashdown sentence is invented, and bad drafting is a drafting problem." The drafting complaint is fair for Ashdown: anyone writing that rule should rewrite it. But Congress wrote the Voss sentence, and three judges and a tribunal split over it. Better drafting helps new text and does nothing for the stock of existing law. I would change my mind if a survey of encoding projects showed reading choices of this kind to be rare, which the Catala team's 70% to 90% figure makes me doubt.

"Courts decide what statutes mean. The translator writes nothing." Correct as a statement of validity, and my title overstates it to that extent. Voss and Sophy litigated. For everyone whose case never reaches a tribunal, the executed reading is the rule they live under. A Proof Is Not an Appeal takes up what contest requires. My verdict: the translator writes the rule for whoever does not contest it. Evidence that automated decisions are routinely contested and corrected at scale would weaken this.

"Then keep lawyers in the loop and stop." Where the budget exists, I agree, and Catala's method is the one to copy first. The gate is for where the economics have already gone the other way, which includes the route my own essay described. If pairs prove affordable at the volume of machine-generated rules, the gate is redundant.

Predictions

1. By 31/12/2028, no peer-reviewed study will show a language-model translator, not prompted about ambiguity, flagging at least half of the interpretive choices that a lawyer and programmer pair flags on the same statutory provisions. A study reporting that result refutes this.
2. By 31/12/2028, CNAF or the French tax authority will have stated publicly that a named production calculation runs on Catala, and no national tax or benefits agency will have stated that a production calculation has its rules encoded in a general-purpose proof assistant such as Lean, Rocq or Isabelle. Either a missing Catala statement or such a proof-assistant statement refutes this.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.