+Formal verification is a complicated process, made even more arduous for smart contracts by the lack of a common baseline of desirable properties one might want to prove. Our work aims to address this by providing some universally desirable properties that generalize well. We also provide a framework with which one can prove these properties in Agda for a validator that can be subsequently exported directly as Haskell and put on the blockchain. This process can also handle token minting policies and has been separately linked to the official Formal Ledger Specification.
0 commit comments