chore: follow the upstream leanMultisig → leanVM repository rename

.claude/skills/hive/SKILL.md

@@ -16,7 +16,7 @@ description: |
   Negative triggers: Do NOT activate for spinning up a local devnet to RUN it rather than
   test it (use the leanQuickstart skill). Do NOT activate for consensus container shapes /
   fork choice / state transition (use the leanSpec skill). Do NOT activate for aggregation
-  / zkVM / proof internals (use the leanMultisig skill). Do NOT activate for the metric
+  / zkVM / proof internals (use the leanVM skill). Do NOT activate for the metric
   contract — names/types/buckets/labels — (use the leanMetrics skill). Do NOT activate for
   pure docs-site (mdBook) work. Do NOT activate when working outside the Verity project.
 ---
@@ -150,7 +150,7 @@ Paths are relative to the hive repo root, read at `master`.
 ## 7. Relationship to the other skills & Verity
 
 - **leanQuickstart** (separate skill) = spin up and **run** a local lean devnet.
-- **leanSpec** / **leanMultisig** / **leanMetrics** (separate skills) = protocol &
+- **leanSpec** / **leanVM** / **leanMetrics** (separate skills) = protocol &
   container shapes / aggregation & zkVM / the metric contract.
 - **hive** (this skill) = the **test harness** that exercises clients (build + `--sim` +
   `--client`), especially the `lean` simulator.

.claude/skills/leanMetrics/SKILL.md

@@ -14,7 +14,7 @@ description: |
   any work exposing or monitoring consensus-client metrics in Verity.
   Negative triggers: Do NOT activate for consensus container shapes / fork choice /
   state transition behavior (use the leanSpec skill). Do NOT activate for aggregation /
-  zkVM / proof internals (use the leanMultisig skill). Do NOT activate for pure docs-site
+  zkVM / proof internals (use the leanVM skill). Do NOT activate for pure docs-site
   (mdBook) work. Do NOT activate when working outside the Verity project.
 ---
 
@@ -126,10 +126,10 @@ authoritative for the contract.
 3. For coverage/status questions, read the per-client status column (✅/📝/□).
 4. In your output, cite the **`metrics.md` section + the `main` commit SHA** you checked.
 
-## 5. Relationship to leanSpec & leanMultisig & Verity
+## 5. Relationship to leanSpec & leanVM & Verity
 
 - **leanSpec** (separate skill) = consensus protocol & container shapes (Python).
-- **leanMultisig** (separate skill) = aggregation + zkVM (Rust).
+- **leanVM** (separate skill) = aggregation + zkVM (Rust).
 - **leanMetrics** (this skill) = the observability **metric contract** (Prometheus
   names/types/buckets/labels) + Grafana dashboards.
 - Verity's `verity-metrics` crate implements leanMetrics; **ethlambda** and **Ream** are

.claude/skills/leanQuickstart/SKILL.md

@@ -14,7 +14,7 @@ description: |
   and any work spinning up or running a local lean multi-client devnet for Verity.
   Negative triggers: Do NOT activate for consensus container shapes / fork choice /
   state transition (use the leanSpec skill). Do NOT activate for aggregation / zkVM /
-  proof internals (use the leanMultisig skill). Do NOT activate for the metric
+  proof internals (use the leanVM skill). Do NOT activate for the metric
   contract — names/types/buckets/labels — (use the leanMetrics skill); this skill
   only covers RUNNING the bundled Prometheus/Grafana stack. Do NOT activate for pure
   docs-site (mdBook) work. Do NOT activate when working outside the Verity project.
@@ -114,10 +114,10 @@ Paths are relative to the lean-quickstart repo root, read at `main`.
    `metrics/docker-compose-metrics.yaml` if you want the Prometheus/Grafana stack.
 4. In your output, cite the **file/script + the `main` commit SHA** you checked.
 
-## 5. Relationship to leanSpec, leanMultisig, leanMetrics & Verity
+## 5. Relationship to leanSpec, leanVM, leanMetrics & Verity
 
 - **leanSpec** (separate skill) = consensus protocol & container shapes (the chain rules).
-- **leanMultisig** (separate skill) = aggregation + zkVM proof internals.
+- **leanVM** (separate skill) = aggregation + zkVM proof internals.
 - **leanMetrics** (separate skill) = the observability **metric contract** (names/types/
   buckets/labels). This skill only covers **running** the bundled Prometheus/Grafana
   stack, not what the metrics are.

