Web3 基金会很高兴地宣布，去中心化期货计划支持的另一个开创性项目 — GRANDPA 协议的形式化验证是 Polkadot 网络的重要组成部分。该项目由 MLabs 领导，旨在为 Polkadot 最基本的共识机制之一带来数学严谨性，确保其稳健性和安全性。
理解 GRANDPA 的重要性
这 GRANDPA（基于GHOST的递归祖先派生前缀协议） 协议是 Polkadot 最终确定机制的核心，使区块能够在整个网络中快速确定。鉴于其在维护网络完整性方面发挥的关键作用，验证其正确性至关重要。
形式化验证 是一种超越传统软件测试的过程。它使用数学证明来确保协议完全按照预期运行，不留任何错误空间。这种方法在像 Polkadot 这样的系统中至关重要，因为安全性和可靠性是不可协商的。
方法
MLabs 在各种 Cardano 项目中积累了丰富的形式化验证经验，现在正将其专业知识应用于 Polkadot。该团队已着手实施一项严格的流程，包括创建“纸笔”证明并将其实现在 Coq 证明助手中。这种双重方法可确保证明是可靠的，并经过人工和机器的严格验证。
该项目分为三个主要阶段：
- 前言 — 初步构建并将证明分解为更易于管理的引理。
- 安全 — 专注于证明GRANDPA协议的安全性，确保其运行不会对网络造成损害。
- 活跃度 — 确保该协议在任何条件下继续有效运行。
这些阶段的结果将包括 Coq 中的正式证明，它将作为协议正确性的经过验证的保证。
为什么这很重要
该项目证明了 Polkadot 致力于构建安全、可靠且面向未来的网络。通过对 GRANDPA 协议进行形式化验证，Polkadot 正在巩固其在区块链领域的领先地位——数学证明不仅仅是一种工具，而是一种卓越的标准。
未来之路
正式验证过程已接近最后的里程碑，MLabs 正在持续更新其进展。
在他们完成正式化 GRANDPA 协议的复杂任务时，更广泛的 Polkadot 生态系统可以放心，其核心组件之一正在得到最高级别的审查和关注。
有关该项目的信息和更新，请访问 https://github.com/mlabs-haskell/GRANDPA-formal-verification
我们很高兴看到该项目将为 Polkadot 和更广泛的 Web3 社区带来的进步。随着 MLabs 在这一重要工作上的进展，请继续关注更多更新。
