LeaTTa 1.0.6

LeaTTa 1.0.6

LeaTTa 1.0.6 adds the next checked piece of the generated-hypercube layer. Modal sites, spatial heads,
slot families, rule schemes, and judgment footprints were already represented in Lean. This release
adds explicit slot constraints and connects them to the finite equational-center checker.

Announcement

LeaTTa 1.0.6 moves the generated-hypercube work one step closer to the center construction described
by Stay, Meredith, and Wells.

MeTTaIL.Semantics.Hypercube now defines SlotConstraint, the explicit equality that says two
generated slots must receive the same sort. The file also adds nullary slot expressions, so those
equalities can be seen by the generic equation checker already used for the hypercube center.

The new constrainedCenter and Presentation.hypercubeConstrainedCenter functions compute the center
under a list of explicit slot constraints. The theorem mem_constrainedCenter_iff states the exact
meaning of that computation: a member is a raw slot assignment that satisfies every listed slot
equality. The bridge theorems are included in the axiom audit and in the Verso theorem register.

The checked claim is precise. The release checks explicit slot constraints. It does not yet
derive every constraint automatically from source equations and rewrite laws, and it does not yet turn
the recorded judgment footprints into the full generated typing system. Those are the next hypercube
obligations.

Highlights

• The minimal MeTTa interpreter and standard library still pass Hyperon's vendored oracle corpus:
  270 assertions across 22 files.
• LeaTTa --mettail FILE --term TERM [--fuel N] still runs a term through a small editable MeTTaIL
  dialect file.
• Cordial Miners remains hosted as a MeTTaIL runtime presentation with AC-aware state and inbox
  rewriting.
• MeTTaIL.Semantics.Hypercube now has checked explicit slot constraints, the constrained center, and
  the membership theorem connecting that center to direct constraint satisfaction.
• The denotational files still provide checked interfaces and small kernels for the rset, rho/RSpace,
  and knotted-universe route. They do not claim the knotted topos or full rho operational
  correspondence.
• The release bundles include examples/bool.mettail, so the MeTTaIL runtime path can be tested
  without a Lean toolchain.

Quick Checks

From a release bundle:

bin/LeaTTa --min '!(+ 1 (* 2 (- 10 4)))'
bin/LeaTTa --mettail examples/bool.mettail --term '(notOp tt)'
bin/LeaTTa --oracle examples/a1_symbols.metta

Expected outputs:

[13]
ff
==== PASS=7  FAIL=0  TOTAL=7 ====

From a source checkout:

lake build
lake build MeTTaIL MeTTaILProofs MeTTaILTests
lake build CordialMiners CordialMiners.Runtime.Run
./scripts/run-oracle.sh
./scripts/run-regression.sh
cd book && lake exe docs

Scope

The --mettail file format covers sort, term, and base rewrite declarations over S-expression
terms. The format is the CLI path into the checked runtime, not the full BNFC MeTTaIL surface parser.
The AC matcher used by the Cordial Miners runtime bridge covers the linear collection fragment needed
by those rules: one fixed payload and one rest variable.

The hypercube layer now checks explicit slot constraints through the finite center machinery. The
automatic derivation of those constraints from source equations and rewrite laws remains open, as does
the full generated typing theorem for binder calculi.

The rho and denotational additions say what the future model has to prove and check the pieces already
in reach. The release does not claim the knotted topos, the full MeTTaIL-to-rho desugaring theorem, the
trie store, the cut distributive law, the cost endofunctor, or a language-specific
observational-calibration theorem.

v1.0.5

LeaTTa 1.0.5

LeaTTa 1.0.5 extends the red/black denotational track with a checked category of reflective
universes. The runnable MeTTaIL runtime and Cordial Miners bridge remain in scope, while the knotted
topos, the full MeTTaIL-to-rho operational correspondence, and language-specific observational
calibration remain open work.

Announcement

LeaTTa 1.0.5 adds the next checked categorical surface for the MeTTaIL denotational line.

MeTTaIL.Semantics.KnottedUniverse now defines ReflectiveUniverseHom, the structure-preserving maps
between red/black reflective universes. A morphism carries red sets, red atoms, black sets, and black
atoms forward, and it must commute with quote, drop, and the colour-swap equivalences.

The file also packages reflective universes as a Mathlib category. ReflectiveUniverse.category
supplies identity morphisms, composition, and the category laws for those structure-preserving maps.
The new names are included in the axiom audit.