.claude/skills/leanSpec/SKILL.md

@@ -8,7 +8,7 @@ description: |
   test vectors. Maps a topic to the authoritative leanSpec path for any protocol element.
   Triggers: "leanSpec", "leanSpecを確認", "仕様を確認", "Verityの仕様", "prime", "verity context",
   "where is the spec for", "container shape", "コンテナの形", "3SF", "fork choice",
-  "state transition", "XMSS", "leanMultisig", "devnet spec", and starting any Verity
+  "state transition", "XMSS", "leanVM", "devnet spec", and starting any Verity
   implementation or review work.
   Negative triggers: Do NOT activate for pure docs-site work (mdBook page authoring or
   build/serve). Do NOT activate when working outside the Verity project.
@@ -84,7 +84,7 @@ Paths are relative to the leanSpec repo root, read at `origin/main`.
 | Genesis / validator / chain config | `src/lean_spec/subspecs/{genesis,validator,chain}/`, `forks/lstar/containers/config.py` |
 | API | `src/lean_spec/subspecs/api/` |
 | Conformance test vectors | `tests/consensus/devnet/{state_transition,fc,ssz,networking,sync,verify_signatures}/` |
-| leanMultisig (aggregation / zkVM) | **not** in leanSpec — use the dedicated `leanMultisig` skill (`github.com/leanEthereum/leanMultisig`) |
+| leanVM (aggregation / zkVM) | **not** in leanSpec — use the dedicated `leanVM` skill (`github.com/leanEthereum/leanVM`) |
 | ethlambda (Rust *design* reference, not spec) | external `github.com/lambdaclass/ethlambda` |
 
 ## 4. How to use (implementing / reviewing / answering)

.claude/skills/leanMultisig/SKILL.md → .claude/skills/leanVM/SKILL.md

@@ -1,80 +1,85 @@
 ---
-name: leanMultisig
+name: leanVM
 description: |
   Ground every question about post-quantum signature aggregation and the zkVM in
-  leanMultisig — the authoritative spec and Rust reference implementation
-  (github.com/leanEthereum/leanMultisig), always read from the latest remote main.
+  leanVM — the authoritative spec and Rust reference implementation
+  (github.com/leanEthereum/leanVM), always read from the latest remote main.
   Verity's verity-crypto crate depends on it directly. Use before implementing,
   reviewing, or answering anything about XMSS aggregation, Type-1/Type-2 proofs, the
   prover/verifier, the zkVM, the zkDSL, or WHIR.
-  Triggers: "leanMultisig", "lean_multisig", "leanMultisigを確認", "署名集約", "aggregation",
+  Triggers: "leanVM", "lean_vm", "leanVMを確認", "leanMultisig", "lean_multisig" (the
+  repo's former name — old references still mean this skill), "署名集約", "aggregation",
   "Type-1 proof", "Type-2 proof", "zkVM", "zkDSL", "WHIR", "prover", "verifier",
   "verity-crypto", and any work touching signature aggregation or proof generation in Verity.
   Negative triggers: Do NOT activate for consensus container shapes / fork choice / state
   transition (use the leanSpec skill). Do NOT activate for pure docs-site work. Do NOT
   activate when working outside the Verity project.
 ---
 
-# leanMultisig — source of truth for aggregation & the zkVM
+# leanVM — source of truth for aggregation & the zkVM
 
-leanMultisig (`github.com/leanEthereum/leanMultisig`) is a minimal zkVM targeting
+> Renamed upstream from **leanMultisig** to **leanVM** (2026-08-14; the old GitHub URL
+> redirects). Older Verity docs, memories, and upstream discussions may still use the old
+> name — they refer to this same repository.
+
+leanVM (`github.com/leanEthereum/leanVM`) is a minimal zkVM targeting
 aggregation of hash-based (Generalized-XMSS) signatures. It is the **authoritative spec
 and Rust reference implementation** for everything aggregation/zkVM-related in Verity.
 Verity's `verity-crypto` crate depends on it directly (as a pinned git dependency).
 
 ## 0. Core principle
 
 - The behavior of signature aggregation, Type-1/Type-2 proofs, the prover/verifier, the
-  zkVM and its zkDSL is defined by **leanMultisig** (its Rust crates + design docs). When
+  zkVM and its zkDSL is defined by **leanVM** (its Rust crates + design docs). When
   in doubt, read the source.
 - Division of authority with the leanSpec skill: **leanSpec** defines the *consensus
   containers* that carry proofs (`TypeOneMultiSignature`, `SignedBlock.proof` =
-  `ByteList512KiB`, the verify entry points). **leanMultisig** defines how those proofs
+  `ByteList512KiB`, the verify entry points). **leanVM** defines how those proofs
   are *produced and verified*. For container shapes → leanSpec; for proof internals →
   here.
 
