The smart contract language Solidity supports data areas for persistent and volatile data. Developing a deductive verification system for Solidity requires to formalize these areas. As we intend to allow users to interact directly with the proof object, the formalization must not only be efficient for the automated verifier, but also human-readable. We present here our approach towards such a formalization.