The root README and the Verso book now describe the reflective-universe category directly. The docs
still draw the line where the Lean code currently draws it: the project has checked interfaces and
kernels for the denotational route, but it does not yet construct the knotted topos, prove finality for
the real rho behaviour functor, or prove the full MeTTaIL-to-rho desugaring theorem.

The next step is still to carry the MeTTaIL and Cordial Miners bridge deeper while turning the rho,
RSpace, and knotted-universe interfaces into concrete correspondence and finality proofs.

Highlights

• The minimal MeTTa interpreter and standard library still pass Hyperon's vendored oracle corpus:
  270 assertions across 22 files.
• LeaTTa --mettail FILE --term TERM [--fuel N] still runs a term through a small editable MeTTaIL
  dialect file.
• Cordial Miners remains hosted as a MeTTaIL runtime presentation with AC-aware state and inbox
  rewriting.
• MeTTaIL.Semantics.RSet adds finite red/black rsets, atom opacity, finite support, colour-swap
  equivalences, and extensional union laws.
• MeTTaIL.Semantics.KnottedUniverse now has a category of reflective universes, a category of
  coalgebras, and the calibration bridge from final behaviour to full abstraction.
• The release bundles include examples/bool.mettail, so the MeTTaIL runtime path can be tested
  without a Lean toolchain.

Quick Checks

From a release bundle:

bin/LeaTTa --min '!(+ 1 (* 2 (- 10 4)))'
bin/LeaTTa --mettail examples/bool.mettail --term '(notOp tt)'
bin/LeaTTa --oracle examples/a1_symbols.metta

Expected outputs:

[13]
ff
==== PASS=7  FAIL=0  TOTAL=7 ====

From a source checkout:

lake build
lake build MeTTaIL MeTTaILProofs MeTTaILTests
lake build CordialMiners CordialMiners.Runtime.Run
./scripts/run-oracle.sh
./scripts/run-regression.sh
cd book && lake exe docs

Scope

The --mettail file format covers sort, term, and base rewrite declarations over S-expression
terms. The format is the CLI path into the checked runtime, not the full BNFC MeTTaIL surface parser.
The AC matcher used by the Cordial Miners runtime bridge covers the linear collection fragment needed
by those rules: one fixed payload and one rest variable.

The rho and denotational additions say what the future model has to prove and check the pieces already
in reach. The release does not claim the knotted topos, the full MeTTaIL-to-rho desugaring theorem, the
trie store, the cut distributive law, the cost endofunctor, or a language-specific
observational-calibration theorem.

v1.0.4

LeaTTa 1.0.4

LeaTTa 1.0.4 is a focused metatheory release. It builds on the 1.0 runtime line by making the
red/black denotational track more explicit in Lean. The runnable MeTTaIL runtime and Cordial Miners
bridge remain in scope, while the knotted topos, the full MeTTaIL-to-rho operational correspondence,
and language-specific observational calibration remain open work.

Announcement

LeaTTa 1.0.4 adds five checked pieces to the MeTTaIL denotational line.

The rset paper now has a finite Lean core. MeTTaIL.Semantics.RSet defines finite red and black sets,
atoms as sealed opposite-colour sets, finite support for atom renaming, colour-swap equivalences, and
an exact-member extensional quotient with finite union laws. Those union laws prove that empty is
neutral and that union is idempotent, commutative, and associative at the extensional level.

The rset core is tied back to the generic red/black interface. The reflective_* theorems identify
the ReflectiveUniverse quote/drop and colour-swap fields with the concrete rset functions. This keeps
the rset work connected to the knotted-universe surface instead of living as a separate model.

The coalgebra side now uses standard category-theory language. CoalgebraHom gives the morphisms
between coalgebras for a TypeEndofunctor, Coalgebra.category packages them as a Mathlib category,
and FinalCoalgebra.isTerminal states that a final coalgebra is a terminal object in that category.

The final-behaviour model now exposes the last calibration step directly.
FinalBehaviourModel.fullyAbstractFor calibrates final-behaviour equality against a chosen
object-language equivalence, and FinalBehaviourModel.fullyAbstractForObservations does the same for
an observation family. These theorems are axiom-free.

The README and Verso book now state the current scope more directly. The project has checked interfaces
and kernels for the denotational route. It does not yet construct the knotted topos, prove finality for
the real rho behaviour functor, or prove the full MeTTaIL-to-rho desugaring theorem.

The next step is still to carry the MeTTaIL and Cordial Miners bridge deeper while turning the rho and
knotted-universe interfaces into concrete correspondence and finality proofs.

