Let’s examine the modal logic of thin client proofs in Bitcoin and in Ethereum.
In Bitcoin, an SPV proof contains the merkle path to a transaction. You can prove that a UTXO is necessarily-spent by giving the path to a transaction which has spent it.
You can also prove that any one of its UTXOs are possibly-unspent by giving the path to the transaction it is a part of. But this does not prove that it is necessarily-unspent. There could be another transaction which has spent this output, which would appear in the merkle tree of a later block (or even later in the same block).
Even if you are willing to download the entire UTXO set from a full node, there is no way to prove that it is accurate. A proof would require downloading and replaying the entire transaction history - in other words, becoming a full node.
The only way to prove that a UTXO is necessarily-unspent, is to spend it. More accurately, this proves that it was necessarily-unspent. By generating this proof you have made it necessarily-spent.
So to a thin client, “is this output spent” is not a simple boolean true/false, it is a modal boolean with orientation necessarily-true/possibly-false (necessarily-spent/possibly-unspent).
The practical impact of this is that checking for 0conf double-spends requires trust. In practice, the nodes (miners) will not be the ones lying, it will be intermediate infrastructure that might be exploited for this attack vector. And in practice, the solution is to simply wait for a confirmation for high-value transactions, whether it be a transfer or a state transition in L2.
Let’s compare to the EVM. Although the EVM does not use the UTXO model, we can draw a comparison to a strictly-decreasing state variable (decreasing to help us imagine “spending”). Proving “unspent” is analagous to proving the state variable hasn’t changed, while proving “spent” is analagous to proving that the state variable has been decremented.
EVM state proofs are given in the form of a merkle-patricia trie, which is basically a merkle tree that can support arbitrary strings as keys (rather than simple consecutive indices like a regular merkle tree). The form of the proof is the same for both “changed” and “unchanged”, as we are just querying the state. The proof is the path to the state variable of interest in the MPT given at the latest block header.
At first glance this appears to give us a concrete boolean: We can prove both “necessarily spent” and also “necessarily unspent”. But “necessarily unspent” is only true as of the block height of the proof! There is no proof that the state was not decremented since that last state.
So in reality Ethereum still gives us “necessarily spent” versus “possibly unspent” in the thin client. It just gives us an additional “necessarily-unspent as of block N”.
State in Ethereum is valuable because it allows composing building blocks that are not aware of each other a priori in a fill-or-kill manner. As far as off-chain systems are concerned, the fact that the latest state proof can be updated frequently is a comforting misdirection. From the point of view of an attacker, 10 seconds is plenty of time.
In both UTXO and MPT state models, your system should be architected so that off-chain ‘latest state’ logic requires an on-chain confirmation.