Formal verification is a process that mathematically proves the correctness of a system, ensuring it behaves exactly as intended under all defined conditions. Given the complexity and the high-stakes nature of blockchain technology, where flaws can lead to significant financial losses or breaches of privacy, formal verification goes beyond traditional testing or auditing by providing a mathematical proof that certain properties of a program are correct, thereby eliminating a broad class of potential bugs and vulnerabilities.

Zero knowledge proofs (ZKPs) are critical for scaling blockchain. The smart contracts of tomorrow will run on advanced zero knowledge virtual machines (zkVMs), such as zkEVM for Ethereum contracts and zkWasm for Wasm contracts. This is a paradigm shift from traditional VMs to those powered by ZKPs, accommodating a broader range of applications, such as gaming platforms and high-performance computing solutions.

We recently achieved a significant milestone by completing the first full formal verification of a zkVM, the zkWasm circuits. This breakthrough sets a new standard in the industry, demonstrating that comprehensive formal verification is feasible for complex zero knowledge circuits. By ensuring that every zero knowledge proof verified corresponds uniquely and correctly to its intended smart contract execution, CertiK is leading the way in securing the next generation of blockchain applications.

Formal Verification of ZKP Applications

For ZKP-based applications, formal verification plays a crucial role in addressing two principal classes of security and correctness concerns. The first class involves verifying the correctness of zero knowledge circuits. This verification process ensures that each zero knowledge proof accepted by a proof checker corresponds precisely to a single, licit transaction specific to that application. Since this type of verification is unique to each zero knowledge circuit, it is typically tailored to specific applications.

The second class focuses on the correctness of the zero knowledge proof checker itself, including its underlying cryptography. This aspect of formal verification is universal across applications, ensuring that the foundational components that validate proofs are reliable and function correctly.

While both classes of formal verification are critical, the formal verification of zero knowledge circuits, due to their application-specific nature, is an area of high demand and focus. We prioritize this aspect of formal verification, addressing the nuanced and specific needs of zero knowledge circuits to ensure the highest level of security and correctness.

For zkVM circuits, the actual smart contract code that runs on the VM circuit also contributes to defining the transaction. FV of these smart contract code’s security and correctness is also highly desirable. This has been the case since blockchain and smart contract exist, and CertiK have been a leader in doing these smart contract FVs in the past.

The Current State of Formal Verification of ZKPs

Formal verification of ZKPs has been conducted primarily on application-specific circuits, such as those used for token transfers. These efforts should not be underestimated in terms of complexity. However, when it comes to zkVM circuits—used within more generalized virtual machines like those handling smart contracts—the challenges increase dramatically.

The inherent complexity of these zkVM circuits, compounded by the vast size and dynamic nature of the smart contract executions they support, has made their complete formal verification an elusive goal. Until recently, no complete formal verification of a zkVM circuit for an operational blockchain had been successfully demonstrated. The daunting nature of this task often led researchers to limit their formal verification efforts to very small and partial subsets of the zkVM, tackling the easier pieces of the technology before attempting more comprehensive verification.

Traditionally, the security and correctness of blockchain systems and smart contracts were primarily established through audits, with formal verification serving as an optional but stronger guarantee. This is partly due to the fact it is possible to run multiple implementations of the chain while achieving decentralized consensus, exposing bugs and attacks in the process. However, in the landscape of next-generation ZKP-based blockchains, formal verification is no longer a luxury, it’s a necessity. The inherent complexity of ZKP cryptographic theories and algorithms, along with the dynamic nature of smart contract execution in general-purpose zero knowledge circuits like zkVMs, demands the scrutiny that only formal verification can provide. These zero knowledge circuits face added challenges due to their implementation-specific nature, which compresses full computations into succinct proofs, making them less amenable to the decentralized consensus benefits enjoyed by traditional blockchain systems.

CertiK's Formal Verification of zkWasm

CertiK achieved a significant milestone by conducting the full formal verification of zkWasm circuits based on their Rust implementation. This achievement marks the world’s first complete formal verification of any zkVM implementation. Our verification process ensured that each zero knowledge proof validated by the zkWasm proof checker was uniquely associated with a corresponding smart contract execution on the zkWasm VM.

By managing dynamic zkWasm states and operations, such as memory handling and function calls/returns, we effectively enhanced the reliability of the system. Critical bugs were identified and rectified during the FV process, underscoring the essential role of formal verification in the development and deployment of zkVMs.

This comprehensive verification means that all smart contracts operating on zkWasm chains have their zero-knowledge proofs' existence and correctness universally guaranteed, eliminating the need for individual formal verification of ZKP for each smart contract. Additionally, we also conducted a thorough security review of zkWasm. This parallel process identified and resolved critical bugs in the initial implementation of zkWasm, enhancing the overall reliability and security of the system.

