In this talk, Matteo Maffei will give an overview on this research line, illustrating how formal methods can positively impact browser and web security. He will initially exemplify how web security properties can be formalized and enforced, both in browsers and at the level of web specifications. He will then focus on WebSpec, a framework encompassing a formal model of the browser in Coq and a compiler turning Coq specifications into SMT-Lib formulas, thereby enabling the usage of off-the-shelf SMT solvers to automatically discover vulnerabilities and prove security properties. This line of research brings together formal methods and applied security in a cross-fertilizing feedback loop: vulnerabilities identified in the model are measured in the wild and large-scale evaluations often bring back new threat models that are then fed into the formal specification. This approach allowed us to identify a number of vulnerabilities in the specification and interaction of web components, and to identify fixes that we proved correct in our model.