program 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

[monperrus]

solc-verify: A Modular Verifier for Solidity Smart Contracts 2019

Tool: https://github.com/SRI-CSL/solidity

[MaryemHadjWannes]

Hi @monperrus, I’m trying to use the VerX client script to verify a Solidity contract. but I’m not sure how to obtain a username and password. Is this information available to all users, or is it restricted to certain members?

[monperrus]

don't know, this is not the official repo of VerX. best regards, --Martin

[monperrus]

Design and Implementation of Static Analyses for Tezos Smart Contracts
https://dl.acm.org/doi/pdf/10.1145/3643567

[monperrus]

Deductive verification of smart contracts with Dafny
http://link.springer.com/10.1007/s10009-024-00738-1

we do not yet have a compiler from Dafny to Ethereum Virtual Machine bytecode

[monperrus]

Towards benchmarking of Solidity verification tools
https://arxiv.org/pdf/2402.10750

compares SolCMC and Certora

[monperrus]

Solvent: liquidity verification of smart contracts
https://arxiv.org/pdf/2404.17864

[monperrus]

Practical Verification of Smart Contracts using Memory Splitting
https://abakst.github.io/oopsla24.pdf

[monperrus]

Kontrol
https://docs.runtimeverification.com/kontrol
https://github.com/runtimeverification/kontrol