Tezos offers a platform to create smart contracts and build decentralized applications that cannot be censored or shut-down by third parties. Furthermore, Tezos facilitates formal verification, a technique used to improve security by mathematically proving properties about programs such as smart contracts. This technique, if used properly, can help avoid costly bugs and the contentious debates that follow.
Tezos has several popular high-level languages which offer more approachable syntaxes and familiar developer experience (e.g. local variables) compared to writing Michelson directly. SmartPy and LIGO are the most popular and widely-supported languages for writing Tezos smart contracts.