---
# System prepended metadata

title: 'Open Discussion: ACTing formal - Formal Verification & Solidity'

---

# 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).