This article is based on reporting originally published at cryptonewsbytes.com in June 2019.
Why Smart Contract Verification Matters
Smart contracts are self-executing pieces of code deployed on a blockchain. Once deployed, they are immutable — you cannot patch them in the way you would a traditional web application — and their execution results are irreversible. Those two properties are a double-edged sword: they make smart contracts tamper-proof and trustworthy, but they also mean that bugs can have permanent, financially damaging consequences.
High-profile incidents such as the Ethereum DAO hack and the Parity wallet vulnerability demonstrated just how costly a single logic flaw in a smart contract can be. Because smart contracts are typically open source, any bug that exists in a deployed contract can be studied and exploited by malicious actors before the contract can be replaced.
Traditional software relies on a combination of unit testing, integration testing, and formal verification to catch bugs before they reach production. Smart contracts can benefit from the same discipline, but verification has historically been difficult to apply in this context.
The Challenge of Verifying Solidity Smart Contracts
Most Ethereum smart contracts are written in Solidity, a statically-typed language purpose-built for the Ethereum Virtual Machine (EVM). Formal verification of Solidity code requires deep knowledge of the language semantics, the EVM execution model, and formal methods — a combination of skills that is genuinely rare in the developer community.
Third-party smart contract auditing firms exist, but manual audits are time-consuming, expensive, and do not scale well as the number of contracts an organization deploys grows. An automated, developer-friendly verification tool would significantly lower the barrier to catching critical bugs early in the development lifecycle.
What Is VeriSol?
VeriSol — short for Verifier for Solidity — is an open-source formal verification tool developed by Microsoft Research. Its core workflow involves two steps:
- Translation: VeriSol translates a Solidity smart contract into Boogie, Microsoft Research’s formal intermediate verification language. Boogie provides a well-understood mathematical basis for reasoning about program behaviour.
- Verification: Developers specify the exact behaviour their contract should exhibit under given conditions (preconditions, postconditions, and invariants). VeriSol then mathematically checks whether the compiled Boogie representation actually satisfies those specifications. If it does not, it produces a counterexample that developers can use to locate the bug.
Smart contracts tend to have relatively small code bases compared to enterprise applications, which helps formal verification remain computationally tractable. The VeriSol team explicitly designed their tooling to take advantage of this characteristic in order to keep verification times practical.
VeriSol’s Integration into the Azure Blockchain Platform
Azure Blockchain Service is Microsoft’s managed Blockchain-as-a-Service (BaaS) offering. As of mid-2019, Microsoft announced that VeriSol had been integrated into the platform’s Continuous Integration / Continuous Delivery (CI/CD) pipeline. This is a significant step for developer ergonomics: rather than requiring teams to set up a separate verification environment, developers working within Azure Blockchain can invoke VeriSol as a standard step in their automated build and deployment workflow.
Embedding verification in CI/CD means that every time a smart contract change is committed, verification runs automatically alongside existing tests — catching specification violations before code ever reaches a deployed environment.
How VeriSol Fits into a Broader DevOps Workflow
For DevOps and platform engineering teams building on Azure Blockchain, VeriSol fits neatly into a defence-in-depth strategy for contract quality:
- Unit and integration tests catch runtime regressions and validate happy-path behaviour.
- VeriSol formal verification provides mathematical guarantees about contract invariants and state transitions — things that are difficult or impossible to cover exhaustively with tests alone.
- Manual audits (where budget allows) add human judgment, particularly for business-logic correctness and economic attack vectors.
No single approach catches everything, but layering verification into CI/CD shifts the cost of finding bugs left — catching them during development rather than after deployment, when fixes are no longer possible without deploying an entirely new contract.
Broader Industry Context
Microsoft’s investment in smart contract verification through VeriSol reflects a wider trend of established technology companies treating blockchain infrastructure as a serious engineering discipline rather than a speculative experiment. Tooling that makes formal verification accessible to everyday developers — not just academic researchers — is a meaningful contribution to the maturity of the ecosystem.
For engineering teams evaluating Blockchain-as-a-Service platforms, the availability of integrated verification tooling is a concrete differentiator worth assessing alongside more familiar criteria such as supported consensus mechanisms, SLA guarantees, and cost.
Further Reading
VeriSol is open source. You can find the repository and documentation on the Microsoft VeriSol GitHub page. The Boogie intermediate verification language is documented separately through Microsoft Research publications.