microsoft
/
verisol
зеркало из https://github.com/microsoft/verisol.git
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность
A formal verifier and analysis tool for Solidity Smart Contracts
869 коммитов 14 Ветки 0 Теги 4,5 MiB
C# 58.6%
Solidity 38.1%
Boogie 3%
Batchfile 0.2%
Perl 0.1%
Перейти к файлу
Shuvendu Lahiri 4357a18b73
Merge pull request #276 from microsoft/users/GitHubPolicyService/c9f088c0-051f-419c-ac4e-d0c2bb415633 
Adding Microsoft SECURITY.MD
 		2022-08-31 11:23:19 -07:00
Docs slides 2019-11-24 23:55:27 -08:00
Sources Merge branch 'master' into ellab-exception 2020-05-27 14:48:30 -07:00
Test missing json file for regression 2020-04-16 17:38:19 -07:00
.gitattributes misc(.gitattributes): .sol register as Solidity file 2020-05-13 16:56:57 +08:00
.gitignore Fix building issue 2019-09-17 15:17:11 -07:00
INSTALL.md Merge branch 'master' into ellab-exception 2020-05-27 14:48:30 -07:00
LICENSE.txt Fix building issue 2019-09-17 15:17:11 -07:00
README.md Update README.md 2022-06-02 15:01:01 -07:00
SECURITY.md Microsoft mandatory file 2022-08-31 15:20:32 +00:00
azure-pipelines.yml bump up VeriSol version to 0.1.5-alpha; last merge '69a51b1 3c39efb' 2020-05-26 17:12:16 -07:00

README.md

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 opencode@microsoft.com with any additional questions or comments.