I've heard that the eUTxO model is more amenable to static and formal analysis than the account model. If true, why is that?
I understand that the account model makes formal and static analysis difficult because of the nature of global state. For example, if smart contract
a interacts with smart contracts
c, a formal analysis of smart contract
a requires formal analysis of contracts
c (and all of their dependencies). Is that correct?
If the above is correct, don't similar ideas apply to the eUTxO model?
How exactly does the local nature of UTxOs make this model more amenable (if at all) to static and formal analysis?