Tutorial is made for CVL1 and needs to be updated to CVL2.

[hake-stake]

Running this script solved the issue for me.

However, having beginners to go through this process is counter productive.

Please update the repo with updated specs.

[twicek]

This problem can be partially solved by changing the methods definition:

methods {
    // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
    balanceOf(address)         returns(uint) envfree
    allowance(address,address) returns(uint) envfree
    totalSupply()              returns(uint) envfree
}

To this:

methods {
    // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
    function balanceOf(address) external returns(uint) envfree;
    function allowance(address,address) external returns(uint) envfree;
    function totalSupply() external returns(uint) envfree;
}

This change allows at least to do ERC20Lesson1.

Reference in docs: https://docs.certora.com/en/latest/docs/cvl/cvl2/changes.html#superficial-syntax-changes