I was trying some examples from Certora’s demo website, and I was getting errors due to syntax change in CVL 2. I wondered how does it still work on the demo website, most probably because it doesn’t run every time. Then I thought it would be great to have CVL version number in spec files, like Solidity. Then I found pragma specify xxx, and I was happy! Then I say this in the docs:
CVL 1 had a pragma command for specifying the CVL version, but this feature was not used and has been removed in CVL 2.
I believe having CVL version in the files can help the files work over time, without the need to update it every time, which might be nontrivial due to breaking changes. It also helps you keep a repository of Examples that works all the time. I bet most of the examples in the current docs will not work as is, but if they had pragma specify 1.0 they would. Of course this means keeping different versions of the tool, but it can be managed the same way that Solidity compiler is managed.