Laurel User Guide

9. Debugging and tooling🔗

A verification failure has more possible causes than a compile error: the program may be wrong, the specification may be wrong, or the specification may be right but out of the solver's reach. This section is about telling those apart.

  1. 9.1. Running a program
  2. 9.2. Seeing what the compiler did
  3. 9.3. Useful verification flags
  4. 9.4. A debugging order
  5. 9.5. Exit statuses
  6. 9.6. The Lean API