The project includes:
- Developing formal semantis of TEAL, Algorand’s L1 smart contracts language, and deriving formal analysis tools for TEAL programs
- Developing a formal specification of a L2 smart contract language and generating an efficient interpreter for the language to be integrated with the smart contract architecture
- Developing a formal specification of an L2-to-L1 compiler of a subset of the L2 language for automatically generating predicates that can be checked at L1.
More information with pointers will be available later.