Highlights

• The minimal MeTTa interpreter and standard library still pass Hyperon's vendored oracle corpus:
  270 assertions across 22 files.
• LeaTTa --mettail FILE --term TERM [--fuel N] still runs a term through a small editable MeTTaIL
  dialect file.
• Cordial Miners remains hosted as a MeTTaIL runtime presentation with AC-aware state and inbox
  rewriting.
• MeTTaIL.Semantics.RSet adds finite red/black rsets, atom opacity, finite support, colour-swap
  equivalences, and extensional union laws.
• MeTTaIL.Semantics.KnottedUniverse now states final coalgebras as terminal objects in the category
  of coalgebras and links final-behaviour models to observational calibration.
• The release bundles include examples/bool.mettail, so the MeTTaIL runtime path can be tested
  without a Lean toolchain.

Quick Checks

From a release bundle:

bin/LeaTTa --min '!(+ 1 (* 2 (- 10 4)))'
bin/LeaTTa --mettail examples/bool.mettail --term '(notOp tt)'
bin/LeaTTa --oracle examples/a1_symbols.metta

Expected outputs:

[13]
ff
==== PASS=7  FAIL=0  TOTAL=7 ====

From a source checkout:

lake build
lake build MeTTaIL MeTTaILProofs MeTTaILTests
lake build CordialMiners CordialMiners.Runtime.Run
./scripts/run-oracle.sh
./scripts/run-regression.sh
cd book && lake exe docs

Scope

The --mettail file format covers sort, term, and base rewrite declarations over S-expression
terms. The format is the CLI path into the checked runtime, not the full BNFC MeTTaIL surface parser.
The AC matcher used by the Cordial Miners runtime bridge covers the linear collection fragment needed
by those rules: one fixed payload and one rest variable.

The rho and denotational additions say what the future model has to prove and check the pieces already
in reach. The release does not claim the knotted topos, the full MeTTaIL-to-rho desugaring theorem, the
trie store, the cut distributive law, the cost endofunctor, or a language-specific
observational-calibration theorem.

v1.0.3

LeaTTa 1.0.3

LeaTTa 1.0.3 extends the checked MeTTaIL runtime and denotational track. It keeps the
1.0 release scope honest: the runnable runtime is real, the Cordial Miners bridge is in
the checked runtime path, and the knotted-topoi work is represented by checked interfaces
and small kernels, not by a claimed finished topos construction.

Announcement

LeaTTa 1.0.3 adds three pieces to the MeTTaIL line.

The rho bridge now has a clearer K-machine staging path. The release includes candidate-ID
gating, ordinary and persistent K steps, K cell creation, named match-readiness helpers, and
a packet-level theorem that ties a successful MeTTaIL base rewrite to a ready K communication
step and the corresponding rho listener emission.

The denotational side now has the first checked red/black and store-facing surfaces. The
new MeTTaIL.Semantics.KnottedUniverse module records the four visible red/black sorts,
quote/drop round trips, a generic final-coalgebra interface, and the bridge from final
behaviour models to the existing FullyAbstractModel. The new
MeTTaIL.Semantics.InteractingTrieMap module records the reflective RITM equation from
the ITM sketch and connects Jetta-style packed binding addresses to the path-key RSpace
prefix relation.

The full-abstraction interface now names the last calibration step explicitly.
BisimilarityCalibration states when the chosen context-labelled bisimilarity agrees with an
object language's observational equivalence, and
fullyAbstract_of_observation_calibration turns the internal theorem into the user-facing
observational theorem.

The next step is still bridging MeTTaIL and Cordial Miners more deeply, while carrying the rho
and knotted-universe work from interfaces into concrete operational correspondence and finality
proofs.

Highlights

• The minimal MeTTa interpreter and standard library still pass Hyperon's vendored oracle corpus:
  270 assertions across 22 files.
• LeaTTa --mettail FILE --term TERM [--fuel N] still runs a term through a small editable
  MeTTaIL dialect file.
• Cordial Miners remains hosted as a MeTTaIL runtime presentation with AC-aware state and inbox
  rewriting.
• The release bundles include examples/bool.mettail, so the MeTTaIL runtime path can be tested
  without a Lean toolchain.
• The book and README now describe the rho K bridge, the knotted-universe interface, the ITM and
  Jetta store sources, and the observational-calibration theorem.
• The GitHub Pages workflow builds the Verso book and API docs for the kernel, metatheory,
  operational semantics, MeTTaIL, MeTTaILProofs, and CordialMiners targets.

