# Open Discussion: ACTing formal - Formal Verification & Solidity *These are collaborative notes from the open discussion round about "ACTing formal - Formal Verification & Solidity" at the [Solidity Summit 2020](https://solidity-summit.ethereum.org/).* ## Assertions 1. static_assert ```solidity // This does NOT become part of the bytecode, by default. static_assert(f(x+@ == g(x-3))) ``` 2. special comments with proper Solidity expressions ```solidity /// @assert f(x+2) == g(x-3) ``` 3. non-comment annotations ```solidity @assert(f(x+2 == g(x-3))) [[assert f(x+2 == g(x-3))]] ``` ## Contract inductive invariants 1. Could work just like the `assert` annotation. 2. Needs to be enforced only at the external call boundaries (i.e. might temporarily not hold while a function is being called internally).