A formal model of Algorand smart contracts
This work provides a formal verification framework for Algorand smart contracts, which is incremental as it builds on existing blockchain and smart contract theory.
The authors developed a formal model for Algorand stateless smart contracts to prove fundamental blockchain properties and establish security for archetypal contracts, validating the model's coherence with the actual implementation through experiments.
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.