5. Minimize Verification Code🔗

To achieve goal (4), minimize the amount of user code needed to enable verification, Laurel has the following features:

1. 5.1. Transparent procedures
2. 5.2. Heap mutation in contracts
3. 5.3. Aliasing helpers
4. 5.4. Invoke on