[pron]

Temporal logic verification (via model checking, static analysis, test generation, runtime checks etc.)?

[fsantanna]

That would be interesting.

It seems to be feasible given the language semantics.

We'll definitely investigate it.