Read and Write
The verifier uses a read/write permission model to track access to actor fields and mutable heap locations.
Permission Errors
Understanding and fixing "missing permission" failures.
Framing and Permissions
How reads and modifies clauses translate into verification permissions that enable automatic framing.