Markdown for LLMs

Assist formalization and review

The source Markdown for this article. Copy it into your assistant or download it as a text file.

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

```text
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](/guide/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):

```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:

```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:

```text
/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:

```text
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:

```text
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`:

```text
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

```sh
# 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](/guide/mcp/).

## Validation record

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](/agent-engineering/evaluations/)
Next: [Agent Engineering with Arxo](/agent-engineering/)