Additional Concepts In CVL (Certora Verification Language)

• Go over the following sources of free and public information to learn how to think of systems as state machines:

  • Part of a lecture explaining the idea of state machines¹. Watch the video from 48:58 to 1:02:45 - Link

  • A recitation on state machines for the same course¹ - Link.

  • A short written explanation on state machines - Link

📝 If you feel you need some more explanations of the subject you can search the web for many additional great and free sources.

• Follow the instructions on Methods_Definitions_Functions to learn about method declarations, definitions, and functions in CVL, and exercise the concepts.

• Read the documentation on Types and Type Handling to learn about the different CVL types available to use, their distinction from EVM types, casting operations, and useful macros.

---

Useful flags

• Continue to the next lesson: Getting Familiar With CVT to learn about additional flags that you can use for your benefit.

---

"Programs must be written for people to read, and only incidentally for machines to execute.“ - Hal Abelson

---

Footnotes

1. The content was created for the course Introduction to Electrical Engineering and Computer Science for MIT University (OCW). ↩ ↩²