Versions Compared


  • This line was added.
  • This line was removed.
  • Formatting was changed.


    1. ✔️ indicatesthe rule is formally verified on the latest commit.

    2. We write ✔️* when the rule was verified on a simplified version of the code (or under some assumptions). 

    3. ✔️x indicates that the rule was violated at some version of the code.

  1. (blue star) indicates the rule was violated under the current tested version of the code.

  2. ✍ indicates the rule is not yet formally specified.

  3. 🔁 indicates the rule is postponed (<due to other issue, low priority?>) .

  4. We use Hoare triples of the form {p} C {q}, which means that if the execution of program C starts in any state satisfying p, it will end in a state satisfying q. In Solidity, p is similar to require, and q is similar to assert.