# Solc-verify, a source-level formal verification tool for Solidity smart contracts by Akos Hajdu

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2020-10-09
- Duration: 30:14
- Topics: blockchain, smart contracts, distributed ledger, ethereum, ethereum solidity, solidity, solidity summit, language design
- Watch: https://streameth.org/watch/yt-1q2gSm3NuQA
- YouTube: https://www.youtube.com/watch?v=1q2gSm3NuQA

## Description

Solc-verify is a source-level formal verification tool for Soldity smart contracts, developed in collaboration with SRI International. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code. This enables solc-verify to effectively reason about high-level functional properties while modeling low-level language semantics (e.g., the memory model) precisely. The contract properties, such as contract invariants, loop invariants, function pre- and post-conditions and fine grained access control can be provided as in-code annotations by the developer. This enables automated, yet user-friendly formal verification for smart contracts.