formal verification of smart contracts

[monperrus]

Surveys:

A Survey of Smart Contract Formal Specification and Verification. ACM Comput. Surv. 2022

Awesome:

• https://github.com/leonardoalt/ethereum_formal_verification_overview

[monperrus]

The Certora Verification Language (often abbreviated CVL) isa language used to write specifications for smart contracts.:

• https://pypi.org/project/certora-cli/
• https://docs.certora.com/en/latest/docs/cvl/index.html
• https://demo.certora.com/
• http://wayback.archive.org/https://www.certora.com/pubs/QuickGuide.pdf

[monperrus]

Cairo is a programming language for writing provable programs, where one party can prove to another that a certain computation was executed correctly.
https://www.cairo-lang.org/

[monperrus]

Pluto: Exposing Vulnerabilities in Inter-Contract Scenarios

[monperrus]

https://github.com/crytic/slither a static analyzer avaialable through a CLI and scriptable interface.

resources: https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/slither

[monperrus]

Manticore is a symbolic execution tool for the analysis of smart contracts and binaries.
https://github.com/trailofbits/manticore

[bbaudry]

Evolution of Automated Weakness Detection in Ethereum Bytecode: a Comprehensive Study.
http://arxiv.org/abs/2303.10517

[monperrus]

Our public audits contain examples of verified or tested properties. Consider reading the Automated Testing and Verification sections of the following reports to review real-world security properties:

https://github.com/crytic/building-secure-contracts/tree/master/program-analysis

[bbaudry]

Awesome testing tools for Web3 and Blockchain
https://github.com/TheJambo/awesome-testing#web3-and-blockchain

[monperrus]

A Survey of Smart Contract Formal Specification and Verification. ACM Comput. Surv. 2022

[monperrus]

The K Framework is a tool for designing and modeling programming languages and software/hardware systems
https://github.com/runtimeverification/k

K Semantics of the Ethereum Virtual Machine (EVM):

• paper https://daejunpark.github.io/kevm.pdf
• tool https://github.com/runtimeverification/evm-semantics

(written in Java)

[monperrus]

End-to-End Formal Verification of Ethereum 2.0 Deposit Contract in K (staking)
https://github.com/runtimeverification/deposit-contract-verification

[monperrus]

Verx: Safety verification of smart contracts 2020

[monperrus]

ethor: Practical and provably sound static analysis of ethereum smart contracts 2020