ZTL Judge¶
A logic for checks on data you do not own, and a judge that says what a claim needs.
A program often decides on a value it does not hold: a field from another system, a flag another process may set, a file that may be replaced. Its owner can change it between two reads; in security this is the time-of-check to time-of-use problem. Zero-Trust Logic (ZTL) is a logic for such checks. Each check grants only what its own inputs force; the judge then reports, for a whole claim, which grants hold up.
The rule¶
An atom is T (true), F (false) or Z — dirty: not ours, it may change between two reads. Each occurrence of a dirty atom is read on its own. That is a modelling choice, and it is yours to make: if your program reads a value once into a variable, write that value once. Which atoms are dirty is also your input.
One rule generates every connective:
A connective is false whenever some reading of its arguments makes the classical connective false, and true otherwise.
An argument that is a dirty atom can be read as 1 or 0; an argument that is itself a compound is read as the verdict it already recorded. So every compound is T or F, and Z occurs only on atoms: the atoms have three values, the connectives answer with two. Negation: ¬T = F, ¬F = T, ¬Z = F. Three binary connectives (rows: the left argument):
| ∧ | T | F | Z |
|---|---|---|---|
| T | T | F | F |
| F | F | F | F |
| Z | F | F | F |
| ∨ | T | F | Z |
|---|---|---|---|
| T | T | T | T |
| F | T | F | F |
| Z | T | F | F |
| → | T | F | Z |
|---|---|---|---|
| T | T | F | F |
| F | T | T | T |
| Z | T | F | F |
A T says: every reading of what this check reads makes it true. An F says: not established — not that the data are false. Because a check reads the recorded verdict of a compound, ¬¬p on a dirty p is T: the inner check records F (p might be true), and the outer check negates that record. Whether such a T survives verification is the judge's question.
The judge¶
A cleaning verifies every dirty value, to T or to F. For one claim the judge reports three readings at once:
- per occurrence — is the claim true under every reading of every occurrence? (strong Kleene logic's answer)
- per cleaning — is it true after every cleaning?
- as written — the value of the claim in the tables above.
They combine into one disposition:
- EARNED / REFUTED — reading 1 is true / false: settled whatever the dirty values are.
- EARNED IF STABLE / REFUTED IF STABLE — reading 1 is undecided, but reading 2 is true / false: settled once the dirty values are verified, either way. The judge names the values that must stay the same until then.
- ON CREDIT / OPEN — readings 1 and 2 are undecided, and the claim as written is T / not T. ON CREDIT is true now, and some verification would refute it.
| claim, every atom dirty | as written | the judge says | why |
|---|---|---|---|
| p ∨ ¬p | F | EARNED IF STABLE | true after every cleaning; two reads of p may differ |
| p → p | F | EARNED IF STABLE | the same |
| ¬¬p | T | ON CREDIT | true now; verifying p as false refutes it |
| p | Z | OPEN | not established |
The value as written and the disposition can differ, and they answer different questions: p → p as written is F, because a check that reads p twice cannot rely on getting the same value; after verification it is true.
Check it yourself¶
In the browser: the ZTL studio. Through the public API:
curl -s -X POST https://api.ztljudge.com/judge \
-H 'Content-Type: application/json' \
-d '{"claim": "p -> p", "rows": [{"name": "p", "means": "it rains", "status": "unverified"}]}'
The answer's disposition is EARNED IF STABLE, with its meaning and the names to check. Both run on our server; to
run the judge on your own machine, clone the repository and, from its root:
python3 -c "import ztljudge; print(ztljudge.judge('p -> p', {'p': 'Z'})['disposition'])"
What is proved, and what is measured¶
- Proved. The judge's dispositions, their properties and the translation to Bochvar's logic are theorems checked by
the Lean 4 kernel with an empty axiom list — no excluded middle, no choice — in
lean/ZSpeaks.lean,lean/ZDirty.leanandlean/ZBochvar.lean. The kernel checks the statements as formalized; whether the short definitions there match the prose here is for you to judge. The program is tested against them, not proved. - Measured. Counts are computed, not proved, by public scripts
(
publications/core-logic/paper_numbers.py). - Published. The preprint, with every result and its proof: ZTL — Zero-Trust Logic, v2.1.6 (Zenodo, 2026). It is a preprint, not peer-reviewed.
Where it stands¶
- Nothing new in what it computes. ZTL computes the same two-valued functions as Bochvar's external formulas (1938),
in another basis — proved both ways in
ZBochvar.lean. For classical logic a change of basis is cosmetic; for ZTL it is not, because each connective is one check and its table says what one check may grant. - Two of the judge's readings are known. Readings 1 and 2 are the compositional and the thorough semantics of three-valued model checking (Bruns and Godefroid, 1999; 2000). Reading 3 is ZTL's.
- One measured difference. Our regression pool holds every formula of depth at most two over two atoms, at every valuation with a dirty atom. Over the true verdicts of its compound formulas, ZTL and Bochvar's external connectives (in both conventions in use) give the same 2 448 verdicts that every reading forces, and ZTL gives 3 738 that no reading forces, against 5 090 and 5 358 for Bochvar's. An unforced T is a grant that no reading of the data supports; ZTL gives fewer, though not none and not in every cell. Per connective this holds by construction; on compound formulas it does not follow from the definitions, so it is measured.
Written with Claude (Anthropic). The author, Vitaly Reznik, directs the work and is responsible for it.