"Formal verification" has appeared in various previous questions and answers, and I believe was the topic for one of the talks at DevCon2.
Main question: It's perhaps quite broad, but what is formal verification in the context of Ethereum, and why do we need it for smart contracts?
- Is it something that's already implemented and part of the ecosystem, or is it something that will be implemented in future?
- How is formal verification different to the inherent determinism of the language a smart contract is written in? (See Why do smart contract languages need to be deterministic?)