It would be cool to have a section on verification features, explaining how the verification works for different features like method invocation, if stetatements, recursion, etc