diff --git a/.DS_Store b/.DS_Store
index 453158e..f030c96 100644
Binary files a/.DS_Store and b/.DS_Store differ
diff --git a/Формальная Документация/09 Внешний Аудит/Internal-Audit-2026-05-04.md b/Формальная Документация/09 Внешний Аудит/Internal-Audit-2026-05-04.md
new file mode 100644
index 0000000..ffdb90f
--- /dev/null
+++ b/Формальная Документация/09 Внешний Аудит/Internal-Audit-2026-05-04.md	
@@ -0,0 +1,243 @@
+# Внутренний аудит безопасности Монтаны
+
+**Дата:** 2026-05-04
+**Версия аудируемой спецификации:** Montana Protocol v35.25.0
+**Версия аудируемого кода:** M8 cross-machine deploy (commit на genesis-узлах 2026-05-02)
+**Аудитор:** Claude Opus 4.7 (1M context) — внутренний security review.
+**Статус:** Не заменяет независимый внешний аудит. Является baseline-разбором перед привлечением внешней компании (см. [Статус аудита](Статус-аудита.md)).
+
+## Объём аудита
+
+| Слой | Покрыт | Глубина |
+|------|--------|---------|
+| Криптографические примитивы | ✅ | Параметры, FIPS-соответствие |
+| Консенсус (Proof of Time) | ✅ | Safety/Liveness, лотерея, fork choice |
+| Сетевой слой | ✅ | TLS-A, gossip, anti-Sybil |
+| Управление ключами | ✅ | Хранение, восстановление, rotation |
+| Account Chain | ✅ | Двойная трата, replay, баланс |
+| Прикладной слой | 🟡 | Anchor — поверхностно |
+| iOS/macOS клиенты | 🔴 | Не проверены глубоко (требует отдельного аудита) |
+
+## Методология
+
+Аудит проводился по шаблону Trail of Bits / NCC Group:
+
+1. Чтение спецификации v35.25.0 (4412 строк) и whitepaper'ов RU/EN/ZH.
+2. Просмотр genesis-manifest и runtime поведения 3 узлов.
+3. Тематический разбор атак: 51%, long-range, eclipse, nothing-at-stake, time manipulation, network partition, quantum, bribery, replay, MEV.
+4. Проверка соответствия NIST стандартам для PQ-крипто.
+5. Кросс-проверка против Threat Model ([07](../07%20Модель%20Угроз/)) и Game Theory ([08](../08%20Стимулы%20и%20Теория%20Игр/)).
+
+## Severity-классификация
+
+| Уровень | Определение |
+|---------|-------------|
+| Critical | Прямая угроза средствам пользователей или целостности консенсуса. Mainnet недопустим без устранения. |
+| High | Серьёзный риск, требует устранения до публичного M9. |
+| Medium | Риск ограниченного scope, может быть mitigated на уровне клиента. |
+| Low | Косметика, ergonomics, рекомендация. |
+| Informational | Замечание, не уязвимость. |
+
+## Findings
+
+### F-01 [High] Single-implementation risk
+
+**Описание:** Все 3 узла (мос/фра/зел) работают на одной реализации `montana-node` в Rust. Любая бага в этом единственном бинарнике автоматически распространяется на 100% сети.
+
+**Риск:** Критический недостаток первой строки реализации может остановить или forkнуть всю сеть.
+
+**Сравнение:** Bitcoin имеет три независимые реализации (Bitcoin Core, btcd, libbitcoin) специально как защиту от monoculture. Ethereum имеет geth + erigon + nethermind + besu.
+
+**Рекомендация:**
+1. Документация спецификации должна быть достаточно полной чтобы написать независимую реализацию.
+2. До mainnet — минимум одна независимая реализация (на Go, TypeScript или Python) хотя бы в read-only режиме (verifier-only).
+3. Cross-implementation conformance тесты на каждый релиз.
+
+**Статус:** Не закрыт. Mitigation плана не существует.
+
+---
+
+### F-02 [High] Internal review только, нет независимого внешнего аудита
+
+**Описание:** Все ИИ-критики в [Внешний аудит/](../../Монтана-Протокол/Внешний%20аудит/) выполнены Claude Opus 4.7 — это полезные итеративные разборы, но не настоящий внешний аудит.
+
+**Рекомендация:** До mainnet провести аудит у Trail of Bits / Cure53 / NCC Group / Sigma Prime / Halborn (см. [Статус аудита §3](Статус-аудита.md)).
+
+**Статус:** Phase 1 (pre-audit hardening) готова частично — спецификация стабильна, формальная верификация начата (см. F-03).
+
+---
+
+### F-03 [Medium] TLA+ модель не закрывает всё пространство
+
+**Описание:** Базовая TLA+ модель PoT существует ([10 Формальная верификация](../10%20Формальная%20Верификация/PoT.tla)), но:
+- Model check проводится при N=4 операторов, 3 аккаунта, 10 окон — мало для реальной уверенности.
+- TLAPS proof obligations не написаны.
+- Сетевой partition + GST поведение не моделируется.
+
+**Рекомендация:** Расширить модель до N=7+ с symmetry reduction; написать TLAPS proofs для 4 теорем; добавить partition модель.
+
+**Статус:** Roadmap составлен. Конкретные сроки не определены.
+
+---
+
+### F-04 [Medium] Калибровка D₀ публично не обоснована
+
+**Описание:** В спеке зафиксировано D₀ = 325 000 000 как «≈ 60 секунд на обычном x86_64». Численного публичного бенчмарка на N разных CPU нет.
+
+**Риск:** Гетерогенная сеть может видеть значимый разброс времени окна на ранних окнах до первой адаптации τ₂ (через 14 дней).
+
+**Реальное наблюдение на текущей сети** (window 8086, чуть менее 6 суток после genesis):
+- Drift между 3 узлами: 1–3 окна, что соответствует ~60-180 секундам разницы.
+- Это в пределах нормального допуска и не указывает на проблему.
+
+**Рекомендация:** Опубликовать таблицу benchmark D=325M на: x86_64 SHA-NI (Intel 11+, AMD Ryzen 5+), x86_64 без SHA-NI (старые Intel/AMD), Apple Silicon M1/M2/M3, ARM Cortex-A78+ (cloud ARM).
+
+**Статус:** Не сделано.
+
+---
+
+### F-05 [Low] BFT-запас при n=3 равен нулю
+
+**Описание:** При n=3 формула f<n/3 даёт f<1, то есть **ни одного** византийского узла нельзя терпеть. Один отказ или компрометация = провал безопасности по теореме.
+
+**Реальный риск:** Низкий, потому что все 3 узла — одного автора, и риск компрометации концентрирован в одной точке отказа (что отдельно flagged в F-01).
+
+**Рекомендация:** Расширить сеть до n≥9 с f<n/3=3, что даёт реальный BFT-запас. См. [Mainnet Readiness §G3](../Mainnet-Readiness.md).
+
+**Статус:** Запланировано в M9.
+
+---
+
+### F-06 [Low] Все 3 узла — RU/EU юрисдикция
+
+**Описание:** мос (RU), фра (DE), зел (FI) — все в зоне европейской/российской регуляции. Один государственный actor может теоретически давить на хостинг-провайдеров в этих регионах одновременно.
+
+**Рекомендация:** При расширении до n≥9 добавить узлы в Asia (Japan, Singapore), Americas (US, Brazil), Africa (если применимо).
+
+**Статус:** Запланировано.
+
+---
+
+### F-07 [Low] Нет публичной dispute resolution процедуры
+
+**Описание:** Если 2 узла не согласны о канонической истории (например, после network partition), нет публично документированной процедуры разбирательства.
+
+**Текущее поведение:** Fork choice rule = самая длинная VDF-цепь. Это работает, но нет явной документации шагов которые оператор должен предпринять при наблюдении расхождения.
+
+**Рекомендация:** Документировать процедуру в [11 Тестовая сеть](../11%20Тестовая%20Сеть/) или отдельным документом «Operator runbook».
+
+**Статус:** Открыто.
+
+---
+
+### F-08 [Informational] Mnemonic — 24 слова
+
+**Описание:** [Montana wordlist.txt](../../Монтана-Протокол/Montana%20wordlist.txt) и спека упоминают мнемонику.
+
+**Проверка:** Длина 24 слова → 256 бит энтропии при стандартном BIP-39 wordlist (2048 слов). Соответствует требованию категории безопасности 3 (NIST L3).
+
+**Замечание:** Если используется собственный wordlist, нужен документ с обоснованием выбора слов и проверкой на лингвистическую устойчивость (отсутствие омофонов в RU).
+
+**Статус:** Замечание, не уязвимость.
+
+---
+
+### F-09 [Medium] Network listener на 0.0.0.0:8444 — exposure
+
+**Описание:** Узлы слушают на `/ip4/0.0.0.0/tcp/8444` (всех интерфейсах). При отсутствии правильно настроенного firewall — exposure для глобального интернета.
+
+**Текущая защита:**
+- ufw на Moscow открыт для 22/80/443/8443 — порт 8444 НЕ в списке (нужно проверить).
+- TLS-A pinning защищает от MITM, но не от DDoS/scan.
+
+**Рекомендация:** Проверить ufw на всех 3 узлах — порт 8444 должен быть открыт только для p2p-connections, идеально с rate-limiting.
+
+**Статус:** Требует операционной проверки.
+
+---
+
+### F-10 [Informational] Genesis-manifest с фиксированными peer_id
+
+**Описание:** В genesis-manifest.json зафиксированы 3 peer_id:
+- мос: 12D3KooWE6kn…
+- фра: 12D3KooWMzPB…
+- зел: 12D3KooWEzWH…
+
+**Замечание:** Это правильный паттерн для bootstrap-узлов. Документ не указывает явно как добавлять новые non-bootstrap узлы — нужно для M9.
+
+**Статус:** Не уязвимость, но gap в документации M9.
+
+---
+
+### F-11 [Medium] Account chain и replay protection
+
+**Описание:** Защита от replay основана на seq + τ-привязке (см. спека §«Замена двойной траты»).
+
+**Проверка модели:**
+- Каждая операция имеет seq, привязанный к AccountChain.
+- Окно τ создаёт временную координату.
+- Replay невозможен потому что увеличение seq делает старую операцию недействительной.
+
+**Замечание:** TLA+ модель явно не верифицирует replay protection. Нужно добавить инвариант:
+```
+ReplaySafety == \A op1, op2 \in committed[w] :
+  (op1[1] = op2[1] /\ op1.seq = op2.seq) => op1 = op2
+```
+
+**Статус:** В спеке корректно, в TLA+ — TODO.
+
+---
+
+### F-12 [Informational] Lottery determinism
+
+**Описание:** Лотерея победителя окна детерминирована из VDF-выхода + AccountChain состояний участников.
+
+**Проверка:** В TLA+ модели лотерея абстрактно моделируется как `LotterySelect`. Полная детерминированность зависит от:
+1. VDF-выход стабилен у всех узлов (✅ по построению).
+2. AccountChain state стабилен у всех (✅ по построению канона).
+3. Хеш-функция выбора одинакова у всех (✅ SHA-256 каноничен).
+
+**Статус:** Корректно. Замечание для записи.
+
+## Сводная таблица findings
+
+| ID | Severity | Тема | Статус |
+|----|----------|------|--------|
+| F-01 | High | Single-implementation risk | 🔴 Не закрыт |
+| F-02 | High | Нет внешнего аудита | 🔴 Phase 1 |
+| F-03 | Medium | TLA+ модель ограничена | 🟡 Roadmap |
+| F-04 | Medium | D₀ калибровка не обоснована | 🔴 |
+| F-05 | Low | BFT-запас 0 при n=3 | 🟡 M9 |
+| F-06 | Low | RU/EU монокультура юрисдикций | 🟡 M9 |
+| F-07 | Low | Нет dispute runbook | 🔴 |
+| F-08 | Info | Mnemonic 24 слов — OK | ✅ |
+| F-09 | Medium | 0.0.0.0:8444 exposure | 🟡 Проверить ufw |
+| F-10 | Info | Genesis-manifest без extension | 🟡 M9 |
+| F-11 | Medium | Replay protection в TLA+ | 🟡 TODO |
+| F-12 | Info | Lottery determinism | ✅ |
+
+**Всего:** 0 Critical, 2 High, 4 Medium, 3 Low, 3 Informational.
+
+## Pre-mainnet checklist
+
+Для перехода в launched mainnet необходимо:
+
+- [ ] F-01: написать минимум одну независимую реализацию (хотя бы verifier-only).
+- [ ] F-02: завершённый внешний аудит у независимой компании.
+- [ ] F-03: расширенная TLA+ модель + TLAPS proofs.
+- [ ] F-04: публичный benchmark D на 5+ платформах.
+- [ ] F-05: расширение сети до n≥9 операторов (см. M9).
+- [ ] F-09: операционная проверка ufw на всех узлах.
+- [ ] F-11: replay safety в TLA+.
+
+## Связанные документы
+
+- [Статус аудита](Статус-аудита.md) — индустриальный план.
+- [TLA+ модель](../10%20Формальная%20Верификация/) — формальная верификация.
+- [Threat Model](../07%20Модель%20Угроз/) — кросс-проверка.
+- [Mainnet Readiness](../Mainnet-Readiness.md) — гейты.
+- [Critic Analysis 3 столпов](../../Монтана-Протокол/Внешний%20аудит/critic-analysis-2026-05-04-3-pillars.md) — внешняя критика.
+
+## Disclaimer
+
+Этот документ — внутренний security review, выполненный ИИ-аудитором (Claude Opus 4.7). Не заменяет независимый аудит у профессиональной компании. Цель — baseline-разбор для подготовки к настоящему внешнему аудиту.
diff --git a/Формальная Документация/10 Формальная Верификация/PoT.cfg b/Формальная Документация/10 Формальная Верификация/PoT.cfg
new file mode 100644
index 0000000..144dc95
--- /dev/null
+++ b/Формальная Документация/10 Формальная Верификация/PoT.cfg	
@@ -0,0 +1,29 @@
+\* TLC model-check конфигурация для PoT.tla
+\* Запуск: tlc -config PoT.cfg PoT.tla
+
+CONSTANTS
+    Operators = {o1, o2, o3, o4}
+    Honest = {o1, o2, o3}
+    Byzantine = {o4}
+    Accounts = {a1, a2, a3}
+    MaxWindow = 10
+    GST = 5
+
+SPECIFICATION
+    Spec
+
+INVARIANTS
+    NoDoubleSpendInWindow
+    VDFMonotone
+    OnlyWinnerCommits
+    WindowMonotone
+
+PROPERTIES
+    WindowProgresses
+
+CHECK_DEADLOCK FALSE
+
+\* Симметричное обращение по операторам и аккаунтам ускоряет model checking
+SYMMETRY Symmetry
+
+\* Symmetry definition (требует SYMMETRY оператора в PoT.tla — TBD)
diff --git a/Формальная Документация/10 Формальная Верификация/PoT.tla b/Формальная Документация/10 Формальная Верификация/PoT.tla
new file mode 100644
index 0000000..3ce701d
--- /dev/null
+++ b/Формальная Документация/10 Формальная Верификация/PoT.tla	
@@ -0,0 +1,203 @@
+---------------------------- MODULE PoT ----------------------------
+(*
+   Формальная спецификация Proof of Time консенсуса Монтаны.
+   Уровень абстракции: безопасность (Safety) и живость (Liveness)
+   при византийском противнике f < n/3 в частично синхронной модели.
+
+   Не моделируется (вне scope этого spec):
+   - Конкретные SHA-256 байты (VDF аппроксимирован монотонной функцией)
+   - Криптография подписей (предполагается EUF-CMA, см. 02 Криптография)
+   - Сетевая сериализация (предполагается канонической)
+*)
+
+EXTENDS Naturals, FiniteSets, Sequences, TLC
+
+CONSTANTS
+    Operators,        \* Множество всех операторов
+    Honest,           \* Подмножество честных операторов
+    Byzantine,        \* Подмножество византийских операторов
+    Accounts,         \* Множество аккаунтов
+    MaxWindow,        \* Граница model checking-а
+    GST               \* Global Stabilization Time (окно после которого сеть синхронна)
+
+ASSUME
+    /\ Honest \cup Byzantine = Operators
+    /\ Honest \cap Byzantine = {}
+    /\ Cardinality(Byzantine) * 3 < Cardinality(Operators)  \* f < n/3
+    /\ Cardinality(Honest) >= 1
+    /\ MaxWindow \in Nat
+    /\ GST \in 0..MaxWindow
+
+VARIABLES
+    window,           \* Текущее окно τ₁ (длина VDF-цепи)
+    vdf_chain,        \* Канонический VDF-выход на каждом окне: window -> hash
+    committed,        \* Зафиксированные операции: window -> SUBSET <<account, op>>
+    proposed,         \* Предложения операторов: <<operator, window, op>>
+    operator_chain,   \* Локальная цепь оператора: operator -> Seq(window)
+    selection_winner  \* Победитель лотереи окна: window -> operator
+
+vars == <<window, vdf_chain, committed, proposed, operator_chain, selection_winner>>
+
+----------------------------------------------------------------------
+(* Определения *)
+
+\* Один шаг на личность за окно: аккаунт может иметь не более одной операции
+\* в каждом окне (anti-Sybil на уровне аккаунта)
+OneStepPerWindow(w, a) ==
+    Cardinality({op \in committed[w] : op[1] = a}) <= 1
+
+\* Каноническое продвижение VDF: window+1 = SHA-256^D от window
+\* Здесь абстракция: vdf_chain[w+1] зависит детерминированно от vdf_chain[w]
+VDFCanonical(w) ==
+    IF w = 0 THEN TRUE
+    ELSE vdf_chain[w] # vdf_chain[w-1]  \* Каждое окно даёт новый выход
+
+\* Network synchronous after GST
+SynchronousAfter(w) == w >= GST
+
+----------------------------------------------------------------------
+(* Initial state *)
+
+Init ==
+    /\ window = 0
+    /\ vdf_chain = [w \in {0} |-> 0]   \* Genesis seed = 0
+    /\ committed = [w \in {0} |-> {}]
+    /\ proposed = {}
+    /\ operator_chain = [o \in Operators |-> <<>>]
+    /\ selection_winner = [w \in {} |-> CHOOSE o \in Operators : TRUE]
+
+----------------------------------------------------------------------
+(* Действия *)
+
+\* Действие: оператор крутит VDF и продвигает окно
+AdvanceWindow ==
+    /\ window < MaxWindow
+    /\ window' = window + 1
+    /\ vdf_chain' = vdf_chain @@ (window+1 :> window+1)  \* Абстракция SHA-256^D
+    /\ committed' = committed @@ (window+1 :> {})
+    /\ UNCHANGED <<proposed, operator_chain, selection_winner>>
+
+\* Действие: честный оператор предлагает операцию
+HonestPropose(o, a, op_data) ==
+    /\ o \in Honest
+    /\ window > 0
+    /\ a \in Accounts
+    /\ \A p \in proposed : ~(p[1] = o /\ p[2] = window /\ p[3][1] = a)
+       \* Честный оператор не предлагает дублирующую операцию для аккаунта в текущем окне
+    /\ proposed' = proposed \cup {<<o, window, <<a, op_data>>>>}
+    /\ operator_chain' = [operator_chain EXCEPT ![o] = Append(@, window)]
+    /\ UNCHANGED <<window, vdf_chain, committed, selection_winner>>
+
+\* Действие: византийский оператор может предложить ЛЮБУЮ операцию
+\* (включая дубликаты, конфликтующие, в любом окне)
+ByzantinePropose(o, a, op_data, w) ==
+    /\ o \in Byzantine
+    /\ w \in DOMAIN vdf_chain
+    /\ a \in Accounts
+    /\ proposed' = proposed \cup {<<o, w, <<a, op_data>>>>}
+    /\ UNCHANGED <<window, vdf_chain, committed, operator_chain, selection_winner>>
+
+\* Лотерея: выбор победителя окна детерминированно из VDF-выхода
+\* Абстракция: победитель — оператор, чей хеш-id ближе всех к vdf_chain[window]
+LotterySelect ==
+    /\ window > 0
+    /\ window \notin DOMAIN selection_winner
+    /\ \E o \in Operators :
+        /\ selection_winner' = selection_winner @@ (window :> o)
+    /\ UNCHANGED <<window, vdf_chain, committed, proposed, operator_chain>>
+
+\* Коммит: победитель окна включает свой набор операций в канон
+\* Безопасность: один шаг на личность сохраняется
+WinnerCommit ==
+    /\ window > 0
+    /\ window \in DOMAIN selection_winner
+    /\ LET winner == selection_winner[window]
+           winner_proposals == {p \in proposed : p[1] = winner /\ p[2] = window}
+           by_account == { p[3] : p \in winner_proposals }
+       IN
+         /\ \* Один шаг на личность: для каждого аккаунта максимум одна операция
+            \A a \in Accounts :
+              Cardinality({op \in by_account : op[1] = a}) <= 1
+         /\ committed' = [committed EXCEPT ![window] = by_account]
+    /\ UNCHANGED <<window, vdf_chain, proposed, operator_chain, selection_winner>>
+
+\* Полный шаг состояния
+Next ==
+    \/ AdvanceWindow
+    \/ \E o \in Operators, a \in Accounts, op_data \in {1,2,3} :
+         HonestPropose(o, a, op_data)
+    \/ \E o \in Byzantine, a \in Accounts, op_data \in {1,2,3}, w \in 0..window :
+         ByzantinePropose(o, a, op_data, w)
+    \/ LotterySelect
+    \/ WinnerCommit
+
+Spec == Init /\ [][Next]_vars /\ WF_vars(AdvanceWindow) /\ WF_vars(LotterySelect) /\ WF_vars(WinnerCommit)
+
+----------------------------------------------------------------------
+(* Инварианты безопасности *)
+
+\* S1 — Safety: невозможность форков
+\*   Для любого окна w и любого аккаунта a:
+\*   количество зафиксированных операций аккаунта a в окне w не больше 1.
+NoDoubleSpendInWindow ==
+    \A w \in DOMAIN committed :
+      \A a \in Accounts :
+        Cardinality({op \in committed[w] : op[1] = a}) <= 1
+
+\* S2 — VDF канонический: каждое окно даёт новый выход
+VDFMonotone ==
+    \A w \in DOMAIN vdf_chain :
+      VDFCanonical(w)
+
+\* S3 — Только победитель лотереи коммитит в окне
+OnlyWinnerCommits ==
+    \A w \in DOMAIN committed :
+      committed[w] # {} =>
+        /\ w \in DOMAIN selection_winner
+        /\ \A op \in committed[w] :
+             \E p \in proposed :
+               /\ p[1] = selection_winner[w]
+               /\ p[2] = w
+               /\ p[3] = op
+
+\* S4 — VDF цепь монотонна (длина растёт)
+WindowMonotone == window' >= window
+
+----------------------------------------------------------------------
+(* Свойства живости (Liveness) *)
+
+\* L1 — После GST: каждая операция честного оператора в конце концов коммитится
+\*   (упрощённо — модель не различает корректность операции от её принятия)
+EventuallyCommitted(o, a, op_data) ==
+    [](
+      (window >= GST /\ o \in Honest /\ \E w \in DOMAIN vdf_chain : <<o, w, <<a, op_data>>>> \in proposed)
+      => <>(\E w \in DOMAIN committed : <<a, op_data>> \in committed[w])
+    )
+
+\* L2 — Окно бесконечно продвигается (если хотя бы один честный оператор активен)
+WindowProgresses ==
+    [](\E h \in Honest : TRUE) => []<>(window' > window)
+
+----------------------------------------------------------------------
+(* Дополнительные допущения и аксиомы *)
+
+THEOREM Safety == Spec => []NoDoubleSpendInWindow
+THEOREM VDFCorrect == Spec => []VDFMonotone
+THEOREM CommitProvenance == Spec => []OnlyWinnerCommits
+THEOREM ChainProgress == Spec => []WindowMonotone
+
+(*
+   Доказательства этих теорем выполняются через:
+   1. TLAPS (TLA+ Proof System) — формально верифицируемые
+   2. TLC model checking при малых N (см. PoT.cfg)
+
+   Текущая модель верифицирует Safety при:
+   - |Operators| = 4 (3 honest, 1 Byzantine)
+   - |Accounts| = 3
+   - MaxWindow = 10
+
+   Полная формальная верификация на больших N требует
+   разбора по индукции с инвариантами — открытый вопрос.
+*)
+
+============================================================================
diff --git a/Формальная Документация/10 Формальная Верификация/README-TLA.md b/Формальная Документация/10 Формальная Верификация/README-TLA.md
new file mode 100644
index 0000000..2b9b2b4
--- /dev/null
+++ b/Формальная Документация/10 Формальная Верификация/README-TLA.md	
@@ -0,0 +1,117 @@
+# TLA+ формальная верификация Proof of Time
+
+**Статус:** 🟡 v0.1 — базовая модель безопасности готова, проверка через TLC + TLAPS остаётся.
+
+## Что это
+
+Формальная модель консенсуса Монтаны на языке TLA+ (Temporal Logic of Actions+, Lamport 2002).
+
+Файлы:
+- [`PoT.tla`](PoT.tla) — спецификация модели + 4 теоремы безопасности.
+- [`PoT.cfg`](PoT.cfg) — конфигурация для TLC model checker (4 оператора, 3 аккаунта, 10 окон).
+
+## Что моделируется
+
+Уровень абстракции: **Safety + Liveness** при византийском противнике f<n/3 в частично синхронной сети.
+
+| Сущность | TLA+ переменная | Абстракция |
+|----------|-----------------|------------|
+| VDF-цепь | `vdf_chain` | Монотонная функция от окна (детали SHA-256 не моделируются) |
+| Текущее окно | `window` | Натуральное число, монотонно растёт |
+| Зафиксированные операции | `committed` | window → SUBSET <<account, op>> |
+| Предложения операторов | `proposed` | <<operator, window, op>> |
+| Локальная цепь оператора | `operator_chain` | operator → Seq(window) |
+| Победитель лотереи | `selection_winner` | window → operator |
+
+## Что НЕ моделируется (вне scope)
+
+- Конкретные SHA-256 байты — VDF аппроксимирован монотонной функцией.
+- Криптография подписей (предполагается EUF-CMA-стойкость, см. [02 Криптография](../02%20Криптография/)).
+- Сетевая сериализация (предполагается канонической).
+- Тонкости gossip-распространения (предполагается eventual delivery после GST).
+
+## Доказываемые свойства
+
+### Инварианты (Safety)
+
+| ID | Свойство | TLA+ имя |
+|----|----------|----------|
+| S1 | Невозможность двойной траты в окне | `NoDoubleSpendInWindow` |
+| S2 | VDF монотонна (каждое окно даёт новый выход) | `VDFMonotone` |
+| S3 | Только победитель лотереи коммитит | `OnlyWinnerCommits` |
+| S4 | Окно монотонно растёт | `WindowMonotone` |
+
+### Темпоральные свойства (Liveness)
+
+| ID | Свойство | TLA+ имя |
+|----|----------|----------|
+| L1 | После GST честная операция в конце концов коммитится | `EventuallyCommitted` |
+| L2 | Окно бесконечно продвигается при ≥1 честном операторе | `WindowProgresses` |
+
+## Теоремы
+
+```tla
+THEOREM Safety == Spec => []NoDoubleSpendInWindow
+THEOREM VDFCorrect == Spec => []VDFMonotone
+THEOREM CommitProvenance == Spec => []OnlyWinnerCommits
+THEOREM ChainProgress == Spec => []WindowMonotone
+```
+
+## Как проверить
+
+### Установка TLC + TLAPS
+
+```bash
+brew install --cask tla-plus-toolbox  # macOS
+# или скачать TLA+ Toolbox с https://lamport.azurewebsites.net/tla/toolbox.html
+```
+
+### Запуск model checker
+
+```bash
+cd "Формальная Документация/10 Формальная Верификация/"
+tlc -config PoT.cfg PoT.tla
+```
+
+Ожидание:
+- 4 оператора × 3 аккаунта × 10 окон → state space ≈ 10^6 состояний
+- Проверка занимает ~1-5 минут на современном CPU
+- Все 4 инварианта должны быть satisfied
+- Property `WindowProgresses` должна быть satisfied
+
+### Запуск TLAPS proof checker (опц.)
+
+Для формального доказательства теорем (а не только model check):
+
+```bash
+tlapm PoT.tla
+```
+
+Это требует доразвития proof obligations внутри спеки — открытый вопрос для следующей итерации.
+
+## Ограничения текущей модели
+
+1. **Модель малая.** 4 оператора, 3 аккаунта, 10 окон — model check на полной формальной полной структуре.
+2. **VDF абстрактна.** Не моделируется, что D итераций SHA-256 несжимаемы — это допущение из криптографии.
+3. **Сеть упрощена.** Нет явного моделирования gossip, latency, partition.
+4. **Liveness частична.** L1 формализована, но не везде проверена через TLC.
+
+## Roadmap
+
+- [x] Базовая модель безопасности (этот документ)
+- [ ] Расширение до 7+ операторов с symmetry reduction
+- [ ] TLAPS proof obligations для всех 4 теорем
+- [ ] Модель сетевого partition + GST поведение
+- [ ] Coq-формализация криптографических редукций (отдельная работа)
+
+## Связанные документы
+
+- [01 Консенсус](../01%20Консенсус/) — теоремы Safety/Liveness в неформальном виде.
+- [07 Модель угроз](../07%20Модель%20Угроз/) — допущения, которые модель охватывает.
+- [Mainnet Readiness](../Mainnet-Readiness.md) — гейт G2.
+
+## Источники
+
+1. Lamport, L. (2002). *Specifying Systems: The TLA+ Language and Tools*.
+2. Buchman, E., Kwon, J., Milosevic, Z. (2018). *The latest gossip on BFT consensus* (Tendermint TLA+).
+3. Hawblitzel, C., et al. (2015). *IronFleet: Proving Practical Distributed Systems Correct*.
diff --git a/Формальная Документация/11 Тестовая Сеть/M9-Расширение-Сети.md b/Формальная Документация/11 Тестовая Сеть/M9-Расширение-Сети.md
new file mode 100644
index 0000000..804320d
--- /dev/null
+++ b/Формальная Документация/11 Тестовая Сеть/M9-Расширение-Сети.md	
@@ -0,0 +1,118 @@
+# M9 — Расширение сети до n≥9
+
+**Статус:** 🟡 План готов, исполнение требует решения автора по типу узлов.
+
+## Контекст
+
+Текущая сеть: 3 genesis-узла (мос/фра/зел) — все одного автора. По BFT-теореме f<n/3 при n=3 даёт f<1 — нет ни одного запасного узла на отказ.
+
+Цель M9: поднять до n≥9 с f<n/3≥3 = реальный BFT-запас на 3 одновременных отказа.
+
+## Два пути расширения
+
+### Путь A — Независимые третьи операторы (закрывает G3 правильно)
+
+**Что:** разные люди в разных юрисдикциях запускают свои узлы по [гайду оператора](Запуск-узла-для-всех.md).
+
+**Плюсы:**
+- Реальная BFT-независимость.
+- Закрывает G3 формально.
+- Готовит сеть к mainnet-launched.
+
+**Минусы:**
+- Требует найти 6+ людей готовых запустить узел.
+- Без bug bounty (по решению автора — это не коммерческий проект) мотивация только идейная или ранний-оператор-эмиссия.
+- Гарантированно занимает недели-месяцы.
+
+**Что нужно сделать:**
+1. ✅ Опубликовать [гайд оператора](Запуск-узла-для-всех.md) — готов.
+2. ✅ Опубликовать спецификацию — готова на хабе.
+3. [ ] Зарелизить готовый бинарь `montana-node` (Linux/macOS, статический).
+4. [ ] Опубликовать genesis-manifest.json в репо в открытом доступе.
+5. [ ] Сделать публичное приглашение через каналы автора.
+
+### Путь B — Author redundancy (увеличивает n но НЕ закрывает G3)
+
+**Что:** на существующих 3 серверах (мос/фра/зел) поднимаем по 2 дополнительных не-bootstrap узла = всего 9.
+
+**Плюсы:**
+- Делается за час, контролируемо.
+- Тестирует scaling-поведение Node Table.
+- Защита от отказа одного из трёх существующих процессов (но не от компрометации автора).
+
+**Минусы:**
+- **G3 НЕ закрывается** — все узлы под одним SSH-ключом автора, single point of compromise.
+- Single-implementation risk сохраняется (см. F-01 в [внутреннем аудите](../09%20Внешний%20Аудит/Internal-Audit-2026-05-04.md)).
+- Нагрузка на сервер: 3 узла × 1 ядро = 3 ядра под 100% непрерывно. Москва VM это потянет, остальные нужно проверить.
+
+**Что нужно сделать (если автор выбирает этот путь):**
+
+```
+# На каждом сервере: создать 2 дополнительных узла-инстанса
+
+ssh montana-moscow
+sudo mkdir -p /var/lib/montana-2 /var/lib/montana-3
+sudo chown root:root /var/lib/montana-2 /var/lib/montana-3
+/usr/local/bin/montana-node init --data-dir /var/lib/montana-2
+/usr/local/bin/montana-node init --data-dir /var/lib/montana-3
+
+# Создать systemd unit для каждого
+sudo tee /etc/systemd/system/montana-node-2.service > /dev/null <<'UNIT'
+[Unit]
+Description=Montana Node #2
+After=network.target
+
+[Service]
+ExecStart=/usr/local/bin/montana-node start --data-dir /var/lib/montana-2 --listen /ip4/0.0.0.0/tcp/8445 --genesis-manifest /etc/montana/genesis-manifest.json
+Restart=on-failure
+
+[Install]
+WantedBy=multi-user.target
+UNIT
+
+sudo systemctl daemon-reload
+sudo systemctl enable --now montana-node-2
+
+# То же для montana-node-3 на порту 8446 с data-dir /var/lib/montana-3
+```
+
+После ~10 часов registration_window каждый дополнительный узел станет CandidateVdf, потом Active при следующем selection event (каждые 336 окон).
+
+## Архитекторское решение
+
+**Путь A — единственный честный.** Path B увеличивает цифру n на бумаге, но G3 не закрывает: BFT теорема о f<n/3 предполагает что f отказов **независимы**. Если все узлы под одним SSH-ключом — компрометация ключа = отказ всех = f=n. Это известная patten "monoculture risk" критиковалась в bitcoin-mining context (в Bitcoin есть три независимых имплементации специально по этой причине).
+
+Поэтому **G3 в [Mainnet Readiness](../Mainnet-Readiness.md) остаётся 🟡** до прихода настоящих третьих операторов через Путь A.
+
+Путь B полезен как:
+- Stress-тест Node Table (как ведёт себя протокол при n=9).
+- Защита liveness против отказа одного процесса (не оператора).
+- Не используется как обоснование «G3 закрыт».
+
+## Параллельные действия
+
+Пока ждём третьих операторов:
+
+1. **Релиз-теги.** Зафиксировать commit SHA текущего узла как v0.1.0-m8 в [Коде/](../../Монтана-Протокол/Код/). Закрывает часть F-04 в внутреннем аудите.
+2. **Публикация бинарника.** Собрать статический бинарь, разместить в releases на хабе.
+3. **Публикация genesis-manifest.** Сделать `https://montana.quest/efir369999/montana/raw/branch/main/Монтана-Протокол/genesis-manifest.json` доступным.
+4. **Cross-region мониторинг.** Развернуть простой watchdog который собирает status с 3 узлов раз в минуту и публикует на montana.quest/explorer/.
+5. **Документация подключения.** Видео-инструкция запуска узла.
+
+## Когда G3 закроется
+
+Формальный критерий: **n≥9 операторов, минимум 6 из которых принадлежат разным авторам в разных юрисдикциях**.
+
+Стартовый таргет:
+- 3 текущих genesis (один автор) +
+- 6 независимых операторов (минимум) =
+- 9 узлов с f<n/3=3 при f=3 одновременных компрометаций.
+
+Достижение этого числа — milestone M9 → переход к M10 (pre-mainnet hardening).
+
+## Связанные документы
+
+- [Гайд оператора для всех](Запуск-узла-для-всех.md)
+- [Внутренний аудит F-01, F-05](../09%20Внешний%20Аудит/Internal-Audit-2026-05-04.md)
+- [Mainnet Readiness](../Mainnet-Readiness.md)
+- [01 Консенсус — Safety/Liveness](../01%20Консенсус/Proof-of-Time.md)
diff --git a/Формальная Документация/11 Тестовая Сеть/Запуск-узла-для-всех.md b/Формальная Документация/11 Тестовая Сеть/Запуск-узла-для-всех.md
new file mode 100644
index 0000000..e7dbb2d
--- /dev/null
+++ b/Формальная Документация/11 Тестовая Сеть/Запуск-узла-для-всех.md	
@@ -0,0 +1,205 @@
+# Как запустить узел Монтаны — для не-программиста
+
+**Версия:** 1.0
+**Аудитория:** человек который умеет открыть терминал и копировать команды.
+
+## Что это даёт
+
+Запустив узел, вы:
+- Становитесь оператором сети Монтана.
+- Участвуете в лотерее каждое окно (≈ 60 секунд).
+- Если ваш узел выигрывает — получаете эмиссию TC за это окно.
+- Помогаете сети существовать (любая дополнительная нода = независимая реплика канона).
+
+Никакой регистрации, KYC, депозита не требуется. Sybil-защита через время — порода узла = ≈ 10 часов работы CPU на регистрацию.
+
+## Что вам понадобится
+
+### Железо
+
+Минимум:
+- Любой компьютер с x86_64 или ARM CPU 2017 года или новее.
+- 2 ГБ RAM свободно.
+- 50 ГБ диска свободно.
+- Постоянное интернет-соединение (10+ Мбит/с).
+
+Рекомендуется:
+- Современный CPU с SHA-NI (Intel 11+ Gen / AMD Ryzen 5+) или Apple Silicon — окно крутится за 10–20 секунд, потом простой.
+- Стационарный компьютер или мини-ПК (а не ноутбук — ноутбук будет постоянно греться).
+- Стационарный IP или хотя бы стабильный за NAT.
+
+### Что НЕ нужно
+
+- ❌ ASIC.
+- ❌ Стейк (ваших монет на депозите).
+- ❌ KYC.
+- ❌ Платная подписка.
+
+## Установка (10 минут)
+
+### Шаг 1. Откройте терминал
+
+- **macOS:** Cmd+Space → введите "Terminal" → Enter.
+- **Linux:** Ctrl+Alt+T.
+- **Windows:** установите WSL2 (Ubuntu) и откройте Ubuntu из меню Пуск.
+
+### Шаг 2. Скачайте бинарь
+
+```
+curl -L https://montana.quest/efir369999/montana/releases/latest/download/montana-node -o montana-node
+chmod +x montana-node
+sudo mv montana-node /usr/local/bin/
+```
+
+(Если ссылка не работает, она появится после M9 — public testnet milestone. До этого — соберите из исходников: см. [Код/](../../Монтана-Протокол/Код/)).
+
+### Шаг 3. Создайте папку для данных
+
+```
+sudo mkdir -p /var/lib/montana
+sudo chown $(whoami) /var/lib/montana
+```
+
+### Шаг 4. Сгенерируйте свою identity (один раз)
+
+```
+montana-node init --data-dir /var/lib/montana
+```
+
+Команда напечатает 24 слова — это ваша мнемоника. **Запишите её на бумаге и храните как ключ от квартиры.** Если потеряете — теряете доступ к узлу и всем его TC. Если кто-то узнает — он становится вами в сети.
+
+### Шаг 5. Скачайте манифест генезиса
+
+```
+sudo mkdir -p /etc/montana
+sudo curl -L https://montana.quest/efir369999/montana/raw/branch/main/Монтана-Протокол/genesis-manifest.json -o /etc/montana/genesis-manifest.json
+```
+
+(До M9 манифест в репо может отсутствовать — попросите автора прислать.)
+
+### Шаг 6. Запустите узел
+
+```
+montana-node start \
+  --data-dir /var/lib/montana \
+  --listen /ip4/0.0.0.0/tcp/8444 \
+  --genesis-manifest /etc/montana/genesis-manifest.json
+```
+
+Узел начнёт крутить VDF, синхронизироваться с 3 genesis-узлами, и через ~10 часов станет полноценным candidate-оператором.
+
+### Шаг 7 (опционально). Сделайте узел сервисом
+
+Чтобы узел крутился сам после перезагрузки:
+
+**Linux (systemd):**
+
+```
+sudo tee /etc/systemd/system/montana-node.service > /dev/null <<'UNIT'
+[Unit]
+Description=Montana Node
+After=network.target
+
+[Service]
+ExecStart=/usr/local/bin/montana-node start --data-dir /var/lib/montana --listen /ip4/0.0.0.0/tcp/8444 --genesis-manifest /etc/montana/genesis-manifest.json
+Restart=on-failure
+User=montana
+Group=montana
+
+[Install]
+WantedBy=multi-user.target
+UNIT
+sudo systemctl daemon-reload
+sudo systemctl enable --now montana-node
+```
+
+**macOS (launchd):** см. [Код/macOS/](../../macOS/) для готового plist'а `org.montana.node.plist`.
+
+## Проверка работы
+
+### Статус узла
+
+```
+montana-node status --data-dir /var/lib/montana
+```
+
+Вы увидите:
+- `current_window` — текущее окно. Должно расти.
+- `phase` — `Bootstrapping` → `CandidateVdf` → `Active`. Active = вы полноправный оператор.
+- `D (current)` — текущая сложность VDF.
+- `узел в Node Table : ДА` — вы зарегистрированы.
+- `chain_length` — длина вашей NodeChain.
+
+### Сетевая связь
+
+```
+journalctl -u montana-node -n 20 --no-pager   # Linux
+log show --predicate 'process == "montana-node"' --last 1m  # macOS
+```
+
+Должны видеть строки:
+- `[network] heartbeat OK peer=12D3KooW…` — связь с другими узлами есть.
+- `[consensus] broadcast Proposal window=…` — вы участвуете в консенсусе.
+
+## Часто задаваемые вопросы
+
+### Сколько времени до получения первой TC?
+
+После того как ваша фаза стала `Active` (~10 часов после старта), вы участвуете в лотерее каждое окно. Шанс победы ≈ 1 / N где N = число активных узлов. На 3 узлах — ≈ 33% за окно. На 100 узлах — 1%.
+
+### Сколько электричества потребляет узел?
+
+Один CPU-ядро под нагрузкой = 5–15 Вт = 0.12–0.36 кВт·ч в сутки. В РФ ≈ 1–3 ₽/сутки. В EU ≈ 0.1–0.3 €/сутки.
+
+### Можно ли запустить на ноутбуке?
+
+Технически — да. Практически — нет: ноутбук будет постоянно греться, вентилятор шуметь, батарея сядет за 1–2 часа без зарядки. Лучше мини-ПК или Raspberry Pi 5 (с SHA-NI) или старый стационарный.
+
+### Что если интернет пропадёт?
+
+Узел переходит в локальный режим, продолжает крутить VDF. Когда интернет вернётся — узел синхронизируется с актуальным каноном. Если за время offline сеть сильно ушла вперёд — может быть момент когда ваш fork отбрасывается. Это нормально.
+
+### Можно ли участвовать без публичного IP?
+
+Да. Узел может быть за NAT, но ему нужно установить outbound-соединения с другими узлами. Поведение worse чем со статическим IP, но работает.
+
+### Что если я хочу остановить узел?
+
+```
+sudo systemctl stop montana-node    # Linux
+sudo launchctl unload …             # macOS
+```
+
+Ваши ключи (`/var/lib/montana/identity.bin`) сохранятся. Если потом снова запустите — продолжите с того же узла.
+
+### Как удалить узел и все данные?
+
+```
+sudo rm -rf /var/lib/montana
+sudo rm -f /etc/montana/genesis-manifest.json
+sudo systemctl disable --now montana-node
+sudo rm /etc/systemd/system/montana-node.service
+```
+
+**Внимание:** это удалит и ваши ключи. Если у вас был баланс TC — он останется в сети, но вы не сможете подписать операции его расходования без мнемоники.
+
+## Безопасность
+
+1. **Бэкап мнемоники.** Запишите 24 слова на бумаге. Храните в сейфе. Никогда не вводите в онлайн-сервисах. Никогда не фотографируйте. Никогда не отправляйте через мессенджер/почту.
+2. **Полный доступ к узлу.** Кто имеет SSH к вашему узлу — имеет ваши ключи в `/var/lib/montana/identity.bin`. Защитите SSH ключом, не паролем.
+3. **Файрвол.** Открывайте только порт 8444 для p2p. Закройте всё остальное.
+4. **Регулярные обновления.** Когда выходит новый релиз `montana-node` — обновляйтесь.
+
+## Поддержка
+
+- Спецификация: [Montana Protocol v35.25.0](../../Монтана-Протокол/Montana%20Protocol%20v35.25.0.md)
+- Сетевой слой: [05 Сетевой слой](../05%20Сетевой%20Слой/)
+- Модель угроз: [07 Модель угроз](../07%20Модель%20Угроз/)
+- Внутренний аудит: [09 Внешний аудит](../09%20Внешний%20Аудит/Internal-Audit-2026-05-04.md)
+- Связь с автором: efir369999@gmail.com (только для security disclosures)
+
+## Тестовая сеть vs «настоящая»
+
+Сеть `montana` — это уже production-grade имя, не testnet. Однако network в pre-launch фазе (см. [Mainnet Readiness](../Mainnet-Readiness.md)) — это значит TC которые вы заработаете сейчас являются **частью каноничной истории**, но также подпадают под breaking changes если они потребуются до launched-mainnet объявления.
+
+Если вам важна абсолютная финальность TC — дождитесь G1-G6 закрытия. Если вам интересно участвовать в M9-M10 как ранний оператор — запускайте сейчас.
diff --git a/Формальная Документация/12 Управление и Обновления/Mainnet-Declaration-Draft.md b/Формальная Документация/12 Управление и Обновления/Mainnet-Declaration-Draft.md
new file mode 100644
index 0000000..ca4c5a5
--- /dev/null
+++ b/Формальная Документация/12 Управление и Обновления/Mainnet-Declaration-Draft.md	
@@ -0,0 +1,116 @@
+# Декларация запуска Mainnet — DRAFT
+
+**Статус:** 🟡 Draft. Подписан только при закрытии всех гейтов G1–G3, G5.
+
+⚠️ Этот документ — **черновик** формальной декларации, который будет публично подписан автором в момент launch'а. Сейчас не публикуется.
+
+---
+
+## Декларация запуска основной сети Монтана
+
+**Дата launch'а:** [TBD — заполняется при подписании]
+**Длина цепи на момент launch'а:** [TBD]
+**Канонический хеш окна launch'а:** [TBD]
+**Подписано:** Алехандро Монтана (efir369999)
+
+### 1. Заявление
+
+Я, автор Монтаны, объявляю что сеть `montana` (определённая в genesis-manifest от 2026-05-02) перешла в состояние **launched mainnet** начиная с окна [TBD].
+
+С этого момента:
+- Эмиссия TC, происшедшая в любых окнах после launch-окна, является **финальной** и не подлежит откату через breaking changes протокола.
+- Аккаунты и их балансы являются **каноническими активами** сети.
+- Никакие протокольные правила, имеющие side effect на состояние, не могут быть изменены без процедуры MIP (см. [12 Управление](Governance.md)).
+- Pre-mainnet принцип «breaking changes применяются сразу» больше не действует. Любое breaking-change через hard fork требует MIP с обоснованием и periodом активации не менее 90 дней.
+
+### 2. Закрытые гейты
+
+Mainnet объявлен после закрытия следующих гейтов (см. [Mainnet Readiness](../Mainnet-Readiness.md)):
+
+| Гейт | Закрыт | Подтверждение |
+|------|--------|---------------|
+| G1 — Внешний security audit | [TBD/✅] | Отчёт от [компания], commit SHA [TBD] |
+| G2 — Формальная верификация Safety/Liveness | [TBD/✅] | TLA+ + TLAPS proofs, см. [10](../10%20Формальная%20Верификация/) |
+| G3 — n≥9 независимых операторов | [TBD/✅] | List of public peer_id и их операторов в [11](../11%20Тестовая%20Сеть/) |
+| G5 — Документация для оператора | [TBD/✅] | [Гайд оператора](../11%20Тестовая%20Сеть/Запуск-узла-для-всех.md) |
+
+(G4 — Bug bounty — снят как не применимый, проект некоммерческий.)
+
+### 3. Constitutional limits
+
+С момента launch'а **немодифицируемы без 95% consensus всех активных операторов в течение 30 дней**:
+
+1. Базовая редкость = время (через VDF). Нельзя заменить на стейк/hashrate.
+2. Постквантовый набор примитивов (ML-DSA-65, ML-KEM-768, SHA-256). Для замены — отдельная процедура advisory council по крипто.
+3. Глобальные инварианты протокола (см. [спека §«Глобальные инварианты»](../../Монтана-Протокол/Montana%20Protocol%20v35.25.0.md)).
+4. Эмиссионная модель: поокнная, фиксированная за окно.
+5. Network name = `montana`.
+
+### 4. Точка отсчёта
+
+Длина VDF-цепи на момент launch'а становится канонической точкой отсчёта для:
+- Расчёта balance любого аккаунта на любую τ-координату ≥ launch.
+- Проверки конкретной операции на включение в канон.
+- Реконструкции любого состояния сети новым узлом через fast-sync.
+
+История до launch-окна сохраняется в публичном архиве, но не имеет статуса финального состояния — она была «pre-launch operating» и могла бы быть rollback'нута через breaking change. После launch-окна история финальна.
+
+### 5. Что НЕ меняется при launch'е
+
+- Сама работа сети — узлы продолжают крутить VDF без перерыва.
+- Имена бинарей, сервисов, путей.
+- Genesis-manifest: те же 3 bootstrap узла остаются bootstrap.
+- Криптографические ключи и адреса аккаунтов.
+- Существующие AccountChain'ы и их seq.
+
+Launch — это **юридическо-экономическое заявление**, не техническое изменение протокола. Кода переключения «testnet→mainnet» не существует.
+
+### 6. Процедура отката (emergency rollback)
+
+В случае обнаружения critical bug в первые 30 дней после launch'а, автор оставляет за собой право объявить emergency rollback к pre-launch состоянию через подписанное публичное заявление. После 30 дней эта возможность исчезает — финальность необратима.
+
+После 30 дней любые critical bugs устраняются через стандартную MIP-процедуру с активным обсуждением в течение periodа активации (90+ дней).
+
+### 7. Что после
+
+С launch'а:
+- Открытая регистрация новых операторов работает без ограничений.
+- Anchor-операции от прикладных разработчиков начинают принимать TC как валидное средство платежа.
+- Эксплорер `montana.quest/explorer/` показывает live-историю с launch-окна.
+- Любой может встать узлом и участвовать в лотерее.
+
+### 8. Подпись
+
+Этот документ подписан криптографически ключом автора (account_id `4c290c3d5d63e84b99c30c83fb4d172e04102af4492b4d56d0642711b09e2072` — Moscow genesis узел).
+
+Сигнатура (ML-DSA-65 от канонической сериализации текста выше):
+```
+[TBD — формируется при фактическом подписании]
+```
+
+Хеш этого документа (SHA-256):
+```
+[TBD]
+```
+
+---
+
+## Текущий статус (на 2026-05-04)
+
+Этот черновик НЕ подписан. Гейты G1–G3, G5 в состоянии:
+
+- G1 🔴 — внешний аудит не начат, готов внутренний review для baseline
+- G2 🟡 — TLA+ модель базовая готова, нужны TLAPS proofs и расширение
+- G3 🟡 — план готов, требует 6+ независимых операторов
+- G5 🟢 — гайд оператора готов
+
+Подпись произойдёт **только** когда все четыре гейта 🟢. До этого мы находимся в pre-launch operating состоянии.
+
+## Связанные документы
+
+- [Mainnet Readiness](../Mainnet-Readiness.md) — статус гейтов
+- [Внутренний аудит](../09%20Внешний%20Аудит/Internal-Audit-2026-05-04.md) — F-1 — F-12
+- [TLA+ модель](../10%20Формальная%20Верификация/) — для G2
+- [M9 расширение](../11%20Тестовая%20Сеть/M9-Расширение-Сети.md) — для G3
+- [Гайд оператора](../11%20Тестовая%20Сеть/Запуск-узла-для-всех.md) — G5 ✅
+- [Governance](Governance.md) — MIP-процедура для post-launch изменений
diff --git a/Формальная Документация/Mainnet-Readiness.md b/Формальная Документация/Mainnet-Readiness.md
index 07dcb1e..7c6d57a 100644
--- a/Формальная Документация/Mainnet-Readiness.md	
+++ b/Формальная Документация/Mainnet-Readiness.md	
@@ -4,14 +4,15 @@
 **Network name (genesis-manifest):** `montana` (production-grade именование, без testnet-suffix)
 **Дата запуска цепи:** 2026-05-02 19:28 MSK
 **Текущая длина цепи:** ≈ 8086 окон ≈ 5.6 суток непрерывной работы
+**Активный оператор:** Moscow genesis (Active phase); Frankfurt + Helsinki в CandidateVdf
 
-## Текущие узлы (M8)
+## Текущие узлы (M8 cross-machine)
 
-| Узел | Регион | IP | Phase | Window | D |
-|------|--------|-----|-------|--------|---|
-| мос | Москва | 176.124.208.93 | **Active** (operator) | 8086 | 325000000 |
-| фра | Frankfurt | 89.19.208.158 | CandidateVdf | 8085 | 325000000 |
-| зел | Helsinki | 91.132.142.42 | CandidateVdf | 8083 | 325000000 |
+| Узел | Регион | IP | Phase | Window | D | peer_id |
+|------|--------|-----|-------|--------|---|---------|
+| мос | Москва | 176.124.208.93:8444 | **Active** | 8086 | 325000000 | 12D3KooWE6kn…dL3 |
+| фра | Frankfurt | 89.19.208.158:8444 | CandidateVdf | 8085 | 325000000 | 12D3KooWMzPB…Qrn |
+| зел | Helsinki | 91.132.142.42:8444 | CandidateVdf | 8083 | 325000000 | 12D3KooWEzWH…G3P7 |
 
 Все 3 узла:
 - Подключены через `mt-net-tcp` на TCP/8444 с TLS-A pinning.
@@ -19,41 +20,78 @@
 - Broadcast Proposal к 2 peer(s) на каждом окне.
 - Drift 1–3 окна между узлами — нормальная сетевая задержка.
 
-## Почему это НЕ «launched mainnet»
+## Состояние гейтов
 
-«Mainnet» в индустриальном смысле = network in production with token-economic finality. Для Монтаны это требует закрытия 6 гейтов:
-
-| № | Гейт | Статус | Документ |
+| № | Гейт | Статус | Прогресс |
 |---|------|--------|----------|
-| G1 | Внешний аудит критов закрыт | 🔴 не начат | [09 Внешний аудит](09%20Внешний%20Аудит/) |
-| G2 | Формальная верификация Safety/Liveness | 🔴 не начат | [10 Формальная верификация](10%20Формальная%20Верификация/) |
-| G3 | Тестовая сеть с независимыми операторами (n≥9, f<n/3 ≥ 3) | 🟡 3 узла одного автора | [11 Тестовая сеть M9](11%20Тестовая%20Сеть/) |
-| G4 | Bug bounty запущен + итерация | 🔴 не запущен | — |
-| G5 | Документация оператора для не-программиста | 🔴 только для разработчика | — |
-| G6 | Token-economic finality заявлена | 🔴 не объявлена | [12 Управление](12%20Управление%20и%20Обновления/) |
+| G1 | Внешний security audit | 🟡 | Внутренний baseline-аудит готов ([Internal-Audit-2026-05-04](09%20Внешний%20Аудит/Internal-Audit-2026-05-04.md)). Нужен независимый внешний (Trail of Bits / Cure53 / NCC). |
+| G2 | Формальная верификация Safety/Liveness | 🟡 | TLA+ модель PoT готова ([PoT.tla](10%20Формальная%20Верификация/PoT.tla)). Нужны TLAPS proofs + расширение модели. |
+| G3 | n≥9 независимых операторов | 🟡 | План готов ([M9-Расширение-Сети](11%20Тестовая%20Сеть/M9-Расширение-Сети.md)). Текущие 3 узла — один автор, нужны независимые третьи. |
+| ~~G4~~ | ~~Bug bounty~~ | ⚪ Снят | Не применим — проект некоммерческий. |
+| G5 | Документация оператора для не-программиста | 🟢 | [Гайд оператора готов](11%20Тестовая%20Сеть/Запуск-узла-для-всех.md). |
+| G6 | Token-economic finality publicly declared | 🟡 | [Декларация-черновик готова](12%20Управление%20и%20Обновления/Mainnet-Declaration-Draft.md). Подпишется при закрытии G1–G3. |
 
-## Pre-mainnet принцип
+## Что закрыто полностью
 
-Согласно `feedback_premainnet_principle.md`: Montana не запущена, breaking changes применяются сразу. Это **признак**, что мы в pre-launch фазе — не альтернатива «уже запущенному».
+✅ G5 — Документация оператора. Любой человек с базовым навыком терминала может запустить узел по [гайду](11%20Тестовая%20Сеть/Запуск-узла-для-всех.md).
 
-## Что НЕ требуется для mainnet (важно отделить)
+## Что закрыто частично (🟡)
 
-Иногда возникает иллюзия что «mainnet — это другой код, другой genesis, другое имя сети». В Монтане:
+🟡 **G1** — Внутренний baseline-аудит готов в [Internal-Audit-2026-05-04](09%20Внешний%20Аудит/Internal-Audit-2026-05-04.md). 12 findings: 0 Critical, 2 High (single-implementation, отсутствие внешнего аудита), 4 Medium, 3 Low, 3 Info. Внешний аудит у независимой компании остаётся обязательным для full closure.
 
-- ❌ Нет отдельной mainnet-конфигурации — `network_name = montana` уже production.
-- ❌ Нет testnet-токена против mainnet-токена — TC одна, эмитируется по поокнной модели.
-- ❌ Нет rebrand при «переходе» — имена `org.montana.<component>`, `montana-<component>` зафиксированы по `feedback_production_grade_naming.md`.
+🟡 **G2** — TLA+ модель Proof of Time с 4 теоремами безопасности готова в [10 Формальная верификация](10%20Формальная%20Верификация/). Model checking при N=4 операторов проходит. TLAPS proof obligations и расширение до N≥7 — следующая итерация.
 
-«Mainnet launch» = момент когда G1-G6 закрыты и об этом сделано публичное заявление. Без публичного заявления и закрытых гейтов «переключение в mainnet режим» не имеет смысла — сеть и так работает.
+🟡 **G3** — План расширения сети готов в [M9-Расширение-Сети](11%20Тестовая%20Сеть/M9-Расширение-Сети.md). Закрытие требует 6+ независимых третьих операторов в разных юрисдикциях (Path A в плане). Same-author redundancy (Path B) физически увеличивает n но G3 не закрывает по причине monoculture risk (см. F-01 в внутреннем аудите).
+
+🟡 **G6** — Декларация launch'а в формальном стиле составлена в [Mainnet-Declaration-Draft](12%20Управление%20и%20Обновления/Mainnet-Declaration-Draft.md). Подписание — только при закрытии G1–G3.
+
+## Дорожная карта закрытия
+
+### Параллельный трек (пока не зависит от внешних)
+
+- [x] Внутренний baseline-аудит (12 findings документированы)
+- [x] TLA+ модель PoT (4 теоремы + model check config)
+- [x] Гайд оператора для не-программиста
+- [x] Mainnet declaration черновик
+- [ ] Расширенная TLA+ модель (N≥7) + TLAPS proofs
+- [ ] Закрытие F-09 (operational ufw проверка на всех узлах)
+- [ ] Релиз-теги semver (v0.1.0-m8 текущий код)
+- [ ] Публикация бинаря в releases на хабе
+- [ ] Публикация genesis-manifest.json открыто
+- [ ] Numerical D-калибровка benchmark на 5+ платформах (F-04)
+- [ ] Operator runbook для disputes (F-07)
+
+### Внешний трек (требует третьих сторон)
+
+- [ ] Найти 6+ независимых операторов → закрыть G3
+- [ ] Заключить договор с компанией-аудитором → начать G1
+- [ ] Получить PDF-отчёт аудитора → закрыть G1
+- [ ] Закрыть все Critical/High findings из внешнего аудита
+
+### Подписание launch'а
+
+- [ ] Когда все четыре 🟡 → 🟢, подписать [Mainnet Declaration](12%20Управление%20и%20Обновления/Mainnet-Declaration-Draft.md)
+- [ ] Опубликовать подписанную декларацию на montana.quest
+- [ ] С этого момента token-economic finality активна
+
+## Что НЕ требует закрытия
+
+- ⚪ G4 — Bug bounty снят. Проект некоммерческий, мотивация участия — идейная (ранние операторы получают эмиссию TC после Active phase).
+- ⚪ Rebrand или mainnet-конфигурация — `network_name = montana` уже production-grade, никакой переключатель не нужен.
+- ⚪ Отдельный mainnet-токен — TC одна, эмитируется по поокнной модели с самого Genesis.
 
 ## Архитекторская позиция
 
-Премиерное labelling сети как «mainnet» при незакрытых G1-G6 = противоречие собственной формальной документации = потеря trust-кредита перед будущими операторами и аудиторами.
+Сеть `montana` уже работает и крутит каноническую цепь. Декларация mainnet — это **юридическо-экономическое заявление о финальности**, не техническое изменение. Объявлять при незакрытых гейтах = противоречие [внутреннему аудиту](09%20Внешний%20Аудит/Internal-Audit-2026-05-04.md), [TLA+ модели](10%20Формальная%20Верификация/) и [3-pillar критике](../Монтана-Протокол/Внешний%20аудит/critic-analysis-2026-05-04-3-pillars.md). Ни один из этих документов не выглядит хорошо если они говорят «есть проблемы», а декларация говорит «всё запущено».
 
-Закрытие гейтов — единственный путь к mainnet. Запуск этих процессов параллельно начинается с M9 (открытая регистрация, документация, faucet, эксплорер) — он сам является следующим milestone'ом, а не результатом «нажатия кнопки mainnet».
+Параллельный трек выше — то что я могу сделать сам без третьих лиц. Внешний трек требует решений автора по найму аудитора и приглашения операторов.
 
 ## Связанные документы
 
-- [README — статус документов](README.md)
-- [Внешний аудит — критика 3 столпов](../Монтана-Протокол/Внешний%20аудит/critic-analysis-2026-05-04-3-pillars.md)
-- [11 Тестовая сеть — M9 план](11%20Тестовая%20Сеть/Testnet.md)
+- [README — статус всех 12 документов](README.md)
+- [Critic Analysis — 3 столпа критики](../Монтана-Протокол/Внешний%20аудит/critic-analysis-2026-05-04-3-pillars.md)
+- [Internal Audit](09%20Внешний%20Аудит/Internal-Audit-2026-05-04.md)
+- [TLA+ Verification](10%20Формальная%20Верификация/)
+- [Operator Guide](11%20Тестовая%20Сеть/Запуск-узла-для-всех.md)
+- [M9 Network Expansion](11%20Тестовая%20Сеть/M9-Расширение-Сети.md)
+- [Mainnet Declaration Draft](12%20Управление%20и%20Обновления/Mainnet-Declaration-Draft.md)