What it is. A specification, a schema and a reference checker for legal statements that software can check: a clause is written as a set of Hohfeldian positions, each anchored to an exact span of a pinned revision of a legal text, and a program decides whether the set is internally coherent, fully anchored, and how much of it was actually closed.
What it is not. Not an AI that reads contracts and tells you they are fine. Not legal advice. Not a
theorem prover, not a statute parser, and not a claim that a clause passing the checker is lawful. The
checker never issues a verdict about legality — its reports do print legal validity inside not_claimed, which is the opposite of a claim; it outputs a verdict over a triple (statement, encoding, corpus@revision) and a list of the things it did not check.
Russian mirror: README.ru.md. This file is canonical; where they disagree, this one wins.
Anchor or refuse. An atom without an unambiguous span in a pinned text revision is not a weak claim — it is a different product. A phrase that occurs twice in the text does not anchor anything, because the citation can silently re-point after an amendment (
S2_SPAN_AMBIGUOUS).
Everything else in the repository follows from accepting that rule, including the parts where the tool refuses work it could have done.
"Formalise legal language" is four problems, and collapsing them is how the field produces confident nonsense:
| Layer | Question | What this repo has |
|---|---|---|
| L1 Surface | what does the sentence say, exactly? | nothing: v0.1 does not parse prose. A human or a model proposes a statement, and the proposal is falsifiable |
| L2 Model | which legal position is this? | Hohfeld's eight positions as a closed set, with correlatives and opposites (spec §4) |
| L3 Inference | what follows, what conflicts? | combinational checks only: opposites, time overlap, declared conflict policy. No entailment |
| L4 Provenance | which bytes, at which revision, say so? | every atom anchored by span + sha256 of the corpus file (spec §5) |
The interesting consequence is in L2/L3: because the positions form two squares with known opposites, contradictions between them are combinatorial, so a few hundred lines of Python find them without a prover. "A may not do X" written next to "A may do X" in the same document is not a subtle semantic problem.
python tools/lexcheck.py examples/01-delivery-ok.lex.json # human output
python tools/lexcheck.py examples/01-delivery-ok.lex.json --json # machine report
python tools/lexcheck.py --canonical examples/01-delivery-ok.lex.json # canonical form + sha256
python tests/run_tests.py # the guard suite
python tools/lexspec_status.py # the numbers quoted belowPython 3.11+, standard library only. Nothing to install.
Exit codes: 0 the statement passed, 1 refused, 2 usage or parse error.
Exactly three, in ascending strength. The wording is part of the contract:
| Verdict | Means |
|---|---|
REFUSED |
the statement does not survive checking; every reason carries a code from a closed vocabulary |
CHECKED |
what is encoded is coherent and anchored where anchored, but at least one atom is open and declared as an escape; the threshold is a reporting metric, not a cause (ADR-0010) |
CHECKED_ANCHORED |
every atom is closed and anchored; this is still not a statement about law |
Every report carries at least these, verbatim:
"not_claimed": ["legal validity",
"completeness of the encoded law",
"correctness of the corpus outside the pinned revision"]A verdict quoted without that list is a different claim than the one the tool made. The full catalogue of refusals — what each code means, and what a reader should do — is docs/11-REFUSAL-CODES.md.
| File | Role |
|---|---|
| docs/00-CHARTER.md | why this exists, what we refuse to build, and five falsifiers that could prove it wrong |
| docs/08-INTEROP.md | the channel between repositories: what a note may contain, what it may not, and why the exchange is part of the method rather than a courtesy |
| docs/10-SPEC-v0.1.md | the constitution: the document model, canonical form, Hohfeld layer, anchoring, time, conflicts, coverage, verdicts, conformance |
| docs/11-REFUSAL-CODES.md | closed vocabulary of ways a statement is wrong, with the remedy for each |
| docs/20-METHOD.md | how a paragraph of law becomes a checked statement, and what it costs in minutes |
| docs/02-DESIGN-SPACE.md | prior art: Catala, L4, LegalRuleML, Akoma Ntoso, deontic logic, proof assistants, LLM legal checking — what we borrow and what we refuse |
| docs/04-SEMANTIC-VS-FORMAL.md | when a machine-checked proof pays and when it is money wasted: CompCert, seL4, Cedar, TLA+, PBT, policy engines, and the PutnamBench incident where two formalised statements were wrong |
| docs/05-HARNESS-LESSONS.md | what a published 672/672 proof run teaches a checker: the harness owns the stopping rule, identity is checked on the elaborated form, cost is recorded per attempt — failures included |
| docs/06-FROM-TEXT-TO-PROOF.md | the research program: twenty numbered hypotheses on turning legal text into a proof obligation, each with the test that would kill it — and why the provable target is the checker, not the clause |
| docs/07-ROUND-01-QUESTIONS.md | sixteen questions we could not answer from inside, for external models and practitioners — anchoring, Hohfeld for civil law, whether the soundness theorem is trivial, measured encoding cost, evidence admissibility |
| docs/09-IMPLEMENTATION-LANGUAGE.md | the language choice on evidence: twelve requirements derived from the spec, four candidates, the seven byte-level traps, and the Lean 4 bridge — Rust primary, Python twin (ADR-0002) |
| docs/12-LANDSCAPE-REGISTER.md | four search passes merged: 53 distinct approaches, graded by our own re-check, with the defects found — including one fabricated repository and our own schema defect |
| docs/13-DEFEASIBILITY-CHOICE.md | the blocking sub-problem: carve-outs. Five requirements as tests, seven candidate mechanisms with where each stops, and the five scenarios that settle the choice |
| docs/14-ARCHITECTURE.md | the chain: law text → positions → quantities and flows → compiled rule → enforced decision → evidence walkable back to a span. Says what "reliably protected" can honestly mean, and what it cannot |
| docs/40-RUST-FIRST-SLICE.md | the Rust implementation begins: canonical form and SHA-256 with zero dependencies, agreeing with Python 12 of 12 byte-identically — and what it still cannot do |
| docs/39-MEMORY-AUDIT.md | memory audit: 1.6 MB worktree, no junk, the 466 KB chat digest never committed, and five documents that nothing linked to — now a guard rather than an audit |
| docs/38-STACK-AND-ARTEFACT.md | the stack advice from a chat, judged as experience rather than evidence — and the smallest reader-facing artefact built instead: one HTML file, no JavaScript, no CDN, with the verdict and the boundary on the same page |
| docs/37-CHAT-EXPORT.md | a two-year Telegram export studied and found to be an LLM research feed, not a legal source: the measurement error that first said otherwise (150 vs 43), and the three leads that do bear on us |
| docs/36-HYPOTHESIS-BENCH.md | the bench: hypotheses with falsifiers, predictions frozen with a file digest before the run, forecasts that expire — and the first pre-registered result, which came out refuted |
| docs/35-REPORTS-INVENTORY.md | ten usefulness reports read in full: the inventory with scores, and the finding that a project with 14 installs scored 94 while one with 2 500 users scored 76 — because the genre collapses problem evidence, costly commitment and adoption volume into one number |
| docs/34-USEFULNESS-REPORTS.md | the winners' reports read for what they reuse: a fixed questionnaire that forbids vanity metrics, the five questions verbatim, and what each winner offered as its one checkable data point |
| docs/33-PROOF-OF-USEFULNESS.md | the claim this repository has never made, measured against a public rubric: four dimensions of usefulness, what evidence each needs, which one we can prove (technical stability), and the rule that we publish no score of ourselves |
| docs/32-PORTFOLIO-INSIGHTS.md | what the other five repositories already solved: eight mechanisms with file and line, the three adopted here (citation liveness, a catalogue guard, exemptions that expire), and the four deliberately not taken |
| docs/31-LONGTAILS.md | what a Lean 4 framework with 132 verified optimisation bounds teaches a legal checker: the verifier must be able to say what the author did not, an escape needs a defence, and the one step their team also left to judgement is our interpretation gap |
| docs/30-REPO-WALK.md | the repository walk: what moved in the other five repositories, the defect flowguard's review found in our tool, and the three things we now owe |
| docs/29-PRINCIPLES-AND-DATA.md | principles, experiments and the dataset: one append-only row per encoding attempt, six testable regularities with their current (weak) evidence, and the rule that no generalisation is claimed before twenty provisions |
| docs/28-CLASSIFIER-LADDER.md | could a classifier help the surface layer? Three candidate tasks ranked by our measured bottleneck, the cheapest-first ladder, four entry gates, and the metric that decides — anchor hit@3 and minutes per closed atom, not accuracy |
| docs/27-QUANTITY-LAYER.md | the quantity layer specified: a rate series pinned by digest, a period cut at every rate change, and day-count/rounding as declared parameters with a verdict ceiling while they stay undeclared — with a table of what is settled by evidence and what is not |
| lab/legal-read-gk-395.md | the doctrinal read of ГК 395: the statute's six paragraphs against our atoms, which is how the four missing atoms and the collapsed п. 5 were found |
| docs/25-TRUTH-AND-BOUNDS.md | the claim registry: what is verified here and by which command, what is true only conditionally, what is explicitly not claimed, the negative results with how hard we looked, and the three tests that should break the document in ten minutes |
| docs/24-ROUND-03-QUESTIONS.md | six walls, one question each: day-count for statutory interest, whether Symboleo covers the Russian cases, what replaces an authority endorsement, a provision with published arithmetic, official access to Russian acts, and the convention for quote uniqueness |
| docs/23-METHOD-LOOP.md | the working loop: push → test → wall → round → merge, with the four properties that make something a wall rather than missing work, and the five lines every question must carry |
| docs/21-IMPACT-PLAN.md | the plan: seven stages ordered by what moves the portfolio edges and removes opinion, each with an artifact, an acceptance test, an estimate and a kill criterion — plus the one cheap experiment that could shrink the project's scope |
| docs/20-ROUND-02-MERGED.md | six answers merged: CAP-RRS already specifies the compile-with-provenance chain we thought was unbuilt, Symboleo already has the transition vocabulary, and ГК 395 has no authoritative oracle |
| docs/19-PORTFOLIO.md | the portfolio as one system: five repositories, the edges between them, which are built and which are not — and what "bridge between law and code" means as two conversions rather than a metaphor |
| docs/18-CLOSED-LOOP.md | the thesis made checkable: three objects — text, statement, code — and three pairwise checks; what "sharper" means in four numbers; the stopping rule that makes "ever sharper" falsifiable; and which pair is not checked yet |
| docs/17-ROUND-02-QUESTIONS.md | eight questions that attack the three decisions just made — computational-first, the transition layer, the certificate — asked for witnesses and artefacts rather than literature |
| docs/16-ROUND-01-ANSWERS.md | four answers to round 01, merged: the verified cost measurement from Catala, why the first corpus becomes computational provisions, and the six things that changed in the spec |
| docs/15-SUBSTRATE-INDEPENDENCE.md | the optional outward layer, as a resilience requirement: at least two substrates able to produce and record the same decision, a handover protocol with proof, the anchored legal basis a switch needs, degraded modes, and the drill that makes the fallback real |
| AGENTS.md | the twelve rules for anyone, human or agent, who changes this repository |
| schemas/statement-0.1.json | the schema, with the closed sets in one place |
| examples/ | twelve statements: one that passes, and the rest exercising refusal codes, carve-outs, quantities and defeat — python tools/lexspec_status.py prints the live count |
| Group | Path |
|---|---|
| Constitution | docs/10-SPEC-v0.1.md · docs/11-REFUSAL-CODES.md |
| Why and how | docs/00-CHARTER.md · docs/20-METHOD.md · docs/02-DESIGN-SPACE.md |
| Machine | schemas/ · tools/lexcheck.py · tools/lexspec_status.py |
| Evidence | examples/ · tests/ · corpus/ · tools/SELFTEST.md |
| Process | lab/sources.md — source intake register · lab/decisions/ — decisions; ADR-0001 explains why we are gathering sources before building |
| Interop | interop/ — the note channel with flowguard-spec; messages are append-only and pinned to commits |
| Guards | lab/check-secrets.py · .github/workflows/guards.yml |
- No legal validity. A verdict is about an encoding, never about law.
- No completeness. Coverage is a fraction of the statement; 100 % coverage of a mis-encoded clause is 100 % coverage of a mis-encoding.
- No statute parsing. Nothing here reads legal prose. The corpus is a pinned excerpt, and its header says so.
- No entailment. "The law requires X" is never an output. "Atom
a1is anchored at ——— in this revision" is. - No stability promise. v0.1 is a draft; codes and fields may change, and the report always names the spec version it was checked against.
| Project | Shared discipline | Different subject |
|---|---|---|
| flowguard-spec | declare a boundary, then prove things only inside it; refusal codes; claim registry | value flow through a database control point |
| VecDHT | canonical byte form is the contract between implementations | a peer-to-peer index |
| mak777uh/- | every number carries the command that produced it | a morphogenesis bench |
| cases | "not confirmed" is published as a result | verification case files |
The rule that transfers: an artifact a stranger cannot re-check is a claim, and claims are not results.
v0.1. The checker, schema, examples and tests exist and run; the numbers in this section are produced by
python tools/lexspec_status.py and the guard suite is in tools/SELFTEST.md with the commands and their
real output. What does not exist is listed in spec §11 — in short: no entailment, no
defeasibility, no cross-statement reasoning, no jurisdiction semantics, no signed certificate.
Documents — CC BY 4.0 (LICENSE). Code — Apache-2.0. Legal texts under corpus/ are official
documents of state bodies; under Art. 1259(6) of the Russian Civil Code they are not objects of copyright,
and each file states its source and revision in its own header.