Assist formalization and review

The rest of this section is about an agent that applies a canon to a case. This page is about an agent that helps build or review one: it turns a source (a statute, a standard, a methodology) into a draft executable model, or checks someone else’s draft. Five stages, each catching a different class of mistake: prepare, check, execute, compare, hand to review. A draft is not a canon until a human approves it.

In this repository the two matching skills are formalize-act (create or extend a canon) and audit-formalization (an independent review of an existing one); an assisting agent should load them rather than restate their rules.

Prepare the draft

Start from the pinned source text, never from a summary or memory: dates, rates and thresholds in a brief may differ from the text.

Output

Status: labeled pseudocode (the preparation loop).
pin the source text with its effective dates
  -> read the articles the draft will cover, in full
  -> choose the smallest executable form that keeps the meaning
  -> write rules with source labels, one article at a time
  -> keep quotations and official labels in the source language

Generated text between generator markers is never edited by hand, and every construct choice is proved by execution later: a sentence in a note is not evidence that a form runs.

Check the draft

Build first, check second. Checks confirm shape (names resolve, types fit, references point somewhere) and prove nothing about meaning. A rule that never fires is found only by execution, and an unresolved bare parameter name can pass every static check and fail only at evaluation. Keep the check output with the draft for the review.

Execute the draft

Run the draft’s own tests plus targeted questions over known facts. Every new or changed rule gets at least one firing case and one near-miss case before review: with only firing cases the boundary is untested; with no firing case the rule may be dead.

Reference case: kz-labour-code (Labour Code of Kazakhstan), predicate feeding_break_too_short. Status: files read and MCP calls ran on 2026-10-03 (details in the Validation record).

• The package ships the question card feeding-break-too-short with the template evaluate truth(feeding_break_too_short(<employee>, <employer>)); and four boundary tests.
• The tests pin both rules: one child, 25 minutes fires the thirty-minute rule (TRUE_ONLY); one child, exactly 30 fires nothing (NEITHER); two children, 30 fires the sixty-minute rule (TRUE_ONLY); two children, exactly 60 fires nothing (NEITHER).
• law_ask with 20 minutes, one child, legal time 2026-09-01 returns TRUE_ONLY through the one-child rule; the English law_rules listing names both rules with their premises.

These tests do not probe the nearest miss below each threshold (29 and 59 for integer minutes). A < 60 mistyped as < 59 would still pass at 30 and 60; only 59 tells them apart. Add those values when the boundary itself is under review.

Compare against the source

For each covered article:

1. Quote the article in the source language.
2. List the draft rules labeled with it.
3. Run its boundary cases and read each status exactly: NEITHER is not negation, so a “must not” in the source needs its own negative coverage.
4. Name every article the draft does not cover, and every rule no article labels.

An argument-map probe (law_argue) over the same facts can strengthen the comparison: read its verdict together with the skipped rules and the coverage note, because “no argument” with a skipped decisive rule refutes nothing. Status: the recorded attempt was refused at call time (semantics revision skew between imported packages; message in the Validation record), so no verdict was observed. Reproduction: call law_argue with the feeding-break facts (20 minutes, one child, 2026-09-01).

Hand to review

The handoff to the reviewer carries the pinned source addresses, the draft, build and check outputs, the execution record (firing and near-miss cases per rule), the article-by-article comparison with gaps named, and the open questions. The reviewer’s verdict has a native record shape, review_approval (law.review/0.1); human judgments along the way use law.serve.decision-record/0.1. A workbench report over an edition-versus-draft pair is a recommendation: the draft stays out of the relied-upon canon until approved, and finishing the checklist is not grounds for approval.

A draft is usable when	Shown by
The source is pinned and read in full	source addresses in the handoff
The smallest form is chosen	one article at a time, labeled rules
Build and checks are clean	recorded outputs
Every rule ran both ways	firing and near-miss cases
Behavior matches the source	article-by-article comparison
Gaps are named	uncovered articles listed
A human approved	signed review record

Writing canon text from the editor side: the editor.

Walkthrough: a toy draft to a review handoff

A non-legal subject: “a shift over 6 hours needs a tea break of at least 15 minutes”. Scratch files in /tmp/toy-teabreak (source.law, tests.lawtest, law.toml); no corpus package was touched.

Status: ran locally (./law engine parse/check/lower/test, 2026-10-03). The draft in its final form (line wrapping adjusted; the first version wrote minutes <= 15, which execution caught):

Arxo Law

language "law.core" version "0.2";
package toy.teabreak version "0.1.0";
namespace "urn:toy:teabreak";

// Toy subject for the formalization walkthrough (not law): a canteen rule.
// Rule 1: a shift over 6 hours needs a tea break of at least 15 minutes.
// Anything shorter is too short.

entity Employee {
    label en unofficial "Employee";
}

entity Employer {
    label en unofficial "Employer";
}

relation shift_hours(employee: Employee, hours: Integer) kind empirical {
    label en unofficial "hours worked in the shift";
}

relation tea_break_minutes(employee: Employee, employer: Employer,
    minutes: Integer) kind empirical {
    label en unofficial "tea break length in minutes";
}

relation tea_break_too_short(employee: Employee,
    employer: Employer) kind institutional {
    label en unofficial "tea break shorter than the minimum";
}

