In Rigour by Design I argued that almost everyone is parked on the bottom rung of the spec ladder, and that what GenAI actually made cheap is the labour of climbing. That post ends with a link to a repository and one sentence of description. This post is what is actually in it.
It is a working log. Some of it worked, a good deal was wrong until execution proved it wrong, and one whole architecture was deleted. What the thing buys is reproducibility: the same question returns the same answer, with the provision that decided it attached, and that comes free with the representation. What nothing in here checks is whether the encoding reads the statute correctly in the first place. The failure modes were more instructive than the successes, so I am going to be precise about which is which.
The short version: I took the Singapore Land Titles Act and tried to express it as a SWI-Prolog program you can run, where every rule cites the provision it encodes and every answer reads back to the source. Then I tried to get a language model to write that program, behind deterministic gates that decide whether its output is admissible.
One thing changes how everything below should be read: none of the Prolog was written by a human. That covers the libraries the authoring loop produced, and also the ones I will call reference libraries, which were authored interactively, with me directing and reviewing while the model typed. So the axis that does real work here is how the code was produced: interactively, under review, with unbounded rounds and a human in every one against one call per domain, checked by a gate, with no human in the loop at all. What a human contributed is the representation, the gates, and the judgment about which encodings were wrong.
Contents
- What the Experiment Was
- Version One, and Why It Was Deleted
- The Representation: Nine Predicates
- Where the Model Sits, and the Gates That Contain It
- What the Gates Actually Caught
- Asking Questions of the Program
- Compiling the Spec Down to Readable Python
- The Tradeoffs, Stated Precisely
- What This Does Not Establish
- The Scale Ceiling
- What Is Actually Novel Here
- When to Do This, and When Not To
- Back to the Ladder
What the Experiment Was
The thesis, in the form I wrote it down mid-session:
Instead of giving a pile of prose to an LLM and having it answer questions or convert it into code, with the prose forever dependent on a human or a model to interpret it as a “spec”, build a formal logical specification which is almost an intermediate language: portable, queryable, and convertible into executable code with a high degree of mechanisability.
That is the spec ladder argument with a concrete artifact attached. Domain: land administration, so titles, instruments, caveats and mortgages. Source: imperfect markdown. Output: a logic program plus provenance, where every asserted term traces back to the character span that justifies it.
One constraint shaped everything else. All inference in the hot loop was meant to be strictly local, which means Ollama, a 7–8B model, on hardware you own. That constraint comes from the documents: a land registry’s files cannot leave the building. And a 7–8B model cannot be trusted to author a formal specification. So the whole architecture answers one question: what can you get out of a weak model, if a deterministic checker gets the final say?
Version One, and Why It Was Deleted
The first architecture was the obvious one: bootstrap an ontology from the document, extract facts per segment, extract rules by having the model fill slots in fixed templates, compile to Prolog, validate with a meta-program, feed the findings back into a refinement loop.
It ran end to end on real statute text with qwen2.5:14b locally, and the headline result is why I still believe the guardrail principle. Every output compiled to valid Prolog and loaded clean in swipl. Normalisation produced valid atoms for all 33 proposed entity types and 56 relations. Closed-world extraction skipped 38 fact candidates that used unknown relations or the wrong arity. Template-only rules made all 69 constraints well-formed by construction.
The form was perfect. The meaning was bad, and that is the finding. The model turned s.119(4), a directional prohibition reading “the Registrar shall not register a dealing prohibited by the caveat”, into a symmetric mutual exclusion: structurally impeccable, legally inverted. It converted nearly every relation into “every caveat must have X”. It filled typed argument slots with the literal word "string", and these promoted to accepted, because the type checker validated literal positions while ignoring literal values. And given a bare citation line with no normative content at all, it hallucinated five rules with fabricated quotations.
That last one is the most useful, because the fix was deterministic and worked completely: require every proposed rule to carry an evidence quote, and reject it unless the quote is a literal substring of the segment. All five were rejected. Paraphrased evidence correlates with bogus rules, and a substring check suppresses them with no model in the loop.
But no amount of guardrailing fixed the central problem. The representation was too weak to carry the meaning.
- Time was a string.
"2019-03-03", or worse,"the third business day after filing". Prolog cannot order strings, so “what held before X”, “is this within 21 days” and “which registration came first” were all unaskable. Statutes are made almost entirely of those questions. - Identity was a name. Ids hashed
type:name, which over-merges (every “mortgage” collapses to one) and under-merges (“the mortgage”, “first mortgage”, “second mortgage” fracture into three) simultaneously. - A type was one opaque atom, so every distinction got crammed into the label:
registered_mortgagebakes an event outcome into a name where nothing can reason about it. - Facts had no context.
register(registrar, mortgage)asserted flatly is implicitly true everywhere, which is false. Torrens land law turns precisely on the register differing from the world, and on what a party knew.
So it went: around 11,800 lines deleted in two commits, and the modules serving the old representation went with it. The temptation is always to keep the code and patch the model underneath it. But the stages encoded the bad representation, and maintaining a stage that emits a vocabulary nothing downstream reads is worse than having no stage.
The Representation: Nine Predicates
What replaced it is a coordinate model. The domain-neutral core is nine names in 97 lines, mentioning no dimension, no sort, no relation and no verb:
ist(Ctx, Statement). % Statement holds in Ctx
asserts(Ctx, Record). % INDEX -- whose account. Not a dimension.
mark(Ctx, Dim, at|lower|upper, Value). % where Ctx sits on a dimension
dimension(Dim). % declared per domain
within(Dim, Point, Extent).
precedes(Dim, P1, P2). % OPTIONAL, strict; its presence enables bounds
offset(Dim, Point, Quantity, Point2). % OPTIONAL -- point construction
at_or_before(Dim, A, B). % derived
holds_in(Statement, QueryContext). % derived -- the only query form
ist is McCarthy’s “is true in context”, lifted whole from Notes on Formalizing Context (IJCAI-93). The generating rule is one sentence:
Anything with its own lifetime gets an id, and its value or extent attaches to that id. Anything that varies gets a dimension. Whether something “holds” is membership of a query position inside an extent.
Three consequences follow, and each removed a problem I expected to need machinery for.
There is no Event Calculus. An event is a context positioned at a point, a state is a context with a lower bound and possibly an upper one, and persistence is extent-completion by derived mark/4 rules. So inertia follows from any dimension carrying a directed order, which means the version dimension has it too. “In force from the 1993 Act until repealed” is structurally the same shape as “effective from registration until discharge”, and the same machinery answers “was this a caveat under the Act as it stood in 1990?” and “was it effective in mid-2020?”
Types are patterns you ask at a point. caveat(Cav, Q) is a rule, so the registered_mortgage problem disappears at the root.
Closing conditions need no ordering logic. An extent is clipped if any upper mark falls in the gap, so “earliest terminator wins” fell out of the definition without being implemented. A caveat that can lapse at five years, be withdrawn expressly, or be deemed withdrawn fourteen days after an unrectified deficiency notice just has three upper mark rules, each citing its own provision, and they compose:
% s.121(1)(b) "at the expiration of 5 years from the date of the lodgment"
% -- an UPPER bound, and the reason offset/4 exists: the point is
% CONSTRUCTED, not compared.
mark(ctx(effective(Cav)), time, upper, T2) :-
ist(CL, lodges(_, Cav)), mark(CL, time, at, T1),
offset(time, T1, years(5), T2).
% s.117(3) "if, within a period of not less than 14 days ... the caveat is
% not rectified, it shall be deemed to have been withdrawn".
mark(ctx(effective(Cav)), time, upper, T2) :-
ist(CN, notice_of_deficiency(Cav)), mark(CN, time, at, T1),
offset(time, T1, days(14), T2),
\+ ( ist(CR, rectified(Cav)), mark(CR, time, at, TR),
at_or_before(time, TR, T2) ).
One rule, one provision, one citation. That is Bench-Capon and Coenen’s isomorphism principle from 1992, and it is what turns an amendment into a mechanical edit instead of an audit. Fourteen provisions in the caveat library point at character spans into a content-addressed document version, and a gate checks that every declared provision actually cites text. On its first run that gate found a dead declaration: a provision nothing called, left over from an abandoned modelling attempt. What it found was dead vocabulary, which is a defect the compiler had no way to see.
Three sorts (entity, quantity, text) and four dimensions (time, version, space, money). “Dimension” turns out to mean ordered value domain, and positioning a context in one is optional: nothing is positioned in money, but its precedes/3 and offset/4 are exactly what “exceeds $500” and “the residue after costs” needed. Quantity arithmetic looked like a gap in the vocabulary and was actually a value domain nobody had declared. Four clauses closed it.
Where the Model Sits, and the Gates That Contain It
The founding tenet: the LLM never writes Prolog and never invents structure. It fills schema-constrained slots, and deterministic code compiles terms.
That tenet survives where it matters, which is the hot loop, thousands of calls per corpus, a weak local model. It was deliberately broken in one place. The authoring tier is one call per domain, and its output is small, static, and mechanically checked before anything depends on it. A Pydantic schema plus a JSON to Prolog compiler would buy back one frontier call per domain, at a cost of several hundred lines and a second copy of the grammar to keep in step with the checker, and it would only ever fix violations the shape gate already catches. Every defect that actually produced a wrong answer cleared the shape gate and needed execution to find. The question was asked twice and answered no twice, with revisit conditions written down: if authoring starts running per-document; if the repair loop stops converging in about two rounds; or if something other than swipl consumes the output. A tenet with stated conditions for its own reversal is worth more than a tenet.
flowchart TD
subgraph OFF[Offline -- once per domain]
DOC[statute / policy wording] --> FM[frontier model\nproposes a pattern library]
FM --> G1{Gate 1 + 1.5\nshape · content}
G1 -->|machine-readable violations| FM
G1 -->|accepted| LIB[pattern library\nrelations + cited rules]
end
subgraph HOT[Hot loop -- per segment, NOT BUILT]
SEG[document segments] --> LOCAL[local 7-8B\nentities · relations · dates only\nnever Prolog, never a type name]
LOCAL --> DET[deterministic compile\nto ist / mark]
end
LIB --> G2{Gate 2\nrun against an\nINDEPENDENT corpus}
DET --> G0{Gate 0\ncorpus vs declarations}
G0 --> G2
G2 --> RUN([runnable program\n+ provenance])
classDef default fill:#dde3f5,stroke:#6b7db3,color:#1a1f5e
classDef llm fill:#ede0f8,stroke:#7b2d9b,color:#3b0764
classDef gate fill:#d4edda,stroke:#388e3c,color:#1b5e20
classDef missing fill:#fce7f3,stroke:#be185d,color:#831843
class FM,LOCAL llm
class G0,G1,G2,RUN gate
class SEG,DET missing
The dashed-in-spirit box is real: the hot loop does not exist yet. More on that below.
There are four gates, and none subsumes another.
| Reads | Catches | In the repair loop? | |
|---|---|---|---|
Gate 0 fact_check.pl |
a corpus, against a library’s declarations | undeclared relations, arity mismatches, a mark kind contradicting the relation’s declared class | yes |
Gate 1 shape_check.pl |
the library file | grammar: legal goals, sorts, exactly one cited provision per rule | yes |
Gate 1.5 content_check.pl |
the library file | a library that is perfectly on-grammar and authors nothing | yes |
Gate 2 acceptance.pl |
the library run against a corpus | rules that derive nothing, rules that derive everything, two rules with identical extensions | no, deliberately |
Gate 2 sits outside the loop on purpose. It needs a corpus, and a corpus authored to satisfy the gate compromises the gate. A model that writes its own fixtures writes them to agree with itself.
The repair contract is blunt. A checker returning a negative verdict wants a repair, and the violation list goes back as the next prompt. A checker that raises is saying no repair exists, and the loop propagates it. Exhausting the round budget counts as a result that the caller has to interpret. And one detail decides whether any of it works: the gate must return specific, machine-readable violations. undeclared_relation(effective/1) is actionable. “Try again” is not. An early run reported “0 violations” four times in a row and gave up, which is the degenerate case of the same principle: a rejection carrying nothing the model can act on is just a refusal.
What the Gates Actually Caught
Land Titles Act, ss.115–121. claude-sonnet-4-5 via Bedrock at temperature 0, chosen over the strongest available model deliberately, because a weaker one tests the gate harder. The first one-shot experiment came back SHAPE_FAIL with 13 violations, and the split is the finding. Everything the prompt warned about, it got right: event/state classes assigned correctly, rule-precedence machinery left untouched, no context variable shared across conjuncts, a core derived type all but identical to the reference library’s, plus 28 derived rules and 14 provisions cited. Everything it got wrong was bookkeeping. The silent semantic kind, which took three attempts to get right in the reference libraries with a human reviewing each one, never appeared. Wired into a repair loop, the same task converged in two rounds: two violations, then SHAPE_OK with 17 relations, 16 provisions, 25 derived rules and 9 derived mark rules. A second domain, the NY standard fire policy, chosen because an insurer’s wording is copyright and this one is a statutory form, behaved identically: 10 violations in round one, SHAPE_OK in round two, and again everything caught was vocabulary discipline.
And the accepted library was better than the reference library in one place, which is worth recording. For s.119(1) it declared acceptance as an event and being-in-order as a state whose lower bound derives from that event, where the reference library treats the latter as the event itself. One call plus a gate applied the discipline the prompt teaches, at a point the reviewed interactive sessions had let slide. More rounds with a human in each of them is not uniformly better than one round and a checker.
Here is every defect worth reporting, and which gate saw it:
| Defect | Caught by | Consequence |
|---|---|---|
| 6 relations used, never declared | Gate 1 | 8 rules written over a term absent from its own vocabulary |
| a context term naming the wrong statement | Gate 1 | bookkeeping; repaired in one round |
| a fluent context passed where a query context belongs | nothing | fails silently; the gate hole a model found |
| a condition that constrained nothing | Gate 2 | “Alice may lodge lot 5 as a caveat” was derivable |
an acceptance (an event) read with holds_in |
Gate 2 | the duty to notify existed for one day, then disappeared |
| two predicates never once run | Gate 2 | no fixture exercised the provision they encoded |
fixtures discontiguous but not multifile |
Gate 2 | clauses silently discarded; false vacuity, no error |
| a citation carried by all 63 rules, defined by none | Gate 2 | every rule failed on an unknown procedure |
| a library on-grammar, fully cited, authoring nothing | Gate 1.5 | 12, 8 and 30 authoring rules on the shipped libraries, against 0 |
c1 appearing in 36 of 40 scenario files |
Gate 0 | 29 systematic mark-kind errors, down to 6 after namespacing |
Five things follow.
Gate 1 is structurally blind to meaning. Every Gate 2 row above is grammatically perfect. A gate that reads the file can only check the file, and only running it against a corpus finds a rule that derives nothing, derives everything, or derives the wrong thing. The citation row is the sharpest case: the shape gate asks whether a rule carries a citation, and never whether one resolves.
The silent row is the one worth studying. The model wrote \+ holds_in(extended(Cav), ctx(effective(Cav))). holds_in reads at marks off its second argument, a fluent context carries lower and upper instead, so the goal fails without erroring, and no gate said anything because that argument position was unconstrained. It is now checked, and the check exists because a model did something nobody had thought to forbid. I had not expected the loop to find gaps in the grammar itself, and this is the one benefit of it I would not have predicted.
The recurring error got made syntactic. The event/state conflation appeared three times and survived human review each time, so relations now declare a class, as in relation(lodges, [entity,entity], event). The empirical basis is that the class is a function of the relation: across the whole caveat corpus, every extracted relation had exactly one mark kind. So the gate can now reject reading an event as a state, both historical instances are added as tests and caught, and the mark kind is assigned deterministically from the declaration, which takes the hardest judgment in the representation out of the extraction model’s hands. It emits a relation, its arguments and a date, and deterministic code decides whether that is a point or a bound. Find the error you keep making, then find a declaration that makes it syntactic. That is the transferable technique here, and it applies well outside Prolog and law.
An inert library is a real failure mode, and the gap turned out to be total. The screen-validation library asserted “this notice has not expired” as a corpus fact, where the source document gave the expiry date. The document contained everything needed to derive expiry, and the library copied a flag across instead of writing the rule. Two other candidate smells were tried and discarded for firing on the reference libraries, which I mention because negative results in heuristic design almost never get written down. One of them found 24 instances in one authored library and 0 in another doing the identical thing under different names, so what it measured was naming.
The residual 6 corpus errors are a finding. A classification like “this was a fire” or “this was lightning” is neither an event nor a bounded state. The encoder dates it because the narrative dates it, and the library declares it a state. That is a genuine modelling question the representation has not settled, and it surfaced only because a gate counted.
Asking Questions of the Program
A specification you cannot interrogate is barely a specification. So there is a query tier: a question in, a Prolog transcript and an answer out. Four steps, and only the first and last involve a model:
question -> a CHECKED query structure (model, gated)
-> Prolog goals at one or more points (deterministic)
-> answer + evidence read off the marks (Prolog)
-> prose, printed BESIDE the transcript (model)
The model never writes Prolog text. It picks a predicate from the introspected vocabulary, its arguments, and the points to ask at, and deterministic code renders goals and checks them against the loaded program first. Free text cannot be gated, because a goal string can name a predicate that does not exist and the only way to find out is to run it, whereas a structure is checkable in a few lines. The gate is strict about arity for one reason: a goal with the wrong arity fails silently, and a silent failure reads exactly like a well-formed “no.”
Asking at several points is the normal case. Most real questions about a statute are comparative, and the interesting answer is the one that changes:
Alice lodged a caveat over lot 5 in March 2019, and a buyer now wants dealing1 registered against that lot. Is the Registrar barred from registering it in mid-2020, and would that still be so in mid-2025?
?- must_not_register(dealing1, q_mid_2020). % yes
?- must_not_register(dealing1, q_mid_2025). % no
evidence (marks bounding the relevant contexts):
effective(cav1): time lower = d(2019,3,3)
effective(cav1): time upper = d(2024,3,3)
lodges(alice,cav1): time at = d(2019,3,3)
The date that decides this, 3 March 2024, appears nowhere in the source documents. It is constructed by the five-year rule in s.121(1)(b), and the explanation cites it because the engine gathers evidence mechanically: the marks bounding every context whose statement mentions an entity the question is about. Every date in the explanation is read off the program. The prose step is the weakest link and is treated as such. It is given the transcript and nothing else, told not to introduce facts, and always printed beside the run. An explanation nobody can check is worse than no explanation.
Two results from that tier are worth reporting honestly.
The near-miss the gate cannot catch. Asked whether Alice’s underlying claim was justified, the model composed claimant(alice, Q): valid vocabulary, real entity, and a different question, since being a claimant is not the same as having a good claim. The gate checks that a predicate exists. It never checks that the predicate answers what was asked. Vocabulary checking is not semantic checking, and no amount of grammar work makes it so. Both fixes live outside the gate: an explicit route to decline, because a system that cannot say “I can’t” will always say something, and human-readable glosses so near-neighbours can be distinguished in prose where nothing mechanical can separate them. Declining is never retried, since retrying only pressures the model into naming an adjacent predicate.
Which is the point of the pair, because next door sits a question that is correctly declined. Whether Alice’s claim is good needs contract and property law, evidence, and a court. That is the law itself, and no gap in the library will fix it. Whether the Registrar must not consider it is squarely answerable, because s.117(5) says he must not. A statute’s refusal to decide something is itself a provision with content, and the system knows which side of that line it is on.
The lossy rendering. In three recorded examples the query enumerated solutions through an unbound variable and the transcript surfaced only the first. The prose tier then said, correctly, “the transcript does not settle the question.” The Prolog was right, the presentation layer was lossy, and the interpretation step refused to fill the gap by invention. The design worked and the implementation did not. A tier that declines is the better failure, because the alternative is inventing the other three answers.
Compiling the Spec Down to Readable Python
If the specification is the artifact of record, you should be able to project it into the language you actually ship. So there is a generator: a pattern library in, a self-contained Python module out, with one dataclass per entity kind, one method per derived predicate, and one period method per fluent.
Attempt one was rejected, and it passed every correctness test. It was a Prolog-to-Python transpiler: nested closures over a store, generated names like _derived_mark_1 and _Anon29, continue loops. It agreed with Prolog on every enumerated case and it was unreadable, which defeats the entire purpose. Attempt two is expression-first, so a conjunction is and, an existential is any(...), a negation is not. Same correctness bar, output a human can review.
The constraint that decided everything: readability information lives in the spec, never in the generator. A generator that guessed lodges(Party, Caveat) should render as “lodged_by” would be land law in disguise, custom to one statute. Every readable name comes from a declaration the library author wrote. The mortgages library declares none of them and still compiles end to end against the raw statement store, which is what degrading gracefully has to mean, and it is a test.
Here is what comes out for the caveat lapse rules quoted earlier:
def effective_period(self, cav: str) -> Extent:
"""When effective(cav) holds, on the time axis.
s.121(1)(b): "at the expiration of 5 years from the date of the
lodgment of the caveat, ..."
s.117(3): "if, within a period of not less than 14 days ... the caveat
is not rectified, it shall be deemed to have been withdrawn."
"""
caveat = self.registry.caveats.get(cav)
if caveat is None or caveat.lodged_by is None:
return Extent(dim="time", stated=False)
# without the statement there is no context to hang marks on, and an
# unstated fluent covers nothing, which differs from an unconstrained
# one, which covers everything.
...
if caveat.lodged_by is not None and caveat.lodged_on is not None:
ends.append(add_years(caveat.lodged_on, 5)) # s.121(1)(b)
if caveat.deficiency_notice_on is not None and not (
caveat.rectified_on is not None
and caveat.rectified_on <= caveat.deficiency_notice_on + timedelta(days=14)
):
ends.append(caveat.deficiency_notice_on + timedelta(days=14)) # s.117(3)
The statutory limits are on the page as ordinary date arithmetic, the citation is in the docstring quoting the provision, and there is no Prolog runtime hiding behind it. An equivalence suite runs every predicate through both engines and diffs. Two details from building it generalise.
Never emit a ... stub. The first cut emitted ... for every derived predicate. ... evaluates to None, which is falsy, so each stubbed rule silently answered “no”, indistinguishably from a rule that means it. Anything the compiler cannot render faithfully now raises, naming the clause, the goal and the reason, and the module exports an UNTRANSLATED list so you can see which methods are trustworthy without running anything.
The equivalence suite caught four defect classes, each giving a plausible wrong answer:
| Defect | What it did |
|---|---|
| an index running opposite to a dimension | silence about a dimension means unconstrained, while a context asserting no record answers no record-scoped question; the reversed polarity made two copies of the data disagree |
| an empty extent read as unconstrained | a loader bug dropped a field, the date came out None, empty read as “no bounds”, and every caveat was effective forever. stated=False covers nothing, absent marks cover everything, and that asymmetry is the one to watch |
| a dropped conjunct | a derived call with an unbound argument emitted the scan and discarded the call, so it answered yes for any entity at all |
| a rebound parameter | a store pattern named its loop targets after already-bound variables, widening “this mortgage” to “any mortgage” |
Every one produces confident, well-formed, wrong answers, and none is visible by reading the output. That is the concrete argument for keeping two engines and diffing them, instead of trusting a translation.
The Tradeoffs, Stated Precisely
| Decision | What it buys | What it costs |
|---|---|---|
| Nine-predicate domain-neutral core | Two Parts of one Act plus an insurance policy form fit with no core changes. Rule validity over legislative versions uses the same machinery as facts over time. | Sort conformance became nearly vacuous: collapsing to entity plus quantity leaves quantity as the only checkable sort. Real cost, knowingly paid. |
| Types derived, never stored | Kills registered_mortgage-style label pollution outright. |
Every type question costs a resolution instead of a lookup. Irrelevant at this scale, unknown at corpus scale. |
| Frontier model writes Prolog offline; local model never does | One call per domain, and the artifact is small, static and checked. No second copy of the grammar. | Breaks the founding tenet in one place. And the local tier it protects does not exist yet, so the split is architecturally justified and empirically untested. |
| Gate 2 outside the repair loop | The acceptance corpus stays independent of the model that wrote the rules. | A whole class of defect is only found after the loop reports success, and every serious defect so far was in that class. The independence is also only as real as the sourcing. |
| “It checks; it does not compute” | Aggregates need no arithmetic if their value is stated, and for document extraction it usually is. Priority needs no sorting if rank is a declared position. Several problems that looked like they needed a computation layer went away. | Wrong side of the line for any engine that must perform a distribution instead of testing one. |
| One unstratified rule shape accepted | holds_in inside a mark body is genuinely useful when deriving new bounds. |
It can fail to terminate. Accepted deliberately, reproduced in a fixture, and the failure is loud: a stack trace naming the cycle. |
| Provenance as positioned statements | A provision’s span varies by version: s.115 as enacted and as amended are different words in different documents. An amendment adds a citation with its own version bounds and the machinery picks the right one. | More indirection than a citation string on the rule. |
Two things I expected to be hard were not. Partial holding, as in “according to the extent of his interest” or “freed from the mortgage absolutely or to any lesser extent”, looks like it needs graded truth and does not, and the commercial legal DSLs agree: eFLINT parameterises acts, Symboleo parameterises obligations, Catala computes an amount, and none of them makes “holds” partial. A quantity that changes is a reified term whose value varies by context. An extent that limits is an ordinary comparison on the money dimension. Deeming is likewise just a fact whose bound the statute supplies.
Harder than expected: rule precedence. An overrides/2 relation was declared for it, is used in exactly zero rules across two libraries, and both of the Act’s precedence forms defeated it. A conditional carve-out (“except as otherwise provided in s.129(1)”) encoded as an override disabled the whole section, so no dealing was ever prohibited, because the carve-out displaces the section only for the dealings the other section reaches. It is a condition on the dealing, and it lives inside the rule. And the case the mechanism was designed for, “despite any other provision of this Act”, is worse: overriding the general priority rule kills the registration ordering that the overriding provision itself depends on. Both encode correctly as an exception clause inside the general rule, which is Catala’s prioritised-default shape. A reader who sees “except” and reaches for a precedence relation will silently disable a section, and nothing will error.
What This Does Not Establish
This is the section I most want people to read.
Nothing extracts anything. Every fact in every fixture was put into the repository by a model, interactively or by a generation script, and none of it was extracted from a document. There is no seam from a document to ist and mark. The founding premise is extracting a model from imperfect markdown with a local 7–8B model, and in the current architecture that is entirely untested. The demo answers questions about a knowledge base assembled in directed sessions, which is exactly the part a viewer will assume was automated. Building it needs instrument documents, meaning a folio, a lodged caveat, a judgment, and this corpus does not contain them: the Act gives rules, and records live elsewhere.
There is no baseline, and the baseline is the wrong comparison anyway. I never measured whether a strong model, handed the 6KB statute extract and the same eleven questions, answers them all correctly with no machinery at all. It very likely does. But answer quality was never the axis this buys on, and running the race on that axis concedes the wrong thing.
What the apparatus establishes automatically is that the answer is reproducible, and that is a property of the artifact. The same question asked at the same points returns the same answer every time. The date that decides it, 3 March 2024, is constructed by a cited rule, so anyone with the program and the statute can reconstruct it. The evidence is gathered mechanically off the marks. Two independent engines agree or the diff fails. None of that needs an experiment to establish, because it follows from what the thing is, which is a deterministic program with citations. A model asked the same question twice is not obliged to answer the same way, and cannot show you the provision that made the difference. That is the comparison worth making, and it does not turn on which one is smarter.
The load-bearing word is automatically, and its price is the conditional attached to it. Reproducibility holds assuming the encoding is a correct reading of the source, and that assumption is precisely the one nothing here checks. Of the four properties the case rests on, two come free with the representation: reproducibility and reconstructibility. As-at-date reasoning comes free with dimensions, though it is untested at any real scale. Consistency across thousands of documents is genuinely unmeasured, and cannot be measured until the hot loop exists. Faithful reproduction and correctness are different properties, and this project buys the first cheaply and the second not at all.
The gates check hygiene. No gate establishes that a library is a correct reading of its source. A library can be well-formed, non-vacuous, non-degenerate, fully cited, and still misread the provision it points at. Every serious defect found so far was of that kind. A human reading rule against provision is still necessary, made cheap by one-rule-one-provision, and nowhere near eliminated.
The rules and the fixtures they are checked against share an author. This is the sharpest consequence of everything being model-written. The land corpus and the land libraries came out of the same sessions, so a shared misreading would produce a library and a fixture that agree with each other and both diverge from the statute, and every gate would report success. The insurance experiment was designed specifically to break that circularity, and it is the experiment that did not finish. So the independence the architecture depends on is currently a design commitment that nothing has demonstrated.
Sample size is small and the prompt was loaded. Two Parts of one Act plus one policy form, and the “avoided all four failure modes” result is a handful of runs with those four failure modes spelled out in the prompt. Two further runs did not complete and are not counted.
The second-domain experiment is incomplete. The design was a genuine blind test: one call writes forty scenarios with expected verdicts from the policy alone, seeing no grammar and no hint that a logic model exists; that oracle is committed to git before the library is authored, so commit order is the evidence it was blind; a third call encodes the scenarios into facts without ever seeing the verdicts. The library was authored, the corpus encoded, the corpus gate built and run. The final diff, derived answers against withheld verdicts, was never run. So the strongest evidence this experiment was designed to collect remains uncollected, and I would rather say that than quote the parts that did finish as though they were the result.
Coreference is untouched, and it is the biggest live risk. A wrong entity id does not produce an error. It produces a well-formed false statement: a caveat whose lodgement and acceptance get different ids ends up with no lower bound and reads as effective since the dawn of time. The negation ambiguity compounds it, because \+ rectified(Cav) reads “not rectified”, and in a lossy extraction it also reads “we did not extract the rectification”. Those give opposite legal outcomes and the program cannot tell them apart.
The Scale Ceiling
The authoring loop handles a policy wording and a dozen sections of a statute. It does not reach the whole Act, and the reason has nothing to do with the context window, which is the interesting part.
The caveat library covers 7 real sections in 652 lines with 37 rules, so roughly 93 lines and 5 rules per section. The Land Titles Act has 184 real sections, which extrapolates to something like 17,000 lines and 900 rules. No single call produces that, however large its input window, because the binding constraint is the output budget, and the repair contract makes it worse by demanding the entire file back every round. The second constraint is that the discipline decays over the length of a generation. The four failure modes the prompt warns about are exactly the ones a model stops watching for as the output gets longer, and what that produces is misreadings, which the shape gate cannot catch.
There is a design for this. Decompose the document into a structure map of citable spans, cluster, author per cluster, reconcile. Its central commitment is to assume nothing about document structure, because the real target is validation-rule tables, standard operating procedures, and design documents intermingled with architecture docs. Any design keyed on sections and numbered clauses degrades silently on most of that: a document with no citations yields a reference graph with no edges, a perfectly valid graph that produces one cluster per unit and no error anywhere. The one guard in it worth stealing regardless: a span’s recorded text must be a verbatim substring of the source at the recorded offsets. Total, free, mechanical, and the same move as the evidence gate that killed five hallucinated rules on the very first run.
That design is written down. It is not built.
What Is Actually Novel Here
Very little, and I want to be blunt about it, because a project like this generates a lot of prose that reads as claims.
ist(c, p) is McCarthy, 1993, lifted whole. Contexts carrying coordinates is Guha’s 1991 thesis and Cyc’s microtheories. Statute-as-logic-program is Sergot, Sadri and Kowalski’s British Nationality Act paper in CACM, 1986, which is forty years old. One-rule-one-provision is Bench-Capon and Coenen, 1992, cited by name in the code. Derived types as patterns is ordinary Prolog. Fluents and inertia are Event Calculus, same 1986 vintage. Storing extents as endpoint facts instead of interval terms is how temporal databases have stored valid-time for decades. “LLM writes a DSL, a checker rejects it, repair” is a standard pattern by now, and “natural language to structured query to execution to natural language” is text-to-SQL with a validator. The reified-value pattern I made the biggest fuss about is McCarthy and Buvač’s value(c, term), and it was already in the design document’s own bibliography, so the project rediscovered a citation it had in front of it. Catala, meanwhile, already does the defeasibility part properly, with prioritised defaults as a first-class construct where this project has exception clauses by convention.
Three things might be worth something, hedged:
- Turning your most frequent modelling error into a grammar violation. I conflated an event with the fluent it starts three separate times. Declaring the relation’s class made the error syntactically checkable, and both historical instances are now caught as tests. The general move transfers.
- “It checks; it does not compute” as an explicit scoping decision. Several hard problems went away, and for document extraction it is the right side of the line, though the mechanism underneath, uninterpreted function symbols, is entirely standard.
- Dimensions versus indices. “No order at all means it is not a dimension” killed a coordinate that was wrong and replaced it with a plain index. A clarification, and I would not call it a discovery.
A careful assembly of forty-year-old ideas, with one or two sharp engineering moves and a scoping decision that does real work. That is the honest summary, and it is also the point of the previous post: none of this was ever wrong, it was expensive. What changed is that encoding it got cheap enough to try on a weekend.
When to Do This, and When Not To
Not worth it when the document is short-lived, low-volume, or low-stakes; when one competent person can hold the whole rule set in their head; when nobody will need to ask “what was the answer as at a date two years ago”; or when there is no second document to be consistent with. Handing the statute to a good model and asking is faster, and until somebody runs the baseline nobody can honestly tell you it is worse.
Worth considering when the answer must be reconstructible, because a regulator, an auditor or a court will ask why and “the model said so” ends the conversation badly; when the same rules are applied across thousands of documents and consistency between them is the actual product; when the source amends and you need to know what changed and what it broke, which is exactly what one-rule-one-provision buys; when the rules must be queried forwards and backwards, since a relation runs in both directions and a function runs in one; or when the data cannot leave the building, which forces you into a weak model and therefore into a strong checker.
The domain matters more than the technique. This works on governance documents because they already are rule systems: citable units, defined terms, explicit temporal operators, and a tradition of being read literally. A marketing brief has none of that, and no amount of Prolog will give it any.
Back to the Ladder
Everything above is one long attempt to occupy the declarative, machine-checkable rung of the spec ladder, and to find out what it costs in practice. Four things from the earlier post now have receipts, and one has a correction.
“AI proposes; the verifier disposes” is the load-bearing claim, and it held more completely than I expected, because every proposal in the chain turned out to be a model’s: the libraries, the corpora, the query compositions, the projected Python, the blind oracle. The model contributed candidate generation, which is what it is good at, and it contributed to no decision anywhere. What converged was the check.
The uncomfortable corollary is in the comparison the two authoring paths make possible. One had a human in every round, unlimited rounds, and full review. The other had one call and a gate. The gated path produced a better encoding of s.119(1), and the reviewed path is where all three instances of the event/fluent conflation came from. Human review caught the errors it was looking for and waved through the ones it was not. A mechanical check does not get tired at round nine.
“Only a machine-checkable artifact makes an LLM worth looping” held for a sharper reason than I gave it credit for: the rejection has to be specific. A wall of prose cannot fail, which matters, but specificity is what makes the loop converge. undeclared_relation(effective/1) converges. “Your spec seems inconsistent” is not a check at all.
“Least power” decided the local tier. The way to make a 7–8B model safe is to leave it less to decide, down to a relation, its arguments and a date, with deterministic code taking even the mark kind.
The correction, and it is the one that matters. In the earlier post I wrote that a model’s nondeterminism sits in the gap between the spec and the program. That is true and incomplete. Here the nondeterminism moved up, into the gap between the source document and the spec, and no gate I built can close it. Every gate reads the library, or runs it. None of them reads the statute. Well-formed, non-vacuous, fully cited, perfectly reproducible, and a misreading, is a state this system can reach and cannot detect. The gates made the cheap errors free to find, which is genuinely worth having, and they left the expensive ones exactly where they were: with a human, reading a rule against the provision it cites.
That is a smaller claim than “verified”. It is also the honest one, and it is where the work is.
The repository is at github.com/avishek-sen-gupta/doc-pipeline, including the recorded model runs, the round-by-round violation journals, the fixtures that are expected to fail, and the evaluation document recording which encodings were wrong until running them proved it.