1. Why Formalize MeTTa? Blockchain, AGI, and Verifiable Semantics🔗

MeTTa is headed for use as an on-chain / smart-contract language. On a blockchain, a contract's behaviour must be predictable, replayable, and auditable. An optimised on-chain evaluator must be provably faithful to the published semantics, or a miner and a verifier could disagree on the result. A machine-checked metatheory is what lets you close that gap. That is what drives LeaTTa's emphasis:

• Determinism / replayability: the abstract machine is a single-valued function; all non-determinism is reified in an explicit result list, never in the transition relation.

• Type soundness: a well-typed program is never rejected with a spurious error, and a reported type error is faithful (never fabricated).

• Auditability: the knowledge base (contract state) is mutated only by explicit, attributable add-atom/remove-atom; pure reduction never changes it.

• Gas: a resource-bounded variant in which energy is provably never created.

• Optimisation-faithfulness: first-argument indexing computes exactly the published semantics' result set.