Warning

This page was created from a pull request (#74).

Old Documentation

• Specification By Example
  • The Bank
  • The (Iterable) Map
• The Anatomy of a Specification
  • Overview
  • CVL Functions
  • Ghosts
  • Ghost Functions
  • Storage Hooks
  • Definitions
  • Multicontract Hooks
  • A Complete Example
  • Syntax Update: Ghost Variables and Ghost Mappings
• Advanced Subjects
  • Method declarations
  • Summarizing Solidity Functions
  • Internal Function Summaries
  • More Expressive Summaries
  • Multicontract
  • Linking Contracts
  • Approximation
  • Advanced Debugging
  • Grounding
• Best Practices
  • When to use the environment argument?
• Common Pitfalls
  • Vacuity
  • lastReverted updates
• Assert splitting
  • How the sub rules are generated
  • What if I have an assert command within an if-else statement
  • Report
• Troubleshooting
  • Timeouts
  • Errors
  • Understanding counter-examples