Formal tooling for Algorand’s smart contract architecture

The project includes:

1. Developing formal semantis of TEAL, Algorand’s L1 smart contracts language, and deriving formal analysis tools for TEAL programs
2. 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
3. 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.