Ethereum, the market’s leading altcoin, is currently one of the most-trusted cryptocurrencies and blockchain technologies. Leading businesses such as Facebook, JP Morgan and E&Y have all released open-source software for Ethereum, signalling a strong inclination towards Vitalik Buterin’s brainchild. One of the Goliaths consistently involved with crypto technologies such as Ethereum and Bitcoin is Microsoft. The software giant shared an official blog post announcing the release of an open-source formal verification tool for Solidity smart contracts.
Solidity, an Ethereum-powered programming language used to write smart contracts on a blockchain environment. The driver behind the project seems to aimed at exploiting the potential of blockchain technology to save loss of millions of dollars in cryptocurrency. Microsoft’s post also highlighted some recent attacks such as the DAO exploit and the Parity wallet bug, which could be avoided by deploying a blockchain infrastructure.
Although Microsoft Azure’s Blockchain leader, Marley Gray, gained negative publicity after his old views on Bitcoin resurfaced, the blog shared his team’s involvement in implementing proof-of-concept solutions with Azure Blockchain Workbench. Furthermore, Microsoft had recently announced working on a project which involves creating a Decentralized Identity Tool on the Bitcoin blockchain. The leading technology company’s Principal Researcher, Shuvendu Lahiri, expanded on smart contracts’ clear advantages over Microsoft’s formal verification techniques.
Powering the technology is Verisol, which is built based on Microsoft’s decade of work in verification as part of the company’s larger commitment to security, user experience, and high-quality, state-of-the-art products and services. VeriSol operates by encoding the semantics of Solidity programs to perform high-coverage symbolic testing for finding counterexample traces.
Source: MicrosoftWhile Verisol formal verification tool is designed to improve the quality of smart contracts, the company is investing in improving automation in inferring common inductive invariant to reduce manual overhead for performing correctness proofs.
As a conclusion to the post, Lahiri said,
“We envision empowering not just Azure Blockchain developers and customers, but contributing to a full blockchain ecosystem that is safer and helping people realize the full potential of the technology without being plagued by the costly mistakes in smart contracts.”
Subscribe to AMBCrypto’s Newsletter