Tezos was created first and foremost to address a governance issue in decentralized cryptographic ledgers. It does so by allowing stakeholders to approve updates to the protocol, including the consensus algorithm, and the governance rule themselves. Tezos is written in OCaml (a functional programming language) and rely on Coq for advanced proof checking and formal verification. Source code will be opened and available later this year.
Arthur Breitman of "Tezos" gave this presentation on this new technology on Wednesday, August 31st at Monetas HQ (Zug – Switzerland)