-## 1. Always read leanMultisig from the remote `main` (no local path assumptions)
+## 1. Always read leanVM from the remote `main` (no local path assumptions)
 
-leanMultisig moves fast. Read the latest `main` of the canonical upstream directly from
+leanVM moves fast. Read the latest `main` of the canonical upstream directly from
 the remote — this works for every developer and in CI, with no dependency on anyone's
 local clone path.
 
-Repo: `github.com/leanEthereum/leanMultisig` (canonical; do **not** use a personal fork).
+Repo: `github.com/leanEthereum/leanVM` (canonical; do **not** use a personal fork).
 
 ```bash
 # Latest main commit — cite this SHA in your output:
-gh api repos/leanEthereum/leanMultisig/commits/main --jq '.sha'
+gh api repos/leanEthereum/leanVM/commits/main --jq '.sha'
 
 # Read a file at main:
-gh api "repos/leanEthereum/leanMultisig/contents/crates/xmss/xmss.md?ref=main" --jq '.content' | base64 -d
+gh api "repos/leanEthereum/leanVM/contents/crates/xmss/xmss.md?ref=main" --jq '.content' | base64 -d
 # raw fallback (no gh):
-curl -s https://raw.githubusercontent.com/leanEthereum/leanMultisig/main/crates/xmss/xmss.md
+curl -s https://raw.githubusercontent.com/leanEthereum/leanVM/main/crates/xmss/xmss.md
 
 # List a directory at main:
-gh api "repos/leanEthereum/leanMultisig/contents/crates?ref=main" --jq '.[].name'
+gh api "repos/leanEthereum/leanVM/contents/crates?ref=main" --jq '.[].name'
 # Full tree:
-gh api "repos/leanEthereum/leanMultisig/git/trees/main?recursive=1" --jq '.tree[].path'
+gh api "repos/leanEthereum/leanVM/git/trees/main?recursive=1" --jq '.tree[].path'
 ```
 
-No `gh`/`curl`? Use WebFetch on `https://github.com/leanEthereum/leanMultisig/blob/main/<path>`.
+No `gh`/`curl`? Use WebFetch on `https://github.com/leanEthereum/leanVM/blob/main/<path>`.
 
 If you happen to have a local clone, you *may* use it for fast navigation/grep — but
 `git fetch origin` first and read `origin/main` (clones drift onto feature branches and
 forks). Never assume a specific clone path.
 
 ## 2. How Verity consumes it
 
-- `verity-crypto` depends on leanMultisig as a **pinned git dependency** in `Cargo.toml`.
+- `verity-crypto` depends on leanVM as a **pinned git dependency** in `Cargo.toml`.
   The pinned commit is what Verity builds against; the latest `main` is the source of
   truth for understanding/spec questions. When bumping the pin, re-read `main`.
 - The proving stack is expensive; the prover context is set up once at startup. Verity
   produces Type-1 proofs only when acting as an aggregator; every node verifies.
 
 ## 3. Topic → authoritative location map
 
-Paths are relative to the leanMultisig repo root, read at `main`.
+Paths are relative to the leanVM repo root, read at `main`.
 
-| Topic | leanMultisig (authoritative) |
+| Topic | leanVM (authoritative) |
 |---|---|
 | XMSS signature scheme | `crates/xmss/` (+ `crates/xmss/xmss.md`) |
 | Aggregation: Type-1 / Type-2 proofs | `crates/rec_aggregation/` (+ `crates/rec_aggregation/TYPE1_TYPE2_LAYOUT.md`) |
@@ -90,14 +95,14 @@ Paths are relative to the leanMultisig repo root, read at `main`.
 
 ## 4. How to use (implementing / reviewing / answering)
 
-1. Read the **authoritative leanMultisig path at `main`** for the topic first.
+1. Read the **authoritative leanVM path at `main`** for the topic first.
 2. For the consensus containers carrying proofs, defer to the **leanSpec** skill.
