There's also the "Featherweight Firefox" browser model in Coq http://www.the-inconsistency-principle.com/upenn//browser-mo...