montana/Формальная Документация/10 Формальная Верификация/План.md

Формальная верификация Монтаны

Версия: черновик 1.0 Текущий статус: 🔴 Не начата.

1. Цель

Математическое доказательство ключевых свойств протокола в формальной системе (TLA+, Coq, Isabelle/HOL).

Это самый высокий уровень зрелости L1-блокчейна. Tendermint, Algorand, Cardano — у всех есть формальные модели хотя бы консенсуса.

2. Что должно быть верифицировано

2.1 Консенсус Proof of Time

• Safety теорема S1 (01 Консенсус §4.1): невозможность форков при f<n/3.
• Liveness теорема L1 (01 Консенсус §4.2): включение операций после GST.
• Fork choice rule — самая длинная цепь VDF, формализация и устойчивость.

2.2 Криптография

• KAT-таблицы для ML-DSA-65, ML-KEM-768, SHA-256 — соответствие FIPS-стандартам.
• Канонический формат сериализации — биективность, отсутствие неоднозначности.

2.3 Account Chain

• Двойная трата невозможна в пределах окна τ₁.
• Anti-инфляция (баланс не растёт без эмиссии).
• Replay protection через seq + τ-привязку.

2.4 Лотерея

• Победитель окна детерминирован при заданных входах.
• Невозможность смещения исхода атакующим с f<n/3.

3. Выбор инструмента

Инструмент	Сильные стороны	Применимость к Монтане
TLA+	Распределённые системы, model checking	✅ Идеально для PoT consensus
Coq	Полная теорема-проверка	Для криптографических редукций
Isabelle/HOL	Аналог Coq	Для математической части
K Framework	Operational semantics	Не нужен — нет VM
Lean 4	Современный mathlib	Альтернатива Coq

Рекомендация: начать с TLA+ (consensus + safety/liveness), затем дополнить Coq (крипто-редукции) при необходимости.

4. План работ

Phase 1 — TLA+ модель консенсуса (3-6 месяцев)

• Спецификация PoT в TLA+ (модель сети, операторы, VDF, лотерея).
• Доказательство Safety через TLAPS.
• Liveness через temporal logic.
• Model checking при малых N (3, 5, 7 операторов) через TLC.
• Публикация модели в этой папке.

Phase 2 — Coq крипто-редукции (опционально, если аудит требует)

• EUF-CMA редукция ML-DSA-65 формализована.
• Не самостоятельная задача — обычно делается в академическом контексте либо ссылается на сторонние формализации (NIST PQC has some).

Phase 3 — Account Chain свойства

• Inv: баланс ≥ 0 на любой τ-точке.
• Inv: двойная трата невозможна.
• Inv: эмиссия монотонна и фиксирована.

5. Связанные документы

• 01 Консенсус — теоремы, требующие верификации.
• 07 Модель угроз — допущения, которые модель должна охватить.
• 09 Внешний аудит — комплементарный к этому слою.

6. Источники

1. Lamport, L. (2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers.
2. Buchman, E. et al. (2018). The latest gossip on BFT consensus (Tendermint TLA+).
3. Algorand formal model: github.com/algorand/specs.
4. IronFleet (Hawblitzel et al., 2015). IronFleet: Proving Practical Distributed Systems Correct. SOSP.