In its blog, Microsoft announced the development of an open formal verification scheme for smart Ethereum contracts in the Solidity programming language.
The tool will be called VeriSol (Verifier for Solidity) – it will allow developers to write specifications for smart contracts, which can then be tested using mathematical logic. The Microsoft blog says that the VeriSol team will use the verifier to formally verify the specifications of smart contracts that guide the members of the Ethereum consortium in Azure and the Azure Blockchain Service.
Formal verification of a smart Ethereum contract should ensure their security, which has long been a problem for smart contracts, as evidenced by several major hacks. Validation provides developers with a protocol to check the security of critical components of a smart contract.
The leading researcher at Microsoft, Shuvendu Lahiri, says that the verification process now takes a lot of time, but smart contracts have certain properties that allow them to be formally verified: and an open operating environment significantly reduces the need to manually simulate the environment in which a smart contract operates, ”he said.
VeriSol will complement the Microsoft Azure Blockchain development toolkit.
Recall that Microsoft recently announced that it will use the bitcoin blockchain to create a system of reliable digital identification, and an option with a bitcoin symbol has been added to Microsoft Excel.