Quick Checks

From a release bundle:

bin/LeaTTa --min '!(+ 1 (* 2 (- 10 4)))'
bin/LeaTTa --mettail examples/bool.mettail --term '(notOp tt)'
bin/LeaTTa --oracle examples/a1_symbols.metta

Expected outputs:

[13]
ff
==== PASS=7  FAIL=0  TOTAL=7 ====

From a source checkout:

lake build
lake build MeTTaIL MeTTaILProofs MeTTaILTests
lake build CordialMiners CordialMiners.Runtime.Run
./scripts/run-oracle.sh
./scripts/run-regression.sh
cd book && lake exe docs

Scope

The --mettail file format covers sort, term, and base rewrite declarations over
S-expression terms. The format is the CLI path into the checked runtime, not the full BNFC
MeTTaIL surface parser. The AC matcher used by the Cordial Miners runtime bridge covers the
linear collection fragment needed by those rules: one fixed payload and one rest variable.

The rho and denotational additions say what the future model has to prove and check the small
pieces already in reach. The release does not claim the knotted topos, the full MeTTaIL-to-rho
desugaring theorem, the trie store, the cut distributive law, the cost endofunctor, or a
language-specific observational-calibration theorem.

LeaTTa 1.0.2

LeaTTa 1.0.2

LeaTTa 1.0.2 is a follow-up release for the checked MeTTaIL runtime line. The release adds a
source-backed denotational-semantics interface, rewrites the release-facing README, and keeps the
Cordial Miners runtime bridge in the public release path.

Announcement

LeaTTa 1.0.2 tightens the 1.0 line around exact claims and testable entry points. The root README now
opens with the main validation commands and expected results, then explains the MeTTaIL runtime,
Cordial Miners bridge, and current open surface without alpha or work-in-progress framing.

The MeTTaIL layer now includes MeTTaIL.Semantics.Denotational, a checked interface for labelled
transition systems, simulations, bisimulations, denotational kernels, context congruence, and the
FullyAbstract property. The book connects that interface to the rset, rho-calculus, and knotted-topoi
manuscripts. The release does not claim the knotted topos, the MeTTaIL-to-rho desugaring, or the final
coalgebra construction as completed Lean proofs.

The next step is deepening the bridge between MeTTaIL and Cordial Miners.

Highlights

• The minimal MeTTa interpreter and standard library still pass Hyperon's vendored oracle corpus:
  270 assertions across 22 files.
• LeaTTa --mettail FILE --term TERM [--fuel N] still runs a term through a small editable MeTTaIL
  dialect file.
• The release bundles include examples/bool.mettail, so the MeTTaIL runtime path can be tested
  without a Lean toolchain.
• Cordial Miners remains hosted as a MeTTaIL runtime presentation with AC-aware state and inbox
  rewriting.
• The book cites the rset, rho, and knotted-topoi papers and states which denotational claims are
  interfaces versus completed proofs.
• The GitHub Pages workflow builds the Verso book and API docs for the kernel, metatheory, operational
  semantics, MeTTaIL, MeTTaILProofs, and CordialMiners targets.

Quick Checks

From a release bundle:

bin/LeaTTa --min '!(+ 1 (* 2 (- 10 4)))'
bin/LeaTTa --mettail examples/bool.mettail --term '(notOp tt)'
bin/LeaTTa --oracle examples/a1_symbols.metta

Expected outputs:

[13]
ff
==== PASS=7  FAIL=0  TOTAL=7 ====

From a source checkout:

lake build
lake build MeTTaIL MeTTaILProofs MeTTaILTests
lake build CordialMiners CordialMiners.Runtime.Run
./scripts/run-oracle.sh
./scripts/run-regression.sh
cd book && lake exe docs

Scope

The --mettail file format is intentionally small: sort, term, and base rewrite declarations
over S-expression terms. The format is the release-facing path into the checked runtime, not the full BNFC
MeTTaIL surface parser. The AC matcher used by the Cordial Miners runtime bridge covers the linear
collection fragment needed by those rules: one fixed payload and one rest variable.

The denotational-semantics addition is an interface and theorem scaffold. The interface states the Lean
shape of full abstraction for a context-labelled system. The interface does not construct the knotted
topos or prove the rho desugaring functor.

LeaTTa 1.0.1

LeaTTa 1.0.1

LeaTTa 1.0.1 adds the checked MeTTaIL runtime path and the Cordial Miners runtime bridge to the public
release line.

Announcement

