Record types are typically used to represent mathematical types. As such, they typically require some qualification to me be meaningful. A typical example is a permutation type, giving forward and backward maps, with the requirement that the two maps are inverses. Today, such requirements have to be stated as an external property of the record. This is inconvenient for several reasons:

• Every time such a record is passed in/out a function or updated in a loop, the requirement has to be stated as an explicit precondition/postcondition/invariant.
• When a record type with an implicit invariant is used as a domain of a map, the map gets the wrong definition of equality: two maps should be the same if they agree on inputs satisfying the record invariant, instead of having to agree on "garbage" inputs also.
  

The proper solution to this is to just allow record types to have (single-state) invariants. To deal with initialization, we would allow record types to define initializers (and perhaps define default initializers), and part of the verification of a record type should be to check that the initial value satisfies the invariant. Record update expressions undergo an invariant check. We could also conceivably allow atomic record updates within _(ghost_atomic), but it probably isn't necessary.