Covenant - modern programming language for blockchains - it's a functional, statically-typed language with formal verification features