[TYPES] Query: Types for post-development analysis?

[Michael Anthony Smith]

I have been a (silent) member of the types list for several years, as I 
am interested in monitoring (and hopefully using) developments in type 
theory. I certainly make use of (reasonably) strongly types 
specification and programming languages in my work, which is regularly 
involving the analysis of third party designs/code. Within this context 
it is often hard to use developments in the type-theory, as they appear 
(at least to me) to be aimed at designing solid development languages 
and frameworks.

I know that type systems are used to design languages (and frameworks) 
that have a given collection of desirable properties, whether this be 
the traditional "shape" correctness or for some other concern such as 
guaranteeing various concurrency or security properties. I also am aware 
of the link between type theories and abstract interpretation. What I 
was wondering if anyone here knows of the application of type theories 
to the post-development analysis context?

Thanks,

Anthony.