user2236: 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 b and c, a formal analysis of smart contract a requires formal analysis of contracts b and 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?

user6360: 
As a follow up, can/do smart contracts in the eUTxO model "call out"
to other smart contracts?

A smart contract (plutus script) can only be triggered by a transaction from a wallet.

Another follow up question, you say The interactions between the different > contracts are simpler and stateless

A Plutus script can see the whole transaction (all inputs of txn, all outputs, redeemer and datum). Arbitrary data (state) can be stored within the datum. But the context is restricted and so the only way the script can persist state or pass data (state) to another script is via a EUTxO which has a datum.

user6572: The interactions between the different contracts are simpler and stateless. In a stateful model like Ethereum's, you can have contract a call contract b and contract b call contract c, and then contract c can call back contract b while, at the same time, b is still waiting for contract c to answer. And during the calls, the state of each of the contracts may change.
So reasoning about this kind of interactions is more complicated than reasoning about pure predicates (functions that return a boolean value, like validators) that only depend on the contents of the transaction that is being validated. In other words, the computation that the different validators require does not produce side-effects that affect each other

2236: <p>I've heard that the eUTxO model is more amenable to static and formal analysis than the account model. If true, why is that?</p>
<p>I understand that the account model makes formal and static analysis difficult because of the nature of global state. For example, if smart contract <code>a</code> interacts with smart contracts <code>b</code> and <code>c</code>, a formal analysis of smart contract <code>a</code> requires formal analysis of contracts <code>b</code> and <code>c</code> (and all of their dependencies). Is that correct?</p>
<p>If the above is correct, don't similar ideas apply to the eUTxO model?</p>
<p>How exactly does the local nature of UTxOs make this model more amenable (if at all) to static and formal analysis?</p>
 6360: <blockquote>
<p>As a follow up, can/do smart contracts in the eUTxO model &quot;call out&quot;
to other smart contracts?</p>
</blockquote>
<p>A smart contract (plutus script) can only be triggered by a transaction from a wallet.</p>
<blockquote>
<p>Another follow up question, you say The interactions between the different &gt; contracts are simpler and stateless</p>
</blockquote>
<p>A Plutus script can see the whole transaction (all inputs of txn, all outputs, redeemer and datum). Arbitrary data (state) can be stored within the datum. But the context is restricted and so the only way the script can persist state or pass data (state) to another script is via a EUTxO which has a datum.</p>
 6572: <p>The interactions between the different contracts are simpler and stateless. In a stateful model like Ethereum's, you can have contract <code>a</code> call contract <code>b</code> and contract <code>b</code> call contract <code>c</code>, and then contract <code>c</code> can call back contract <code>b</code> while, at the same time, <code>b</code> is still waiting for contract <code>c</code> to answer. And during the calls, the state of each of the contracts may change.</p>
<p>So reasoning about this kind of interactions is more complicated than reasoning about pure predicates (functions that return a boolean value, like validators) that only depend on the contents of the transaction that is being validated. In other words, the computation that the different validators require does not produce side-effects that affect each other</p>
