{"id":590746,"date":"2019-06-03T08:20:06","date_gmt":"2019-06-03T15:20:06","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-project&#038;p=590746"},"modified":"2019-06-03T08:34:59","modified_gmt":"2019-06-03T15:34:59","slug":"verisol-a-formal-verifier-for-solidity-based-smart-contracts","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/verisol-a-formal-verifier-for-solidity-based-smart-contracts\/","title":{"rendered":"VeriSol: A formal verifier for Solidity based smart contracts"},"content":{"rendered":"<p>Ensuring correctness of smart contracts is paramount to ensuring trust in blockchain-based systems. VeriSol (Verifier for Solidity) is a project for advancing the state-of-the-art in formal specification and verification of blockchain smart contracts, with the goal of bringing the technology to smart contract developers. It is based on translating programs in <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/solidity.readthedocs.io\/\" rel=\"nofollow\">Solidity<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> language to programs in <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/boogie-org\/boogie\">Boogie<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> formal intermediate verification language, and then leveraging and extending the verification toolchain for Boogie programs.<\/p>\n<p>VeriSol is an open-source project on <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/Microsoft\/verisol\">GitHub<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Ensuring correctness of smart contracts is paramount to ensuring trust in blockchain-based systems. VeriSol (Verifier for Solidity) is a project for advancing the state-of-the-art in formal specification and verification of blockchain smart contracts, with the goal of bringing the technology to smart contract developers. It is based on translating programs in Solidity language to programs [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-590746","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2019-04-15","related-publications":[589459,606990,683523,738607,805813],"related-downloads":[],"related-videos":[],"related-groups":[144812],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Shuvendu Lahiri","user_id":33640,"people_section":"Section name 1","alias":"shuvendu"},{"type":"user_nicename","display_name":"Shuo Chen","user_id":33637,"people_section":"Section name 1","alias":"shuochen"}],"msr_research_lab":[199560],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/590746"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":7,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/590746\/revisions"}],"predecessor-version":[{"id":590776,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/590746\/revisions\/590776"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=590746"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=590746"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=590746"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=590746"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=590746"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}