Open monperrus opened 1 year ago
The Certora Verification Language (often abbreviated CVL) isa language used to write specifications for smart contracts.:
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/
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
Manticore is a symbolic execution tool for the analysis of smart contracts and binaries. https://github.com/trailofbits/manticore
Evolution of Automated Weakness Detection in Ethereum Bytecode: a Comprehensive Study. http://arxiv.org/abs/2303.10517
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
Awesome testing tools for Web3 and Blockchain https://github.com/TheJambo/awesome-testing#web3-and-blockchain
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):
(written in Java)
End-to-End Formal Verification of Ethereum 2.0 Deposit Contract in K (staking) https://github.com/runtimeverification/deposit-contract-verification
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?
don't know, this is not the official repo of VerX. best regards, --Martin
Design and Implementation of Static Analyses for Tezos Smart Contracts https://dl.acm.org/doi/pdf/10.1145/3643567
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
Towards benchmarking of Solidity verification tools https://arxiv.org/pdf/2402.10750
compares SolCMC and Certora
Solvent: liquidity verification of smart contracts https://arxiv.org/pdf/2404.17864
Surveys:
A Survey of Smart Contract Formal Specification and Verification. ACM Comput. Surv. 2022
Awesome: