> This takes a language's semantics, i.e. how to evaluate each sort of expression, and extends it to include extra information which can represent time taken, memory usage, cache usage, etc.

This simply says that functional languages could be assigned cost semantics, just like imperative languages have, and so may be used for algorithm analysis. It has nothing to do with verification.

> tracking gas

Yep, but that's a trivial property that could be done by any runtime. It doesn't help prove any other correctness property.