接下来，计算结果通常会被转化成算术电路，即用于计算多项式的计算模型。算术电路由输入和多个门组成，执行基本的算术运算，例如加法或乘法。整个算术电路可用于生成特定格式（R1CS，约束系统），该格式采用基于约束的公式系统（rank-1 约束系统）的形式来表达算术电路的约束。可验证的算术电路是 zk-SNARKs 算法的输入之一。
二次算术程序（QAP）是线性pcp的一个变体，在可验证算术电路转换为QAP格式的过程中起着至关重要的作用。QAP是一个使用多项式来表示算术电路行为的公式系统。利用QAP，zkSNARKs算法的安全性得到了增强，同时其实现效率也得到了提高。
最后是 zk-SNARK 阶段，利用可验证的算法电路和QAP生成证明。
可见约束系统是至关重要的环节。
目前 Aleo 主网的 PoW 算法属于 AVM 指令集算法，而且是 AVM 部分指令集，所以也算是约束系统的一部分。但仅作为 PoW 算法以及通过 PoW 的方式来优化部分指令集，和 Aleo 完整的 AVM 约束系统没有关系。
https://provable.com/blog/formal-verification-of-constraint-systems
在计算机科学中，形式化验证是证明数学定理的艺术和科学，这些定理断言硬件和软件系统的正确性。通常，这些定理是使用定理证明器等工具来证明的，这些工具由人类专家驱动，根据数学逻辑规则操纵断言。不同类型的形式化验证工具在通用性和自动化之间进行权衡，并具有互补的用途。正式断言系统的正确性涉及制定系统的数学精确规范及其感兴趣的正确性属性（功能、安全性、性能等）。
形式化验证起源于研究和学术界，如今已在硬件开发中变得很常见，并且在软件开发中也得到越来越广泛的应用。在区块链世界中尤其如此，区块链中的高风险（通常是财务上的）和相对的不变性（与硬件共有的特性）使得对正确性的需求比其他软件应用程序更为迫切。形式化验证比测试甚至模糊测试等常规做法提供了无与伦比的保证，因为常规做法无法检查所有可能的情况，而只能对其进行抽样。
在 Provable，我们非常重视保证，除了测试和审计等常规做法外，我们还一直在采用形式化验证。我们的最终目标是将形式化验证应用于Aleo 生态系统的各个方面：区块链、钱包、开发工具、应用程序等。除了形式化验证共识算法之外，我们的重点还放在开发工具上，即通过 Aleo 指令将 Leo 编译为 R1CS。
Leo是 Provable 为零知识应用开发的高级编程语言。Aleo指令是 Aleo 的中级汇编语言，用于表示 Aleo 区块链中的应用程序代码。R1CS（等级 1 约束系统）是零知识证明中使用的电路的标准低级表示。零知识证明断言计算已根据其 R1CS 表示正确执行；它并未说明计算是否根据其 Aleo 指令或 Leo 表示正确执行。这是形式验证发挥作用以完成整个过程的地方：通过证明定理断言 R1CS 表示等同于 Aleo 指令表示，并且 Aleo 指令表示等同于 Leo 表示，零知识证明有效地扩展到 Aleo 指令和 Leo 代码，它们是人类可读和可写的表示。
请注意，这里涉及两种证明：零知识证明，它提供基于密码学的、在统计上压倒性的计算断言证据；形式验证证明，它提供以定理形式表达的、基于逻辑的逻辑断言的无条件证据。
Leo、Aleo 指令和 R1CS 之间的这些等价定理依赖于 Leo 和 Aleo 指令以及 R1CS 的语法和语义的正式规范。这些正式规范本身具有独立的价值，因为它们提供了这些语言在数学上精确且明确的定义。它们还支持开发关于这些语言的定理（不同于等价定理），这些定理验证了确定性和其他语言设计标准等属性。
在撰写本文时，我们正在研究 Leo 和 Aleo 指令的形式化规范，以及上图中某些编译阶段的定理生成和检查。作为形式验证工具，我们使用 ACL2，这是一种工业强度的通用定理证明器，在硬件和软件验证中都很流行。
Aleo 指令对 R1CS 的编译通过适当组合snarkVM小工具（分层组织的组件）来构建零知识电路。我们当前形式验证工作的主要重点是开发断言这些小工具正确性的定理。这些定理反映了小工具的层次结构：复合小工具的定理基于组件小工具的定理。
我们已经在2023 年区块链科学会议 (SBC)（论文）和2023 年 ACL2 研讨会（论文）上发表并展示了我们在电路形式验证方面的初步工作。
ZKT Aleo ZPU 芯片机 ，现正式开启第一批头矿预售！
2024 年全球 ZK 峰会 Aleo-ASIC 最有竞争力品牌！
感兴趣请扫码联系，ZKT ASIC 仅对大客户和大渠道！
转载：ZKTo完成Aleo专用ZPU芯片FPGA与PooL联调测试
重磅！Aleo的ARC42主网已经完成切换实施，PoS减产+PoW增产！
Aleo主网后PoSW数据全面分析汇总(10/28/2024)
什么是SNARK？什么是Varuna SNARK？与ZK-SNARK有什么区别？
ALEO 问答集锦 | 关于质押者、证明者和验证者官方最新解答
ALEO 问答集锦 | Aleo积分到底有什么用？区块奖励重大变化？
