Program verification is recognised as crucial in the Tezos community since the very beginning of the Tezos project. It is mentioned in the position and white papers and many teams work on this topic. Smart contract verification in particular is a key aspect in the design of the Tezos smart contract languages (Michelson and the various high-level languages).
In layman's terms what does it mean when it is said that a smart contract is verified? Does it mean there are no bugs?
It means that, with the highest degree of certitude that we can have about a mathematical result, we know that the smart contract behaves exactly as its specification says it does. This is a much stronger statement than "the smart contract is well tested" but it does not exactly mean that there are no bugs because the notion of "bug" cannot be precisely defined.
And are formal proofs and verification the same thing?
More or less. The notion of formal proofs is more general because it applies to all mathematical statements, not only the correctness of programs. However large proofs of mathematical statements that may seem unrelated to programming actually rely on program verification (a good example of this is the Coq proof of the 4-colour theorem).
Is programmatic testing not enough? What does it offer beyond unit tests?
The difference between testing and verification is that verification is exhaustive. When verifying a program we reason about all possible executions of the program, whereas testing is limited to a final number of executions.
What is the verification process?
This is hard to summarize because there are various approaches but the general idea is that we write both a program (in some programming language) and a specification (a formula describing what the program is intended to do) and we want a verification system to check that both agree. The verification system knows the semantics of the programming language (what it means to execute programs written in this language) but that is usually not enough to check that the program satisfies its specification so an expert is needed to guide the verification system (by writing a proof script or by adding annotations on the program).
Are there any contracts verified on Tezos?
Yes. Most notably the Dexter decentralized exchange. I gave a presentation on this topic for the second Nomadic Labs Research Seminar.