-3. In your output, cite the **leanMultisig path + the `main` commit SHA** you checked.
+3. In your output, cite the **leanVM path + the `main` commit SHA** you checked.
 
 ## 5. Relationship to leanSpec & Verity
 
 - **leanSpec** (separate skill) = consensus protocol spec & container shapes (Python).
-- **leanMultisig** (this skill) = aggregation + zkVM (Rust); produces/verifies the proofs
+- **leanVM** (this skill) = aggregation + zkVM (Rust); produces/verifies the proofs
   that fill leanSpec's containers.
 - Verity (Rust) wires both together: `verity-types` (leanSpec shapes) +
-  `verity-crypto` (leanMultisig + Generalized-XMSS). The client is pre-implementation today.
+  `verity-crypto` (leanVM + Generalized-XMSS). The client is pre-implementation today.

ARCHITECTURE.md

@@ -70,7 +70,7 @@ flowchart TB
     subgraph B["Runtime Shell — Rust, panic-free"]
         direction LR
         CODEC["SSZ codec + hash_tree_root<br/>wire bytes ↔ typed values"]
-        CRYPTO["Signature verification<br/>verity-crypto: XMSS · leanMultisig"]
+        CRYPTO["Signature verification<br/>verity-crypto: XMSS · leanVM"]
         STORE["State + fork-choice store<br/>single writer · threads immutable values"]
         DB["Database<br/>blocks · states · anchor"]
         FFI["FFI bindings layer"]