This release adds the verified MeTTaIL runtime path. An editable language definition in the checked
LeaTTa MeTTaIL runtime format can be parsed, monomorphized, and run through the verified reducer. Each
executable step is tied back to the presentation semantics.

It also adds the PoR-weighted Cordial Miners formalization and runtime bridge. The coarse protocol is
encoded as real MeTTaIL.AST, run as a MeTTaIL presentation with AC-aware state and inbox rewriting,
and connected to the protocol model through simulation and stuttering-refinement theorems.

The next step will be deepening the bridge between MeTTaIL and Cordial Miners.

Highlights

• The minimal MeTTa interpreter and standard library still pass Hyperon's vendored oracle corpus:
  270 assertions across 22 files.
• LeaTTa --mettail FILE --term TERM [--fuel N] runs a term through a small editable MeTTaIL dialect
  file.
• The release bundles include examples/bool.mettail, so the MeTTaIL runtime path can be tested
  without a Lean toolchain.
• Cordial Miners now has runtime demos for buried proposal events, ordered-prefix events, and finality.
• The book covers the MeTTa kernel, gradual type system, operational semantics, MeTTaIL runtime path,
  Cordial Miners safety core, proof status, and current limits.
• The GitHub Pages workflow builds the Verso book and API docs for the kernel, metatheory, operational
  semantics, MeTTaIL, MeTTaILProofs, and CordialMiners targets.

Quick Checks

From a release bundle:

bin/LeaTTa --min '!(+ 1 (* 2 (- 10 4)))'
bin/LeaTTa --mettail examples/bool.mettail --term '(notOp tt)'
bin/LeaTTa --oracle examples/a1_symbols.metta

Expected outputs:

[13]
ff
==== PASS=7  FAIL=0  TOTAL=7 ====

From a source checkout:

lake build
lake build CordialMiners
./scripts/run-oracle.sh
./scripts/run-regression.sh
cd book && lake exe docs

Scope

The --mettail file format is intentionally small: sort, term, and base rewrite declarations
over S-expression terms. It is the release-facing path into the checked runtime, not the full BNFC
MeTTaIL surface parser. The AC matcher used by the Cordial Miners runtime bridge covers the linear
collection fragment needed by those rules: one fixed payload and one rest variable.

v1.0.0

LeaTTa 1.0.0

LeaTTa 1.0.0 is the first release that ships the MeTTaIL spec-to-runtime path in the LeaTTa
executable.

Announcement

As quoted by Zarathustra Goertzel, "One of the MeTTa-IL style dreams is to be able to tweak the
LanguageDef specs for a MeTTa dialect and get a runtime for it." This is the realisation of it :))

The next step will be bridging MeTTaIL and Cordial Miners.

Highlights

• The minimal MeTTa interpreter and standard library still pass Hyperon's vendored oracle corpus:
  270 assertions across 22 files.
• LeaTTa --mettail FILE --term TERM [--fuel N] runs a term through a small editable MeTTaIL
  dialect file.
• The release bundles include examples/bool.mettail, so the MeTTaIL runtime path can be tested
  without a Lean toolchain.
• The book covers the MeTTa kernel, gradual type system, operational semantics, MeTTaIL runtime path,
  Cordial Miners safety core, proof status, and current limits.
• The GitHub Pages workflow now builds API docs for the MeTTaIL and Cordial Miners libraries as well
  as the original kernel, metatheory, and operational-semantics targets.

Quick Checks

From a release bundle:

bin/LeaTTa --min '!(+ 1 (* 2 (- 10 4)))'
bin/LeaTTa --mettail examples/bool.mettail --term '(notOp tt)'
bin/LeaTTa --oracle examples/a1_symbols.metta

Expected outputs:

[13]
ff
==== PASS=7  FAIL=0  TOTAL=7 ====

From a source checkout:

lake build
./scripts/run-oracle.sh
./scripts/run-regression.sh
cd book && lake exe docs

Scope

The --mettail file format is intentionally small: sort, term, and base rewrite declarations
over S-expression terms. It is the release-facing path into the checked runtime, not the full BNFC
MeTTaIL surface parser.

LeaTTa 0.5.0

LeaTTa 0.5.0: I machine-checked the safety of Cordial Miners

I formalized PoR-weighted Cordial Miners, a leaderless DAG-based consensus protocol, in Lean 4 and proved it safe. It is the next LeaTTa iteration, after MeTTaIL.

Run it:

#eval simulate demo
-- [1, 2, 3]

