Imandra does interesting work on using SMT-based verification for testing and auditing complex models. Grant Passmore, co founder, got his PhD at university of Edinburgh and gave a talk today.
One of key points I got from his talk here is that most applications can be neatly stacked into layers, which by itself is not surprising, but that lower layers tend to be high frequency IO, but then at the higher level of abstractions there is low frequency interaction, which is usually human driven. A verification tool is perhaps best placed by acting in between these extremes.
I like their punchline: reasoning as a service.
PS In financial trading there is a specification of when the trading happens, but this specification is often given in 100+ page document. And instructions for executing against that specification looks very logical, eg do X subject to Y provided there is Z left in resources.
PPS A previous lab member Lewis Hammond interned at imandra a couple of years ago.