SecTeal (Secure Teal) is the programming language for Algorand stateless smart contracts (stateless ASC1) derived from the formal model of Algorand presented in [OMITTED]. The model abstracts stateless smart contracts by means of a language of expressions that evaluate to true or false.
Such an interpretation enables a natural interpretation of the semantics of a smart contract in Algorand, whose evaluation reverts to true or false, consequently authorising or refusing a transaction in the Algorand blockchain.
Such abstract approach lends itself to both express contracts' intended behaviour in a simple, logical way, and support formal verification of contracts' properties.
This page provides a compiler from SecTeal to Teal, the native, layer-one, smart contract language of Algorand.
This is part of an ongoing research effort aiming to develop general formal verification of smart contracts, with Algorand as a case study.
SecTeal language (grammar). This is an experimental prototype that works on strict syntactic rules dictating how you need to write your smart contracts. The following grammar defines the expression accepted by the compiler (spaces must be respected):exp ::= val a value
 M. Bartoletti, A. Bracciali, C. Lepore, A. Scalas, R. Zunino “A formal model of Algorand smart contracts”. In N. Borisov and C. Diaz (eds) Proceedings of 25th International Conference on Financial Cryptography and Data Security 2021. March, 1-5, 2021, Online. Lecture Notes in Computer Science, Springer, 2021. To appear. (preliminary version at https://arxiv.org/abs/2009.12140".
Insert your contract as an expression from the grammar exp on a single line, respecting space rules (see examples) and press Compile (see text in the box as an example). You will get the Teal (executable) code corresponding to your SecTeal contract.
USE AT YOUR OWN RISK! still an under dev prototype.