What the receipt actually says.
Alelyon's verification layer exists to answer one question precisely: given a published number, what can a recipient establish on their own, and what are they still taking on faith? This page states both halves.
Certified arithmetic and storage error — not truth.
The guarantee lives at a specific layer, and naming that layer is the whole discipline. Alelyon certifies the quantisation errorintroduced by storing a value, and the replay of the program that consumed it. Those are real, checkable properties. They are not a claim that the underlying data is correct.
- 01
Capture
Every element dither-quantised on arrival, with its per-column step recorded beside it.
- 02
Store
Append-only. A restatement becomes a new vintage; the old one is still answerable.
- 03
Compute
A restricted DSL program runs on a deterministic kernel. No model emits a figure.
- 04
Seal
A signed envelope binds program, scalar, per-input commitments and the error budget.
- 05
Replay
You re-run it against your own copy of the inputs, under a key you pinned out of band.
Certified at write
Every element is dither-quantised on arrival with a per-column step recorded alongside it. Certification happens at capture, not as a later pass over rows that were already stored — so there is no window in which an uncertified element looks certified.
Revisions kept, never overwritten
The store is append-only. A restated figure becomes a new vintage beside the old one, and point-in-time reads resolve to what was actually known on the date in question. Future knowledge cannot leak backwards into a historical decision path.
Tamper-evident and anchored
A per-scope hash chain covers the ledger, and the ledger is anchored in an RFC-6962 Merkle transparency log with both inclusion and consistency proofs under an ed25519-signed tree head. Per-input steps are committed in the signed leaves, which is what defeats an invented step — including one declared as exactly zero.
A signed envelope
The result ships as an envelope binding the program, the scalar, the per-input commitments (digest, step, seed), the kernel identity, and the decomposed error budget. A refusal is signed too — it is an outcome, not an absence.
Every term labelled by how it was obtained.
A single number called "the error" hides which part of it is a theorem and which part is a guess. Alelyon publishes the decomposition instead, with each term carrying its own provenance, and names the dominant term rather than letting it disappear into a sum.
- QuantisationTheorem, or first-order for smooth programsMeasured
- SamplingCircular block bootstrap over recognised stationary statisticsMeasured · typically binds
- ProviderCarries a named status, never a valueNamed, not measured
- ModelNo model in the path — the DSL program is the whole computationNot applicable, with reason
Composed, never summed. The terms combine as a root-sum-square of independent contributions and the result is labelled a composition. There is no single figure called "the certified error", because that number would hide which part of it is a theorem and which part is an estimate.
At 24-bit capture, sampling typically binds the result by roughly four orders of magnitude over quantisation. The envelope names which term binds rather than leaving a reader to assume the composite is dominated by the part that sounds most rigorous.
Designed for third-party verification.
The component that checks a certificate is public. The component that computes one is operated by Alelyon. That separation is deliberate: a recipient can run the public replay checks without the private issuer implementation. Those checks still require independently obtained inputs and a public key pinned out of band, and a substrate-sensitive nonzero width may remain explicitly unverified.
The open surface ships as alelyon-os on PyPI. The verifier is the alelyon.verify module inside it, together with thealelyon-verify command it installs, the normative spec, and the conformance vectors — so the format is checkable against a written specification rather than against our implementation's behaviour.
It replays the program against inputs you supply yourself, and a pinned public key obtained out of band is mandatory for a positive verdict — a certificate that carries its own key verifies nothing. Where the numeric substrate differs from the issuer's, the verifier degrades honestly: the scalar is verified to tolerance and the width is left explicitly unverified with a stated reason, rather than being quietly accepted.
Where the boundaries are.
- Determinism
Bit-identical reductions
A Rust substrate produces identical reductions across runs, threads, and machines, with a tested NumPy fallback. A certificate never depends on the native extension being installed — the fallback path is a first-class citizen, not a degraded mode that silently changes results.
- Language
The model writes a program, not an answer
Where a language model is involved, it authors a restricted DSL program and nothing else. A deterministic interpreter computes the result. There is no
eval, no shell, no arbitrary import, no dynamic attribute access, and no filesystem or network reach inside that language. - Refusal
Refusing is a result
When a program falls outside the tier scheme — linear-exact, smooth-first-order, branch-margin-guarded — it is hard-refused rather than approximated. Margin guards are evaluated per element, because one benign element pinning an aggregate margin would defeat the safety factor entirely.
- Corroboration
Asked, answered, or silent
The attempt ledger records what was asked of each source and whether it answered or stayed silent, under a closed outcome vocabulary. Deleting or rewriting a silence is detectable by re-derivation. With a single answering origin this anchors the record of having asked — it is not a cross-source agreement claim.
Selected public research notes.
This website collection includes selected findings, including results that failed. Each entry states what it establishes and, immediately beside it, what it does not. It is not a complete inventory of Alelyon research or public papers.
Verification
A certificate cannot authenticate a quantisation step by repeating its own claim
A certificate that reports its own quantisation step can simply declare it to be zero. Signed transparency leaves make later revision detectable when a verifier retains or independently obtains the required leaves and checkpoints.
Does not establishThe current log, witness, and signing key are issuer-operated. Anchoring does not prove correct capture or prevent an undetected issuer fork when nobody outside the issuer retains the comparison evidence.
A twelve-domain expansion went to referees and came back overclaimed
Two independent referee passes — one on prior art, one taking the buyer's position — rejected the case for applying certified numbers across twelve domains. Two survived; ten did not.
Does not establishThis records the verdict on the expansion, not a finding about the underlying method. The surviving domains remain gated behind platform prerequisites.
The receipt detects revision, not invention
The strongest honest statement about a signed certificate is that committed inputs have not changed since they were committed. A producer who fabricates at capture signs a receipt that verifies perfectly.
Does not establishNothing here establishes that the underlying data is correct. Verification also requires inputs you obtained independently and a public key you pinned out of band.
Numerics
The execution bound covers storage quantisation, and nothing wider
A conformal execution bound over dither-quantised inputs, with a tier scheme that hard-refuses programs it cannot place, and per-element margin guards.
Does not establishIt is a probabilistic order statistic over storage quantisation alone — not a guaranteed enclosure, and not coverage of rounding, truncation, or discretisation error.
Machine learning
A restricted CNE program keeps the model from supplying the computed figure
On the restricted CNE path, the model authors a program and an interpreter computes the result. The accepted DSL output therefore does not take its computed figure from model recall.
Does not establishThis applies only to the restricted CNE/DSL result. Lattice narration and open mode can contain model-origin estimates, and the constraint does not establish that the chosen program, inputs, or conclusion were correct.
Data engineering
Economic data is revised, so a backtest that reads today's series is reading the future
Macroeconomic series are restated for months after first release. Reading the current series when reconstructing a past decision silently imports knowledge that did not exist, and the resulting backtest is measuring hindsight.
Does not establishVintage discipline removes one specific look-ahead channel. It does not make a backtest realistic on execution, liquidity, or transaction costs.
Prior art, stated plainly.
The attestation layer is a competent re-derivation in the SCITT, Sigstore/Rekor, Sigsum, and RFC-6962 family — not new cryptographic theory, and Alelyon does not present it as such. Vendor dispersion as uncertainty is Markit Totem and EBA prudent-valuation territory; over-dispersion is the Birge ratio; error variance without ground truth is triple collocation. The contribution is systems and product: putting these together in one pipeline, at capture, with a public checker.
Replay the applicable checks.
The open verifier replays scalar and other applicable checks against inputs you supply, under a public key obtained and pinned out of band. A substrate-sensitive nonzero width may remain explicitly unverified.
$ pip install alelyon-os
$ alelyon-verify selftest
conformance suite: bundled, offline
$ alelyon-verify verify \
--envelope receipt.json \
--data your_own_extract.json \
--key <pinned out of band>