About

ZTL — Zero-Trust Logic — and its tools are made by Vitaly Reznik.

Made with AI, checked without trusting it. The text, the code and the Lean proofs are written with Claude (Anthropic) in a dialogue that the author directs; the decisions and the responsibility are his. Nothing here should be believed because of who or what wrote it. A theorem is checked by the Lean kernel — which shows the proof is right for the statement as formalized, not that the statement says what the prose says; read the definitions. A number is recomputed by a public script. A verdict can be rerun with the open-source judge on your own machine — which shows the server applies no hidden rule, not that the rule is the right one for your problem.

How to check. On the ZTL pages each claim about the logic is marked as proved (with the Lean file), measured (with the script) or only stated. The tool pages describe what the tools do; their behaviour can be rerun from the code. If you find a claim on this site that cannot be checked, it is a fault of the page — please say so.

Licence. Text: CC BY 4.0. Code: ZTL and the studio under Apache-2.0 or MIT, at your choice; ZTL Engineer under Apache-2.0.