Move fast, break nothing.

contract ERC20 is IERC20, IERC20Metadata {
...
    function transferFrom(address from, address to, uint256 value) public virtual returns (bool) {
        _spendAllowance(from, msg.sender, value);
        _transfer(from, to, value);
        return true;
    }
...

// Checks that transferFrom() decreases allowance of `e.msg.sender`

rule checkTransferFrom(address sender, address recipient, uint256 amount) {
    env e; // represents global variables like msg.sender
    require sender != recipient && amount > 0;

    uint256 allowanceBefore = allowance(sender, e.msg.sender);
    transferFrom(e, sender, recipient, amount);
    uint256 allowanceAfter = allowance(sender, e.msg.sender);
    
    assert (allowanceBefore > allowanceAfter),
        "allowance must decrease..."; // error message 
}