Publications

July 1, 2026 · View on GitHub

Reports

Consensus Protocols Formal Verification

NameReportArtifactYear
Ethereum Weak SubjectivityPDF2020
Ethereum Gasper (GHOST + Casper)PDFGitHub2020
PlatON GiskardPDFGitHub2020
Ethereum CBC CasperPDFGitHub2019-Present
AlgorandPDFGitHub2019
Ethereum Beacon Chain Phase 0PDFGitHub2019
Ethereum Casper FFGPDFGitHub2018
Elrond ESDTPDF2022
MultiversX Async Calls V2PDFGitHub2023

Infrastructure Security Audit, Fuzzing, and Formal Verification

NameReportArtifactYear
MonadMonad Execution2025
KoraKora Paymaster Service2025
WasmiWasmi - WebAssembly (Wasm) Interpreter2024
Rust Soroban Environmentrs-soroban-env2024

Smart Contracts Security Audit and Formal Verification

NameReportBlog PostArtifactYear
Matrixdock RWAReport2026
OctoLendReport2026
Token WrapReport2025
TokenOpsReport2025
Espresso SystemsReport2025
EquitXReport2025
Trustless WorkReport2025
LeveryReport2025
StellarBrokerReport2025
Zivoe VaultReport2025
OctantReport2025
ClickPesa Oracle AggregatorReport2025
FxHashReport2025
Cork ProtocolFV Summary2024
Term FinanceFV Summary2024
OveitPDF2024
Soroswap AggregatorReport Audit Summary2024
Lido (Dual Governance)PDF2024
OptimismBlog PostProofs2024
FxDAOPDF2024
Band Standard Reference ContractPDF2023
SynonymPDF2023
Zivoe Locker ContractsPDF2023
Zivoe Core ContractsPDF2023
Hatom Liquid StakingPDF2023
Blockswap Stakehouse WithdrawalsPDF2023
HydraDX Withdrawal FeePDF2023
Galactic Skyteller v1PDF2023
OjoPDF2023
Gigastar Channel Revenue DistributionPDF2023
Galactic Skyteller Debit Card v0PDF2023
MorphoPDF2023
Proof of Neutrality NetworkPDFBlog PostModel2023
AshSwapPDFBlog Post2023
OptimismPDF2022
EigenLayer Design ReviewPDF2022
WorldMobileGroup OwnershipPDF2022
EUROe StablecoinPDF2022
Tinyman AMM v2PDFBlog Posthere2022
Hatom ProtocolPDF2022
HydraDX OmnipoolPDF2022
xBackedPDFBlog Post2022
Jpg.StorePDF2022
Pact.fi RouterPDFBlog Post2022
Blockswap Stakehouse, 2nd auditPDFBlog Post2022
Blockswap GatewayPDF2022
Swaap Labs PoolsPDFBlog Post2022
Quipuswap StableswapPDFBlog Post2022
HonePDFBlog Post2022
Gyroscope ProtocolPDFBlog Post2022
EXA FinancePDFBlot Post2022
Blockswap StakehousePDFBlog Post2022
Algofi AMM & NanoswapPDF2022
AtlendisPDFBlog Post2022
Folks Finance (Audit)PDFBlog Post2022
Folks Finance (Design)PDFBlog Post2022
Alchemix v2PDFBlog Post2022
Pact.fiPDFBlog Post2022
Pact.fi StableSwapPDFBlog Post2022
SundaeSwapPDF2022
Tinyman (Security Review)PDFBlog Post2022
Tracer Perpetual Pools V2PDF2021
Quipuswap TTDexPDFBlog PostGitHub2021
Stakefish Ethereum Staking 2.0PDFBlog Post2021
Algodex (phase 2)PDF2021
Algodex (phase 1)PDF2021
AlgofiPDFBlog Post2021
Yieldly Multi-Token Staking PoolPDFBlog Post2021
Element Finance GovernancePDFBlog Post2021
Algorand Governance RewardsPDFBlog Post2021
TinymanPDFBlog Post2021
Tezos Liquidity BakingPDFGitHub2021
XET ScriptPDFBlog Post2021
Tezos DexterPDFGitHub2021
Element FinancePDFBlog Post2021
StakerDAOPDF2021
StakeWisePDF2020
StakefishPDFBlog Post2020
Ethereum DepositPDFGitHub2019-2020
Polkadot ModuleGitHub2019-2020
GnosisSafePDFGitHub2019
Ethereum Casper (Deprecated)GitHub2018
Uniswap V1PDFGitHub2018
BihuPDFGitHub2018
ERC20 TokensGithub2017-2018

zkVM Design Security Audits

NameReportBlog PostArtifactYear
Zorp zkVM design reviewPDF2023

zkVM Formal Verification

NameReportBlog PostArtifactYear
zkEVM Formal Verification - KEVM <> EVM-YUL Lean EquivalenceReportklean, EVM Equivalence2025
zkEVM Formal Verification - REVM CorrectnessReportzkEVM Harness, RISC-V Semantics2025
Initial Plonky3 verification with HaxMilestone 1 - Part 1 (Hax) Milestone 1 - Part 2 (Hax) Milestone 2 (Hax)rust-lean repository2026
Initial Plonky3 verification with AeneasMilestone 3 (Aeneas)rust-lean repository2026

Formal Models and Language Semantics

Virtual Machines and Execution Environments

NameReportArtifactYear
EVMCSF'2018GitHub2016-Present
WASMGitHub2018-Present
MIRGitHub2022-Present
Soroban WASMGitHub2024-Present
RISC-VGitHub2024-Present
Elrond WASMGitHub2020-2024
IELEFM'2019GitHub2016-2021

Smart Contract Languages

NameReportArtifactYear
Tezos MichelsonGitHub2019-Present

Standard Specifications

NameReportArtifactYear
ERC777GitHub2018
ERC20GitHub2017