[racket] Specification Language

I think you need to characterize the kinds of vulnerabilities you're 
looking for, and then relate that characterization to the semantics of 
the language about which you're reasoning.

I suspect that what you're doing is actually a research area for people 
who understand both vulnerabilities and programming languages very 
well.  So, if you don't already have that entire foundation, you might 
understand the problem much better after you fill any holes in your 
foundation.