Formally Verifying WebAssembly - A Soroban Case Study
Smart contracts are designed to carry out financial transactions involving millions of dollars. Bugs in these programs are known to have severe consequences. Naturally, formal verification plays a critical role in this domain. In this blog, we present Certora’s recent efforts towards formally verifying Wasm bytecode.
Formally Verifying WebAssembly - A Soroban Case Study October 15, 2024 Formally Verifying WebAssembly A Soroban Case Study Author: Chandrakana Nandi Editors: Uri Kirstein Arie Gurfinkel Alexander Bakst WebAssembly (or Wasm) has recently witnessed significant adoption in blockchains like Arbitrum, Stellar, and Polkadot . For example, in the case of the Stellar blockchain, users write smart contracts on the Soroban platform . These programs are written in Rust and compiled to Wasm which is deployed on the Stellar blockchain within an isolated virtual machine. Smart contracts are designed to carr
saved by
related reading
- A shallow dive into formal verificationvitalik.eth.limo
- The Case Against Formal Verification, 50 Years Laterivan-gavran.github.io
- rsmsrsms.me
- Verifying smart contracts | ethereum.orgethereum.org
- MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Codecseweb.ucsd.edu
- [KO] CosmWasm 101 와씀 1편: Counter 컨트랙트 톺아보기 | by Sigrid Jin | DSRV | Mediummedium.com
- Smart Contract Weakness Classification (SWC)swcregistry.io
- What Are Smart Contracts and How Do They Work?academy.binance.com
- Formally Verifying the Easy Partbrainflow.substack.com
- Sequent — software you can trustsequent.inc
- Wasmi 2.0 - Engineering of the Fastest Wasm Interpreterswasmi-labs.github.io
- inovo_erc721_pbt.pdfdcc.fc.up.pt