I hand it a committee, some blocks, and the approvals each block got. It folds the approvals through the weighted certificate collector, keeps the finalized blocks, and orders them with a verified topological sort. The ordering is a proved pure function, so every honest node computes the same list.

The safety I care about: two honest nodes never publish conflicting orders. It is a theorem, and here is everything it leans on:

#print axioms cm_end_to_end_safety_permanent
-- propext, Classical.choice, Quot.sound

The three standard axioms, nothing else. No sorry, admit, native_decide, partial, or unsafe, CI-enforced.

The theorem: under three assumptions, no two conflicting values ever finalize, correct nodes never disagree on a published position, and the blocklace stays well formed. The assumptions are the usual BFT ones:

• a Byzantine-weight bound,
• honest non-equivocation,
• finality permanence (a final wave stays final).

The hard part is that the published order only grows and never reorders. I did not assume that, I derived it:

• the order lists each finalized leader's history in turn,
• so it grows when the finalized-leader sequence grows at the end,
• which happens when the count of finalized waves goes up,
• which happens when finality is permanent.

It all comes down to those three facts.

In the library:

• the weighted quorum-overlap lemma, the arithmetic core of the safety,
• self-enforcing threshold finality, and no two conflicting final leaders,
• a verified, executable, total topological-sort ordering (no partial),
• a coarse and a fine theory, tied by a forward simulation,
• lossless extraction of protocol facts to MeTTa-IL atoms,
• the end-to-end simulation above.

I proved safety, not liveness. Liveness (delivery, no scheduler starvation) holds only under fairness assumptions I state explicitly; I did the structural cores, the temporal argument is next. Finality permanence is an assumption, not derived from a network model.

The protocol is by Keidar, Naor, Poupko and Shapiro; the PoR-weighted variant and the plan are Ben Goertzel's. There is a Cordial Miners chapter in the LeaTTa book and an overview in the repo. Build it with lake build CordialMiners.

LeaTTa 0.4.0

Adds a first, work-in-progress formalization of MeTTa-IL, the MeTTa intermediate language, built from F1R3FLY's MeTTaIL repository (https://github.com/F1R3FLY-io/MeTTaIL).

It is not finished. It models the determinate core and is honest about what is open.

What is checked

• the elaborate, desugar, type-lift, and monomorphize pipeline, pinned by kernel decide against output captured from the real Scala tool on Rholang.module
• the GSLT reduction relation (soundness)
• subject reduction and confluence for SKI and the simply-typed lambda calculus
• the semantic cores of the two papers' calculi (the spice bounded-reachability rule and the mq-calculus Born-rule probability conservation)
• the MeTTa-to-GSLT bridge and the presentation lattice laws with decidable equality

Built with 0 sorry/admit/native_decide/partial/unsafe; the axiom audit shows only the three standard axioms. Full build green, MeTTa differential oracle 270/270.

What is open is listed in the README's MeTTaIL section and in MeTTaIL/SPECIFICATION.md. Formalizing the tool also surfaced five bugs in it, written up for the F1R3FLY team in MeTTaIL/HYPERON_IMPROVEMENTS.md.

The downloadable bundle below is the MeTTa minimal interpreter, unchanged in behavior from 0.3.x. The MeTTaIL work is a Lean formalization and proof library, not part of the binary.

LeaTTa 0.3.1

LeaTTa 0.3.1 is a fix release. The interpreter's behavior is unchanged: the differential oracle still passes 270/270, the regression suite is green, and the development keeps zero sorry, admit, native_decide, partial, or unsafe.

What changed

• Documentation and comment accuracy. A three-round contradiction review (every docstring and comment against the code, and the prose against the code) fixed each discrepancy found. This included a real bug in the operational trace recorder (traceRunFuel dropped the initial state and duplicated the successor) and reconciling the minimal-instruction count to thirteen everywhere.
• Consolidated docs. The reference markdown (proof status, coverage, improvements over Hyperon, sources) now lives in the book's appendix on the docs site; the repository root keeps only README, INSTALL, and CONTRIBUTING.
• Contributor pipeline. CI now gates pull requests on the build, the no-placeholder invariant, the oracle (270/270), and the regression suite, with PR and issue templates.

Install (Linux x86_64)

tar xzf leatta-0.3.1-linux-x86_64.tar.gz
cd leatta-0.3.1-linux-x86_64 && ./install.sh
LeaTTa --min '!(+ 1 (* 2 (- 10 4)))'   # [13]

macOS and Windows binaries are attached by the release workflow. Docs: https://mestto.github.io/LeaTTa/