TL;DR
This paper presents a formal model of Algorand's stateless smart contracts, enabling proofs of blockchain properties, security guarantees, and validation against real implementations.
Contribution
It introduces a formal model for Algorand smart contracts and uses it to prove blockchain properties and security, highlighting supported design patterns.
Findings
Proven fundamental properties of Algorand blockchain.
Validated the model's coherence with actual implementation.
Established security of archetypal smart contracts.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