The Advanced Formal Verification Process for zkWasm

We pioneered an advanced formal verification approach for zkWasm by developing a modular FV framework specifically designed to model the nuances of zkWasm circuits, such as circuit arithmetization in the Halo2 style. This framework was designed to reflect the specific guarantees and assumptions inherent to VM operations. By integrating machine automation with expert human insight, we were able to produce rigorous, machine-checked mathematical proofs.

These proofs confirm that the implementation of zkWasm circuits meets all specified guarantees and performs exactly as expected. Furthermore, they verify that the zero knowledge proofs generated by these circuits accurately correspond to the correct execution of Wasm-based smart contracts. This ensures a high level of trust and security in the deployment and functionality of smart contracts on the zkWasm platform.

zkEVM and Beyond

Though developed initially for zkWasm, our advanced formal verification framework is designed to be adaptable to other zkVMs, including the zero-knowledge Ethereum Virtual Machine (zkEVM). The common challenges faced by smart contract VMs, such as managing dynamic memory and control-flow, are addressed within this framework. This adaptability is crucial as it allows the framework to be effectively applied to the unique requirements of different zkVMs.

This success in fully verifying zkWasm showcases the technology’s capabilities in the broader domain of ZKP circuits. The experience gained from addressing the details of zero knowledge circuit arithmetization, particularly those implemented in the Halo2 style—a technique widely used in numerous ZKP applications—positions CertiK uniquely to assist with formally verifying other ZKP initiatives.

Next-generation blockchain technology requires formal verification, particularly for systems utilizing zero knowledge proofs.

If you’re a builder on or of a zero knowledge blockchain, reach out today to learn more about how CertiK can prove the security of your systems.

FAQ

What Are Zero Knowledge Proofs?

Zero Knowledge Proofs (ZKP) are a significant technological advancement with wide-reaching implications for privacy and scalability. In Web3, where decentralized computation must balance privacy with performance, ZKP offers a powerful solution. This technology enables the compression of complex computation data and execution steps into concise proofs that contain no information about the input data itself. By doing so, ZKP addresses some of the most pressing performance and scalability challenges faced by blockchain networks. By also enhancing privacy, ZKPs provide a dual benefit that is vital for the widespread adoption of blockchain technology.

What is a zkVM?

ZKP can be implemented on the blockchain in two primary ways. The first method involves creating application-specific "circuits" designed to generate zero knowledge proofs for particular types of transactions, such as token transfers. This approach is similar to how basic transactions like Bitcoin transfers are handled.

The second, more sophisticated method involves developing general circuits for smart contract virtual machines (VMs), like the Ethereum Virtual Machine (EVM). These general-purpose circuits, known as zkVMs, are capable of loading any smart contract along with its input data and generating a zero knowledge proof for the contract's specific execution results.

By integrating the flexibility of smart contracts with the privacy and efficiency of ZKP, zkVMs are essential for scaling Layer 2 solutions and are expected to be foundational for future scalable Layer 1 networks. Given this critical role, ensuring the highest level of security and correctness of zkVM circuits is a top priority.

What is zkWasm?

zkWasm is a specific application of zkVM technology, which merges zero-knowledge proofs (ZKPs) with WebAssembly (Wasm) to significantly improve privacy and scalability in blockchain applications. WebAssembly is a compact binary instruction format designed for fast, efficient execution, which is increasingly used in high-performance web and blockchain environments, including gaming platforms. By integrating ZKPs, zkWasm enables the secure execution of complex computations without exposing any sensitive underlying data. This is crucial for enhancing the privacy of smart contracts and other blockchain-based applications.

What is zkEVM?

A zkEVM, or zero-knowledge Ethereum Virtual Machine, is a variant of zkVM tailored specifically for the Ethereum ecosystem. This technology utilizes ZKPs to enable secure, scalable, and private transactions within Ethereum. Unlike zkWasm, which is designed with a broader focus, zkEVM is deeply integrated with Ethereum's existing infrastructure and has achieved more extensive development and adoption. It offers a unique approach to enhancing scalability and privacy, complementing the capabilities provided by zkWasm but with a distinct focus on Ethereum’s specific needs.

Further Reading

• What is Formal Verification in Smart Contract Auditing?
• Formal Verification, the Move Language, and the Move Prover
• Formal Verification of ERC-20 Tokens
• Challenges Encountered In the Formal Verification of ERC-20 Contracts
• Advanced Web3 Formal Verification of HyperEnclave’s TEE
• Formal Verification of TON Master Chain Contracts
• DeepSEA: Advanced Web3 Formal Verification of a Smart Contract Compiler