# Publications

## Reports

### Consensus Protocols Formal Verification

| Name | Report | Artifact | Year |
| ---- | ------ | -------- | ---- |
| Ethereum Weak Subjectivity | [PDF](https://github.com/runtimeverification/beacon-chain-verification/blob/master/weak-subjectivity/weak-subjectivity-analysis.pdf) |  | 2020 |
| Ethereum Gasper (GHOST + Casper) | [PDF](reports/consensus-protocols/Ethereum-Gasper.pdf) | [GitHub](https://github.com/runtimeverification/beacon-chain-verification) | 2020 |
| PlatON Giskard | [PDF](reports/consensus-protocols/PlatON-Giskard.pdf) | [GitHub](https://github.com/runtimeverification/giskard-verification) | 2020 |
| Ethereum CBC Casper | [PDF](reports/consensus-protocols/CBC-Casper.pdf) | [GitHub](https://github.com/runtimeverification/casper-cbc-proofs) | 2019-Present |
| Algorand | [PDF](reports/consensus-protocols/Algorand.pdf) | [GitHub](https://github.com/runtimeverification/algorand-verification) | 2019 |
| Ethereum Beacon Chain Phase 0 | [PDF](reports/consensus-protocols/Ethereum-BeaconChain.pdf) | [GitHub](https://github.com/runtimeverification/beacon-chain-spec) | 2019 |
| Ethereum Casper FFG | [PDF](reports/consensus-protocols/Ethereum-Casper.pdf) | [GitHub](https://github.com/runtimeverification/casper-proofs) | 2018 |
| Elrond ESDT | [PDF](reports/consensus-protocols/Elrond-ESDT.pdf)| | 2022 |
| MultiversX Async Calls V2 | [PDF](reports/consensus-protocols/MultiversX-Async-Calls-V2.pdf)| [GitHub](https://github.com/runtimeverification/multiversx-protocol-audit/tree/master/async_call) | 2023 |

### Infrastructure Security Audit, Fuzzing, and Formal Verification

| Name | Report | Artifact | Year |
| ---- | ------ | -------- | ---- |
| Monad | [Monad Execution](reports/infrastructure/Monad_audit_report.pdf) | | 2025 |
| Kora | [Kora Paymaster Service](reports/infrastructure/Kora_audit_report.pdf) | | 2025 |
| Wasmi | [Wasmi - WebAssembly (Wasm) Interpreter](reports/infrastructure/Wasmi_-_WebAssembly_(Wasm)_Interpreter.pdf) | | 2024 |
| Rust Soroban Environment | [rs-soroban-env](reports/infrastructure/Stellar_Soroban_Environment_Audit.pdf) | | 2024 |

### Smart Contracts Security Audit and Formal Verification

| Name | Report | Blog Post | Artifact | Year |
| ---- | ------ | --------- | -------- | ---- |
| OctoLend | [Report](https://github.com/runtimeverification/publications/blob/main/reports/smart-contracts/OctoLend.pdf) |  |  | 2026 |
| Token Wrap | [Report](https://github.com/runtimeverification/publications/blob/main/reports/smart-contracts/Token_Wrap.pdf) |  |  | 2025 |
| TokenOps | [Report](https://github.com/runtimeverification/publications/blob/main/reports/smart-contracts/TokenOps.pdf) |  |  | 2025 |
| Espresso Systems | [Report](reports/smart-contracts/Espresso_Systems_audit_report.pdf) |  |  | 2025 |
| EquitX | [Report](reports/smart-contracts/EquitX_audit_report.pdf) |  |  | 2025 |
| Trustless Work | [Report](reports/smart-contracts/TrustLess_Work_audit_report.pdf) |  |  | 2025 |
| Levery | [Report](reports/smart-contracts/Levery_FV_audit_report.pdf) |  |  | 2025 |
| StellarBroker | [Report](reports/smart-contracts/StellarBroker_report.pdf) |  |  | 2025 |
| Zivoe Vault | [Report](reports/smart-contracts/Zivoe_Vault_FV_audit_report.pdf) |  |  | 2025 |
| Octant | [Report](reports/smart-contracts/Octant_v2_report.pdf) |  |  | 2025 |
| ClickPesa Oracle Aggregator | [Report](https://github.com/runtimeverification/publications/blob/main/reports/smart-contracts/ClickPesa%20Oracle%20Aggregator.pdf) |  |  | 2025 |
| FxHash | [Report](https://github.com/runtimeverification/publications/blob/main/reports/smart-contracts/FxHash%20Token%20Security%20Audit.pdf) |  |  | 2025 |
| Cork Protocol | [FV Summary](reports/smart-contracts/Cork%20FV%20Summary%20Report.pdf) |  |  | 2024 |
| Term Finance | [FV Summary](reports/smart-contracts/Term%20FV%20Summary%20Report.pdf) |  |  | 2024 |
| Oveit | [PDF](reports/smart-contracts/TCA_Oveit_7.10.pdf) |  |  | 2024 |
| Soroswap Aggregator | [Report](reports/smart-contracts/Soroswap_Aggregator.pdf) [Audit Summary](reports/smart-contracts/Soroswap_Aggregator_-_Audit_Summary.pdf) |  |  | 2024 |
| Lido (Dual Governance) | [PDF](reports/smart-contracts/Lido_Dual_Governance_Design_Review.pdf) |  |  | 2024 |
| Optimism | | [Blog Post](https://runtimeverification.com/blog/kontrol-integrated-verification-of-the-optimism-pausability-mechanism) | [Proofs](https://github.com/ethereum-optimism/optimism/tree/876e16ad04968f0bb641eb76f98eb77e7e1a3e16/packages/contracts-bedrock/test/kontrol) | 2024 |
| FxDAO | [PDF](reports/smart-contracts/FxDAO.pdf) |  |  | 2024 |
| Band Standard Reference Contract | [PDF](reports/smart-contracts/Band_Protocol_Soroban-Band_Standard_Reference_Contract.pdf) |  |  | 2023 |
| Synonym | [PDF](reports/smart-contracts/Synonym-audit-report.pdf) | | | 2023 |
| Zivoe Locker Contracts | [PDF](reports/smart-contracts/Zivoe_Locker_Contracts.pdf) | | | 2023 |
| Zivoe Core Contracts | [PDF](reports/smart-contracts/Zivoe_Core_Contracts.pdf) | | | 2023 |
| Hatom Liquid Staking | [PDF](reports/smart-contracts/Hatom-Liquid-Staking.pdf) | | | 2023 |
| Blockswap Stakehouse Withdrawals | [PDF](reports/smart-contracts/Blockswap_Stakehouse_Withdrawals_Audit_Report.pdf) | | | 2023 |
| HydraDX Withdrawal Fee | [PDF](reports/smart-contracts/HydraDX-Omnipool-Withdrawal-Fee.pdf) | | | 2023 |
| Galactic Skyteller v1 | [PDF](reports/smart-contracts/Galactic_Skyteller_V1.pdf) | | | 2023 |
| Ojo | [PDF](reports/smart-contracts/Ojo.pdf) | | | 2023 |
| Gigastar Channel Revenue Distribution | [PDF](reports/smart-contracts/Gigastar_CRD.pdf) | | | 2023 |
| Galactic Skyteller Debit Card v0 | [PDF](reports/smart-contracts/Skyteller_Debit_Card_V0.pdf) | | | 2023 |
| Morpho | [PDF](reports/smart-contracts/Morpho-Audit-Report.pdf) | | | 2023 |
| Proof of Neutrality Network | [PDF](reports/smart-contracts/Proof-Of-Neutrality-Network/Proof-of-Neutrality-Network-Report.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-the-proof-of-neutrality-network) | [Model](reports/smart-contracts/Proof-Of-Neutrality-Network/PoN-Off-Chain-Model.pdf) | 2023 |
| AshSwap | [PDF](reports/smart-contracts/AshSwap.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-ashswap-protocol)| | 2023 |
| Optimism | [PDF](reports/smart-contracts/Optimism-Formal-Verification-Report.pdf) | | | 2022 |
| EigenLayer Design Review | [PDF](reports/smart-contracts/EigenLayer_Design_Review.pdf) | | | 2022 |
| WorldMobileGroup Ownership | [PDF](reports/smart-contracts/WorldMobileGroup.pdf) | | | 2022 |
| EUROe Stablecoin | [PDF](reports/smart-contracts/Euroe%20Stablecoin%20Audit.pdf) | | | 2022 |
| Tinyman AMM v2 | [PDF](reports/smart-contracts/Tinyman-amm-v2-audit/tinyman-amm-v2-audit-report.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-tinyman-amm-v2) | [here](reports/smart-contracts/Tinyman-amm-v2-audit/) | 2022 |
| Hatom Protocol | [PDF](reports/smart-contracts/Hatom-audit-report.pdf) | | | 2022 |
| HydraDX Omnipool | [PDF](reports/smart-contracts/HydraDX-Omnipool-AMM-Audit-Report.pdf) | | | 2022 |
| xBacked | [PDF](reports/smart-contracts/xBacked-audit-report.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-xbacked) | | 2022 |
| Jpg.Store | [PDF](reports/smart-contracts/Jpg.Store-audit-report.pdf) | | | 2022 |
| Pact.fi Router | [PDF](reports/smart-contracts/Pact_Fi_Router.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-pact-s-router-smart-contract) | | 2022 |
| Blockswap Stakehouse, 2nd audit | [PDF](reports/smart-contracts/Blockswap_Stakehouse_2nd_Audit.pdf)| [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-blockswap-s-stakehouse-code-changes) | | 2022 |
| Blockswap Gateway | [PDF](reports/smart-contracts/Blockswap_Gateway.pdf)| | | 2022 |
| Swaap Labs Pools | [PDF](reports/smart-contracts/swaap-audit-report.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-swaap-s-pool-smart-contracts) | | 2022 |
| Quipuswap Stableswap | [PDF](reports/smart-contracts/quipuswap-stableswap.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-quipuswap-stableswap-dex-factory-mode) | | 2022 |
| Hone | [PDF](reports/smart-contracts/hone-report.pdf)| [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-hone-s-liquid-staking-protocol) | | 2022 |
| Gyroscope Protocol | [PDF](reports/smart-contracts/Gyroscope_Protocol_Audit_Report.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-gyroscope-protocol-s-mathematical-model-implementation) | | 2022 |
| EXA Finance | [PDF](reports/smart-contracts/EXA_Finance.pdf)| [Blot Post](https://runtimeverification.com/blog/runtime-verification-audits-exa-finance-s-baskets-smart-contract) | | 2022 |
| Blockswap Stakehouse | [PDF](reports/smart-contracts/Blockswap_Stakehouse.pdf)| [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-blockswap-s-stakehouse-protocol) | | 2022 |
| Algofi AMM & Nanoswap| [PDF](reports/smart-contracts/Algofi-dex-nanoswap.pdf)| | | 2022 |
| Atlendis | [PDF](reports/smart-contracts/atlendis-audit-report.pdf)| [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-atlendis-protocol) | | 2022 |
| Folks Finance (Audit) | [PDF](reports/smart-contracts/Folks-Finance-Code-Audit.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-folks-finance) | | 2022 |
| Folks Finance (Design) | [PDF](reports/smart-contracts/Folks-Finance-Design-Review.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-folks-finance) | | 2022 |
| Alchemix v2 | [PDF](reports/smart-contracts/Alchemix_v2.pdf) | [Blog Post](https://runtimeverification.com/blog/alchemix-v2-audit-and-reviewed-code-fixes) | | 2022 |
| Pact.fi    | [PDF](reports/smart-contracts/Pact_Fi.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-pact) | | 2022 |
| Pact.fi StableSwap | [PDF](reports/smart-contracts/Pact_Fi_StableSwap.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-pact-s-stableswap-amm-smart-contract) | | 2022 |
| SundaeSwap | [PDF](reports/smart-contracts/SundaeSwap.pdf) | | | 2022 |
| Tinyman (Security Review) | [PDF](reports/smart-contracts/Tinyman-security-review.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-tinyman) | | 2022 |
| Tracer Perpetual Pools V2 | [PDF](reports/smart-contracts/Tracer-Perpetual-Pools-V2.pdf) | | | 2021 | 
| Quipuswap TTDex | [PDF](reports/smart-contracts/Quipuswap.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-quipuswap-s-token-to-token-distributed-exchange) | [GitHub](reports/smart-contracts/Quipuswap-analysis.md) | 2021 |
| Stakefish Ethereum Staking 2.0 | [PDF](reports/smart-contracts/stakefish-ethereum-staking-audit-report.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-stakefish-ethereum-staking-2-0) | | 2021 |
| Algodex (phase 2) | [PDF](reports/smart-contracts/Algodex_Dec.pdf)| | | 2021 |
| Algodex (phase 1) | [PDF](reports/smart-contracts/Algodex_Jan.pdf)| | | 2021 |
| Algofi | [PDF](reports/smart-contracts/Algofi.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-algofi-lending-v2) | | 2021 |
| Yieldly Multi-Token Staking Pool | [PDF](reports/smart-contracts/yieldly-multi-pool-audit-report.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-yieldly-s-multi-token-staking-pool) | | 2021 |
| Element Finance Governance | [PDF](reports/smart-contracts/Element_Finance_Governance_Security_Audit_Report.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-elements-finance-governance-protocol) | | 2021 |
| Algorand Governance Rewards | [PDF](reports/smart-contracts/Algorand_Governance_Rewards_audit_report.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-the-rewards-contracts-of-algorand-s-community-governance) | | 2021 |
| Tinyman | [PDF](reports/smart-contracts/Tinyman.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-tinyman) | | 2021 |
| Tezos Liquidity Baking | [PDF](reports/smart-contracts/Tezos-Dexter-Liquidity-Baking.pdf) | | [GitHub](https://github.com/runtimeverification/michelson-semantics/tree/master/tests/proofs/liquidity-baking) | 2021 |
| XET Script | [PDF](reports/smart-contracts/XET-script.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-xet-token-and-its-deployment-script) | | 2021 |
| Tezos Dexter | [PDF](reports/smart-contracts/Tezos-Dexter.pdf) | | [GitHub](https://github.com/runtimeverification/michelson-semantics/tree/master/tests/proofs/dexter) | 2021 |
| Element Finance | [PDF](reports/smart-contracts/ElementFinance.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-elements-finance-governance-protocol) | | 2021 |
| StakerDAO | [PDF](reports/smart-contracts/StakerDAO.pdf) | | | 2021 |
| StakeWise | [PDF](reports/smart-contracts/StakeWise.pdf) | | | 2020 |
| Stakefish | [PDF](reports/smart-contracts/Stakefish-BatchDeposit.pdf) | [Blog Post](https://runtimeverification.com/blog/runtime-verification-audits-stakefish-ethereum-staking-2-0) | | 2020 |
| Ethereum Deposit | [PDF](reports/smart-contracts/Ethereum-Deposit.pdf) | | [GitHub](https://github.com/runtimeverification/deposit-contract-verification) | 2019-2020 |
| Polkadot Module | | | [GitHub](https://github.com/runtimeverification/polkadot-verification) | 2019-2020 |
| GnosisSafe | [PDF](reports/smart-contracts/GnosisSafe.pdf) | | [GitHub](https://github.com/runtimeverification/verified-smart-contracts/tree/master/gnosis) | 2019 |
| Ethereum Casper (Deprecated) | | | [GitHub](https://github.com/runtimeverification/verified-smart-contracts/tree/master/casper) | 2018 |
| Uniswap V1 | [PDF](reports/smart-contracts/Uniswap-V1.pdf) | | [GitHub](https://github.com/runtimeverification/verified-smart-contracts/tree/master/uniswap) | 2018 |
| Bihu | [PDF](reports/smart-contracts/Bihu.pdf) | | [GitHub](https://github.com/runtimeverification/verified-smart-contracts/tree/master/bihu) | 2018 |
| ERC20 Tokens | | | [Github](https://github.com/runtimeverification/verified-smart-contracts/tree/master/erc20) | 2017-2018 |

### zkVM Design Security Audits

| Name | Report | Blog Post | Artifact | Year |
| ---- | ------ | --------- | -------- | ---- |
| Zorp zkVM design review| [PDF](https://github.com/runtimeverification/publications/blob/main/reports/zkvm/Zorp%20zkvm%20audit%20report.pdf) | | | 2023 |

### zkVM Formal Verification

| Name | Report | Blog Post | Artifact | Year |
| ---- | ------ | --------- | -------- | ---- |
| zkEVM Formal Verification - KEVM <> EVM-YUL Lean Equivalence | [Report](reports/zkvm/zkEVM_Formal_Verification_report.pdf) | | [klean](https://github.com/runtimeverification/k/tree/master/pyk/src/pyk/klean), [EVM Equivalence](https://github.com/runtimeverification/evm-equivalence) | 2025 |
| zkEVM Formal Verification - REVM Correctness | [Report](reports/zkvm/zkEVM_Formal_Verification_report.pdf) | | [zkEVM Harness](https://github.com/runtimeverification/zkevm-harness), [RISC-V Semantics](https://github.com/runtimeverification/riscv-semantics) | 2025 |
| Initial Plonky3 verification with Hax | [Milestone 1 - Part 1 (Hax)](reports/zkvm/Part_1_-_Milestone_1_-_Rust_Verification_Through_Lean_4_Tooling_Investigation.pdf') [Milestone 1 - Part 2 (Hax)](reports/zkvm/Part_2_-_Milestone_1_-_Rust_Verification_Through_Lean_4_Tooling_Investigation.pdf) [Milestone 2 (Hax)](reports/zkvm/Discovery_report_for_Milestone_2_—_Implementation_and_Verification.pdf) | | [`rust-lean` repository](https://github.com/Verified-zkEVM/rust-lean) | 2026 |
| Initial Plonky3 verification with Aeneas | [Milestone 3 (Aeneas)](reports/zkvm/Discovery_report_for_Milestone_3_—_Implementation_and_Verification.pdf) | | [`rust-lean` repository](https://github.com/Verified-zkEVM/rust-lean) | 2026 |

## Formal Models and Language Semantics

### Virtual Machines and Execution Environments

| Name | Report | Artifact | Year |
| ---- | ------ | -------- | ---- |
| EVM | [CSF'2018](https://daejunpark.github.io/kevm.pdf) | [GitHub](https://github.com/kframework/evm-semantics) | 2016-Present |
| WASM | | [GitHub](https://github.com/runtimeverification/wasm-semantics) | 2018-Present |
| MIR | | [GitHub](https://github.com/runtimeverification/mir-semantics) | 2022-Present |
| Soroban WASM | | [GitHub](https://github.com/runtimeverification/komet) | 2024-Present |
| RISC-V | | [GitHub](https://github.com/runtimeverification/riscv-semantics) | 2024-Present |
| Elrond WASM | | [GitHub](https://github.com/runtimeverification/elrond-semantics) | 2020-2024 |
| IELE | [FM'2019](http://fsl.cs.illinois.edu/FSL/papers/2019/kasampalis-guth-moore-serbanuta-zhang-filaretti-serbanuta-johnson-rosu-2019-fm/kasampalis-guth-moore-serbanuta-zhang-filaretti-serbanuta-johnson-rosu-2019-fm-public.pdf) | [GitHub](https://github.com/runtimeverification/iele-semantics) | 2016-2021 |

### Smart Contract Languages

| Name | Report | Artifact | Year |
| ---- | ------ | -------- | ---- |
| Tezos Michelson | | [GitHub](https://github.com/runtimeverification/michelson-semantics) | 2019-Present |

### Standard Specifications

| Name | Report | Artifact | Year |
| ---- | ------ | -------- | ---- |
| ERC777 | | [GitHub](https://github.com/runtimeverification/erc777-semantics) | 2018 |
| ERC20 | | [GitHub](https://github.com/runtimeverification/erc20-semantics) | 2017 |