Sample contracts you can test Echidna with

pausable.sol

contract Ownable {
    address owner;

    constructor() {
         owner = msg.sender;
     }
     modifier onlyOwner() {
         require(owner == msg.sender);
         _;
    }

    function renounceOwnership() onlyOwner public {
        delete owner;
    }
}

contract Pausable is Ownable {
    bool isPaused;

    modifier ifNotPaused(){
            require(!isPaused);
            _;
    }

    modifier ifPaused(){
            require(isPaused);
            _;
    }

    function pause() onlyOwner public {
        isPaused = true;
    }

    function unpause() ifPaused public {
        isPaused = false;
    }
}


// Test the scenario of decomissioning a contract
contract EchidnaTest is Pausable {

    constructor() {
        pause(); // final pause
        owner = address(0); // renounce ownership
    }

    // define invariant
    function echidna_CheckPauseIsFinal() public view returns(bool){
        return isPaused == true;
    }
}

token.sol

pragma solidity ^0.7.6;

contract Token {
    mapping(address => uint) public balances;
    
    function transfer(address to, uint value) public {
        balances[msg.sender] -= value;
        balances[to] += value;
    }
}

contract EchidnaTest is Token {
    address echidna_caller = 0x00a329C0648769a73afAC7F9381e08fb43DBEA70;

    constructor() {
        balances[echidna_caller] = 10000;
    }

    // add the property
    function echidna_test_balance() view public returns(bool){
        return balances[echidna_caller] <= 10000;
    }
}

echidna-test pausable.sol --contract EchidnaTest

echidna-test token.sol --contract EchidnaTest