rule TeaBreakAfterLongShift(
    employee: Employee,
    employer: Employer,
    minutes: Integer,
    hours: Integer,
) strict {
    label en unofficial "Toy rule 1. A shift over 6 hours needs a break of at least fifteen minutes";
    when shift_hours(employee, hours);
    when hours > 6;
    when tea_break_minutes(employee, employer, minutes);
    when minutes < 15;
    then tea_break_too_short(employee, employer);
}

tests.lawtest holds three tests; the first, quoted in full:

Arxo Law

language "law.core" version "0.2";
package toy.teabreak version "0.1.0";
namespace "urn:toy:teabreak";

// Eight-hour shift, ten-minute break — too short.
test "toy-teabreak-short" {
    given {
        context {
            decision_time @2026-09-01T12:00:00+06:00;
            knowledge_time @2026-09-01T12:00:00+06:00;
            legal_time @2026-09-01;
            timezone "Asia/Almaty";
        }
        assert "t1-0": shift_hours(
            entity_ref("urn:toy:employee:1"), 8) { origin case_input; }
        assert "t1-1": tea_break_minutes(
            entity_ref("urn:toy:employee:1"),
            entity_ref("urn:toy:employer:1"), 10) { origin case_input; }
    }
    evaluate truth(tea_break_too_short(
        entity_ref("urn:toy:employee:1"),
        entity_ref("urn:toy:employer:1")));
    expect truth_status == TRUE_ONLY;
}

The other two have the same shape with assertion ids t2-* and t3-*: toy-teabreak-exact (8 hours, 15 minutes, expects NEITHER) and toy-teabreak-short-shift (6 hours, 5 minutes, expects NEITHER; the rule covers only long shifts).

Check. The first parse failed on every label, five copies of one finding:

Output

/tmp/toy-teabreak/source.law:14:14: error LDC-E0201: expected a name
(label status: official | unofficial | translation (§218))

Adding the label status unofficial fixed it; parse then exits 0 silently, and the shape check prints:

Output

check OK: /tmp/toy-teabreak/source.law

Lowering produced the IR (artifactHash sha256:9ab87f5a19bd4a24e22df2d83cc79763ab5f36b92c13d4d92cd3d948bd6078df, 6 nodes).

Execute. Against the first draft the boundary test failed:

Output

test PASS: toy-teabreak-short
test FAIL: toy-teabreak-exact
  truth_status == NEITHER: in the document TRUE_ONLY
test PASS: toy-teabreak-short-shift
lawc test: 2/3 tests passed

The <= fired at exactly 15 minutes. After the fix to minutes < 15:

Output

test PASS: toy-teabreak-short
test PASS: toy-teabreak-exact
test PASS: toy-teabreak-short-shift
lawc test: 3/3 tests passed

Compare. The source is one sentence. The boundary pair covers its threshold both ways and the short-shift case covers the guard; nothing else is claimed.

Hand to review. The draft, the outputs above, the execution record with the found-and-fixed boundary failure, the sentence-to-rule comparison, and one open question: do minutes arrive as integers from every caller? The walkthrough approves nothing; a human still has to.

How to verify

Terminal

# Status: ran locally on 2026-10-03, from the checkout root,
# after recreating the scratch files from the walkthrough.
./law engine parse /tmp/toy-teabreak/source.law
./law engine check /tmp/toy-teabreak/source.law
./law engine lower /tmp/toy-teabreak/source.law | head -c 300
./law engine test /tmp/toy-teabreak/tests.lawtest \
  --program /tmp/toy-teabreak/source.law

Feeding-break reproduction: over an MCP server whose profile includes kz-labour-code (the public endpoint, root route), ask the truth question (20 minutes, one child, legal time 2026-09-01) with law_ask, and request the English law_rules listing for feeding_break_too_short. The card and its four tests live in the package’s question catalog (analysis/questions.json); the boundary expectations live in its threshold test file (tests/porogi/01-nedostizhimye-porogi.lawtest). Call shapes: Connect an AI assistant.

Validation record

Show commands, versions and results

Date 2026-10-03. Local engine: law 0.1.1, semantics law.core/0.2, binary sha256:7fddf8d081e7fd527c36cc0393aea6cbf9e00ea814e960a76ac701f74794c01f. MCP evidence came over direct stdio to the checkout’s prebuilt MCP server with profile kz (server arxo-law-kz 0.1.0), because the session’s harnessed MCP connection was closed.

Check	Result
Question card, template, four test names; four expectations	read in the package files named above
law_ask truth, one child, 20 and 25 minutes	COMPUTED / TRUE_ONLY via the one-child rule
English law_rules listing	both rules with premises
law_argue over the feeding-break facts	refused, isError, no structured code: Ошибка: мир не слить: пакет "calc-obligations" объявляет семантику 0.2.2, остальные — 0.2.4; NOT RUN as evaluation
Record shapes law.review/0.1, law.serve.decision-record/0.1	read in the checked-in record helpers
Toy walkthrough	parse: five LDC-E0201, fixed; check OK; IR hash above; tests 2/3, then 3/3

Previous: Evaluate, debug and upgrade Next: Agent Engineering with Arxo