@@ -167,8 +167,9 @@ upstream Lean library name per Rust's `-sys` convention.
 
 - `verity-p2p` — gossip and req/resp over libp2p.
 - `verity-crypto` — adapter over the two upstream signature libraries: [`leansig`](https://github.com/leanEthereum/leanSig)
-  for per-validator XMSS sign / verify, and [`leanMultisig`](https://github.com/leanEthereum/leanMultisig)
-  for aggregation and aggregate-proof verification. One capability contract, two suppliers behind it.
+  for per-validator XMSS sign / verify, and [`leanVM`](https://github.com/leanEthereum/leanVM)
+  (formerly leanMultisig) for aggregation and aggregate-proof verification. One capability
+  contract, two suppliers behind it.
 - `verity-db` — persistence (Repository): blocks, states, aggregate proofs, and the finalized anchor.
   Keeps the storage concern out of the single-writer aggregate coordinator. See
   [Storage engine and retention](#storage-engine-and-retention).

CLAUDE.md

@@ -18,7 +18,7 @@ Owner-ratified ground rules for the first Rust code. Do not re-open these withou
 - **Goal**: a full node from the start (networking included), not a fixtures-passing library. leanSpec fixture conformance is still the CI backbone.
 - **Crates**: start with a single `verity-consensus` crate (no chain/validator split). Proposer selection lives chain-side as a pure function next to STF/fork choice. Shared types stay a module until a second crate exists.
 - **Dependencies**:
-  - XMSS: [`leansig`](https://github.com/leanEthereum/leanSig) as a git dependency, **rev-pinned** (not branch-tracked), for per-validator sign / verify. Aggregation and aggregate-proof verification come from [`leanMultisig`](https://github.com/leanEthereum/leanMultisig) — both sit behind `verity-crypto`'s one capability contract, so a doc naming only one of them is incomplete, not contradictory.
+  - XMSS: [`leansig`](https://github.com/leanEthereum/leanSig) as a git dependency, **rev-pinned** (not branch-tracked), for per-validator sign / verify. Aggregation and aggregate-proof verification come from [`leanVM`](https://github.com/leanEthereum/leanVM) (renamed upstream from `leanMultisig` on 2026-08-14; the old URL redirects) — both sit behind `verity-crypto`'s one capability contract, so a doc naming only one of them is incomplete, not contradictory.
   - SSZ: `libssz` 0.2.2 (lambdaclass). [NyxFoundation/leanSSZ](https://github.com/NyxFoundation/leanSSZ) (proven Lean SSZ, C ABI PoC complete) is deliberately NOT adopted initially — it is the future Lean-adoption candidate for SSZ.
   - Networking: upstream `rust-libp2p` (QUIC, gossipsub, reqresp). Fork only if a concrete need materializes, as lambdaclass did for ethlambda.
   - Storage: **RocksDB** behind a backend trait with an in-memory sibling implementation (ethlambda's `StorageBackend` split). Decided 2026-08-10 — see **Storage** below.

DOMAIN_MODEL.md

@@ -34,7 +34,7 @@ below; this section is the *strategic* frame above it.
 |---|---|---|---|---|
 | **State Transition** | Consensus-critical | `State` aggregate + `SignedBlock` processing; justification / finalization invariants | Verified Core (pure fns) | Verity Consensus (separate Lean repo) |
 | **Fork Choice** | Consensus-critical | `Store` aggregate, LMD GHOST, head / safe_target, payload `new → known` | Verified Core pure decision fns **+** Runtime Shell single-writer store | Verity Consensus + `verity-chain` |
-| **Signature & Aggregation** | Supporting | signatures, Type-1 / Type-2 proofs, verify / aggregate | Runtime Shell | `verity-crypto` (ACL → leanSig, leanMultisig) |
+| **Signature & Aggregation** | Supporting | signatures, Type-1 / Type-2 proofs, verify / aggregate | Runtime Shell | `verity-crypto` (ACL → leanSig, leanVM) |
 | **Serialization** | Supporting | SSZ encode / decode, `hash_tree_root`, merkleization | Runtime Shell | `verity-types` (+ external SSZ lib) |
 | **Validator Duties** | Supporting | proposer / attester duties, production, signing, aggregation scheduling | I/O Edge | `verity-validator` |
 | **Networking** | Generic | gossip topics, req / resp, peers | I/O Edge | `verity-p2p` |
@@ -62,7 +62,7 @@ pattern names *how* each relationship is governed.
 |---|---|---|
 | **leanSpec** | State Transition / Fork Choice | **Conformist** on container shapes; **Partnership** on correctness (proofs find spec bugs; fixes flow back upstream) |
 | **leanSig** | Signature & Aggregation | **ACL / Anti-Corruption Layer** (adapter) — per-validator XMSS sign / verify |
-| **leanMultisig** | Signature & Aggregation | **ACL / Anti-Corruption Layer** (adapter) — aggregation and aggregate-proof verification |
+| **leanVM** | Signature & Aggregation | **ACL / Anti-Corruption Layer** (adapter) — aggregation and aggregate-proof verification |
 | **leanMetrics** | Telemetry | **Conformist** (exact metric contract) |
 | **external SSZ library** | Serialization | **ACL / adapter** |
 
@@ -86,7 +86,7 @@ flowchart LR
     subgraph ext["External upstream contexts"]
         SPEC["leanSpec"]
         SIGLIB["leanSig"]
-        MULTI["leanMultisig"]
+        MULTI["leanVM"]
         METR["leanMetrics"]
         SSZ["SSZ library"]
     end

README.md

@@ -22,7 +22,7 @@ Verity makes a different bet — that the implementation should be *proven* to m
 ## References
 
 - https://github.com/leanEthereum/leanSpec
-- https://github.com/leanEthereum/leanMultisig
+- https://github.com/leanEthereum/leanVM
 - https://github.com/leanEthereum/leanMetrics
 - https://hive.leanroadmap.org/
 - https://observatory.leanroadmap.org/

_typos.toml

@@ -13,7 +13,7 @@ extend-exclude = [
 [default.extend-words]
 # "ser" — serialization abbreviation (mermaid node IDs, serde ser/de), not a typo of "set".
 ser = "ser"
-# "symetric" — the real directory name in leanMultisig (`crates/backend/symetric`), misspelled
+# "symetric" — the real directory name in leanVM (`crates/backend/symetric`), misspelled
 # upstream. Correcting it in our docs would point readers at a path that does not exist.
 symetric = "symetric"
 

docs/src/concepts/formal-verification.md

@@ -1,6 +1,6 @@
 ---
 title: Formal Verification
-last_updated: 2026-07-22
+last_updated: 2026-08-17
 tags:
   - formal-verification
   - lean4
@@ -119,7 +119,7 @@ What must be trusted for the claim to hold — listed so no link stays implicit:
   library computes the proven functions.
 - **Cryptography.** `hash_tree_root` collision resistance is an axiom (SSZ-7); the algebra
   of Poseidon / KoalaBear and XMSS is ArkLib's domain and enters the model only at call
-  sites; leanMultisig's implementation is trusted in the Runtime Shell.
+  sites; leanVM's implementation is trusted in the Runtime Shell.
 - **The Rust toolchain and shell.** rustc, and the Runtime Shell / I/O Edge code — held to
   the panic-free bar and model checking rather than proof.
 - **Hardware and OS**, under everything.