Advanced Formal Verification of HyperEnclave's TEE

Advanced Formal Verification of HyperEnclave's TEE

As shown in the figure below, a Web3 application relies on a stack of layers. The business logic of the contract is written in a high-level programming language, which is compiled into bytecode and interpreted by a bytecode interpreter on the blockchain node. The node runs chain-specific code to compute configurations like staking, as well as a consensus algorithm. Finally, the blockchain node runs on physical cloud infrastructure, which involves system software like operating systems, virtual machine hypervisors, trusted execution environments, and more.

HyperEnclave blog post

Related Blogs

Advanced Web3 Formal Verification of HyperEnclave’s TEE

Advanced Web3 Formal Verification of HyperEnclave’s TEE

CertiK applies a range of analytical methods during audits. This includes careful code review by human auditors, bug-finding through fuzzing, static analysis, model checking with respect to standard protocols, and machine-checked proofs (a.k.a. formal verification).

Advanced Formal Verification of Zero-Knowledge Proof Blockchains

Advanced Formal Verification of Zero-Knowledge Proof Blockchains

Formal verification is a process that mathematically proves the correctness of a system, ensuring it behaves exactly as intended under all defined conditions.

Advanced Formal Verification of ZKP: How ZK Memory Was Proven

Advanced Formal Verification of ZKP: How ZK Memory Was Proven

In this post, we will discuss some interesting technical points that arise along our journey of verifying the zkWasm memory subsystem. The memory is the most distinctive part of a zkVM, so handling this well is a crucial point relevant for all other zkVM verification projects as well.