Why this can be trusted

The claim “the answer is computed, not invented” is worth exactly as much as the checks behind it. This page names them — and the bounds of what they prove.

Two implementations, one byte string

The language semantics are implemented twice, independently: lawref is the Python oracle, an executable specification; lawc is the Rust toolchain. On the same case both must emit a byte-identical canonical answer document — not “consistent”, not “equivalent in meaning”, identical byte for byte.

That is the load-bearing construction of correctness. One implementation can err unnoticed; two independent ones erring identically down to the byte is a far less probable event, and a divergence is visible at once.

A rule more important than the comparison itself then applies: divergence is a blocker with a qualification. First it is determined whose defect it is — lawc, lawref, or the specification itself — and only then is it fixed. Fitting one implementation to the other is forbidden; a specification case goes into the errata log, not into the code.

Vectors are written from the prose, not from the code

Behaviour is not treated as implemented until it has a conformance vector, and the vector is written from the specification text, not taken off a running implementation. Expectations are frozen: they cannot be rewritten under new behaviour — a change of behaviour is obliged to break vectors, not to retrain them.

The practical difference. A golden taken off an implementation proves that it does what it did yesterday. A vector written from the prose proves that it does what the specification says.

Third leg: machine-checked proofs

Proof graphs of answers are checked by an independent Lean kernel — on vectors and on live acts of the corpus. That is the third leg of the contour: two implementations are compared with each other, and the proofs with a formal model of inference that knows neither Python nor Rust.

Determinism is a property of the repository, not a promise

The same input yields the same output because sources of non-determinism are forbidden mechanically: access to system time, environment variables, unordered sets, and a random generator do not pass lints in either implementation. Each ban has a canary that must fail: a check that stopped catching a violation discovers itself.

So an answer obtained today is reproduced tomorrow — and a difference, if one appears, is explained by one of four hashes: the law changed (programHash), the case (caseHash), the result (resultHash), or the code (codeHash).

The statute text is pinned as bytes

A formalization does not refer to “article 26”. It refers to pinned bytes of official text with a hash. If the source text diverges from the text the norm was written against, no answer is issued: SOURCE_TEXT_HASH_MISMATCH arrives, and the computation does not run. Official text of any provision and its hash are returned by law_sources.

Coverage does not shrink in silence

The most expensive class of failure here is not an error but a quiet loss: a scenario dropped out of a run, a label vanished, an act stopped being checked — and everything stayed green because both the numerator and the denominator shrank. Against that stand ratchets: lower bounds on the number of scenarios, labels, and translations, movable only upward, and composition manifests that catch substitution of one scenario for another at an unchanged count.

What all of this does NOT prove

Honesty matters more than persuasion here.

It does not prove that the formalization correctly carries the meaning of the statute. Byte equality of two implementations says one thing: both compute the same way. Whether the norm was read correctly is a question for a human, and the system is built so that question can be asked: law_rules returns a deterministic verbalization of the rule next to the official article text, and the check “statute ↔ formalization” is done by eye. Uncovered constructs are named, not skipped in silence.

It does not prove completeness. The corpus is part of the law, an act in the corpus is part of the articles. How deeply a given act is taken apart is shown by the completeness measure: an article may be executable, merely anchored, or present as text alone. law_measure counts both measures at once, because one is not enough — “every article is covered” and “nothing is derived” coexist perfectly.

It does not prove applicability to your case. That the facts of the case are as stated, that this act applies, and that the question was asked correctly is legal qualification, and it remains with the lawyer. The system answers the question that was asked; it does not choose the question for the asker.

It does not replace a lawyer. Terms — Legal and licensing.

How to check it yourself

Question	What checks it
Is this the statute text	law_sources — official text and its hash
Is the norm read this way	law_rules — verbalization of the rule next to the article
How far is the act taken apart	law_measure — article accounting and depth of formalization
Why this answer	law_explain — the chain “rule ← premises → conclusion”
How robust is the conclusion	law_argue — did it stand against counter-arguments
Is this the same answer as yesterday	hashes from provenance — How to read an answer

None of these checks requires trusting the system on its word: each returns what the answer is built on — the statute text, the reading of the norm, the completeness measure, the chain of inference. The system is obliged to present its grounds, and it presents them through the same interface it answers with.