Decision receipts
Trust & Boundaries
What a receipt proves, and what it does not.
The evidence chain
How a decision becomes a receipt
A decision becomes a receipt in five steps. Each step leaves a fingerprint, and the receipt binds them all.
- 01
Source
A program written in the checked subset of Lispex.
- 02
Canonical Core
The source is rewritten into one canonical form, so the same meaning always looks the same.
- 03
Meaning Graph
The canonical form is read into a graph of what the program actually does.
- 04
Meaning Environment
The graph is evaluated under a deterministic rule profile, step by step, leaving a transcript.
- 05
Differential Receipt
sealedTwo execution paths compute the same result separately. The byte-level comparison of their outputs is sealed into the receipt.
The verdict
The verdict
Proves
1 claimA receipt proves that a given input, normalized into a canonical form, was evaluated under a specific public rule profile by a specific engine identity, and that the recorded result matches that evaluation, byte for byte.
Does not prove
6 boundaries- 01
The rightness, fairness, or legality of the policy itself.
- 02
The truth or provenance of the input.
- 03
The actual enforcement, timing, or attribution of the decision. Signatures and timestamps are a separate layer.
- 04
The correctness of target code emitted by an external engine.
- 05
Semantic equivalence across whole languages.
- 06
Fitness for regulatory or audit purposes.
Scope
Verification covers the checked subset of Lispex. Nothing outside that subset is claimed.
Same origin
The two execution paths share some foundations. This design catches divergence between paths. It is not an audit by an unrelated third party.
The product
Honest boundaries are the product.