  We develop a formal model of Algorand stateless smart contracts (stateless
ASC1.) We exploit our model to prove fundamental properties of the Algorand
blockchain, and to establish the security of some archetypal smart contracts.
While doing this, we highlight various design patterns supported by Algorand.
We perform experiments to validate the coherence of our formal model w.r.t. the
actual implementation.
