You can't talk about JavaScript formal analysis for security without mentioning Mark Miller's amazing work here: http://www-cs-students.stanford.edu/~ataly/Pape

You can't talk about JavaScript formal analysis for security without mentioning Mark Miller's amazing work here: http://www-cs-students.stanford.edu/~ataly/Papers/sp11.pdf http://www-cs-students.stanford.edu/~ataly/Papers/sp11.pdf Here, not only does he built a secure subset of JavaScript and _prove_ it's tamper safe using formal logic, Mark also finds exploits with the same method in high end tamper filters like Yahoo's. Definitely impressive use of formal logic in language analysis.