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 (opens in new tab) language to programs in Boogie (opens in new tab) formal intermediate verification language, and then leveraging and extending the verification toolchain for Boogie programs.
VeriSol is an open-source project on GitHub (opens in new tab).