The L'Var Institute for Coherence Dynamics
The L'Var Institute
for Coherence Dynamics
The Verification Record

Tri-verified.
Bitcoin-anchored.

Every formal proof produced by the Institute is mechanically verified across three independent theorem provers — Lean 4, Coq / Rocq, and Dedukti / λΠ-calculus modulo theory — and immutably timestamped into the Bitcoin ledger via OP_RETURN and OpenTimestamps. The record is auditable, public, and cryptographically irreversible.

// loading record…
§ The Triple Stack

Three provers. Independent kernels.
One canonical truth.

Lean 4

18,750 proofs

Modern dependent type theory with a small trusted kernel. Industry-leading mathlib integration. Proofs are checked by the Lean kernel itself; no metatheoretic shortcuts.

Coq / Rocq

18,600 proofs

Calculus of Inductive Constructions. Forty years of mature kernel scrutiny. Independent verification provides cross-checking against any single-prover bias.

Dedukti / λΠ

18,500 proofs

λΠ-calculus modulo theory. Logical-framework rewriting that exposes assumptions other provers leave implicit. The third independent witness.

§ Tri-Validation

A theorem earns Tri-Validated status only when all three kernels accept the proof. Any disagreement triggers a return to the Mathetica for revision. This isn't redundancy — it's distributed kernel scrutiny: we do not trust a result until three independent type theories agree it is sound.

Bitcoin OP_RETURN · OpenTimestamps

Immutable
publication.

Every verified proof is hashed (SHA-256), aggregated into a Merkle tree, and the root is committed to the Bitcoin blockchain — directly via OP_RETURN and via the OpenTimestamps calendar service. The result: a cryptographic proof-of-existence that no actor on Earth can alter or backdate, including us.

Direct OP_RETURN

For Tri-Validated theorems and major framework releases, we publish the SHA-256 root directly to a Bitcoin OP_RETURN output. The transaction itself is the publication. Once mined, the record is physics-locked into the longest chain.

OpenTimestamps

Every individual proof — even minor lemmas — receives an OpenTimestamps receipt. The calendar aggregates submissions across the network and anchors them in batched Bitcoin commits, giving each proof a portable, independently-verifiable timestamp with no fee burden per proof.

opentimestamps.org
The Verification Pipeline

From conjecture to chain — six stages.

01
Conjecture
A statement enters the Polyrheic Mathetica as a candidate. Definitions remain unsettled; the body is allowed to wander.
02
Formalisation
The candidate is encoded in Lean 4 with explicit dependencies on the LICD canonical library. Every assumption surfaces.
03
Cross-translation
The Lean term is translated to Coq/Rocq and to Dedukti/λΠ via verified bridges. Each prover receives a native, idiomatic encoding.
04
Three-kernel acceptance
All three kernels must independently accept the proof. Any rejection sends the result back to stage 02 for revision.
05
OpenTimestamps submission
The accepted proof artefact is hashed (SHA-256) and submitted to the OpenTimestamps calendar within minutes of acceptance.
06
Bitcoin OP_RETURN commit
Tri-Validated theorems and framework releases receive a direct OP_RETURN commit. The Merkle root enters the longest chain. The record is permanent.