This file used in projects to lay out the protocol's properties and invariants. It also serves as a documentation for test coverage.