Skip to content

A formal verifier and analysis tool for Solidity Smart Contracts

License

Notifications You must be signed in to change notification settings

microsoft/verisol

Repository files navigation

We are no longer actively maintaining the tool as of 2021

Build Status

VeriSol

VeriSol (Verifier for Solidity) is a Microsoft Research project for prototyping a formal verification and analysis system for smart contracts developed in the popular Solidity programming language. It is based on translating programs in Solidity language to programs in Boogie intermediate verification language, and then leveraging and extending the verification toolchain for Boogie programs. The following blog provides a high-level overview of the initial goals or VeriSol.

The following paper describes the design of VeriSol and application of smart contract verification for Azure Blockchain:

Formal Specification and Verification of Smart Contracts for Azure Blockchain, Yuepeng Wang, Shuvendu K. Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer, https://arxiv.org/abs/1812.08829

INSTALL

Instructions for installing and running VeriSol can be found here.

VeriSol Code Contracts library

The code contract library VeriSolContracts.sol is present here. This allows adding specifications in the form of pre/post conditions, loop invariants, contract invariants, modifies clauses, and extending the assertion language with constructs such as old, sum, etc.

License

VeriSol is licensed under the MIT license.

Contributing

This project welcomes contributions and suggestions. Most contributions require you to agree to a Contributor License Agreement (CLA) declaring that you have the right to, and actually do, grant us the rights to use your contribution. For details, visit https://cla.microsoft.com.

When you submit a pull request, a CLA-bot will automatically determine whether you need to provide a CLA and decorate the PR appropriately (e.g., label, comment). Simply follow the instructions provided by the bot. You will only need to do this once across all repos using our CLA.

This project has adopted the Microsoft Open Source Code of Conduct. For more information see the Code of Conduct FAQ or contact [email protected] with any additional questions or comments.

About

A formal verifier and analysis tool for Solidity Smart Contracts

Resources

License

Code of conduct

Security policy

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published