Why Don't People Use Formal Methods?(hillelwayne.com)

    description "Admin (and only admin) can set new admin" {
      // e0, e1 can hold any possible environment and are ordered sequentially
      env e0; env e1;

      // free variable for possible values of new admin
      address nextAdmin;
      havoc nextAdmin;
  
      // call to set the new admin
      invoke setAdmin(e0, nextAdmin);

      // assert one of two conditionals must hold for all cases:
      // 1. We were the admin and the next admin is what we sent to `setAdmin()`
      // or 2. We were not the admin, and the next admin is whatever is was before our call to `setAdmin()`.
      static_assert (
        e0.sender == invoke admin(e0) &&
        invoke admin(e1) == nextAdmin
      ) || (
        e0.sender != invoke admin(e0) &&
        invoke admin(e1) == invoke admin(e0)
      );
    }