Iris-Wasm is a mechanised higher-order separation logic building on a specification of Wasm 1.0 mechanised in Coq and the Iris framework. Using Iris-Wasm, we are able to specify and verify individual modules separately, and then compose them modularly in a simple host language featuring the core operations of the WebAssembly JavaScript Interface. Building on Iris-Wasm, we develop a logical relation that enforces robust safety: unknown, adversarial code can only affect other modules through the functions that they explicitly export. Together, the program logic and the logical relation allow us to formally verify functional correctness of WebAssembly programs, even when they invoke and are invoked by unknown code, thereby formally demonstrating that WebAssembly enforces strong isolation between modules. Iris-Wasm has also been used as a starting point to define program logics that allow formal reasoning about extensions to WebAssembly, such as MSWasm, RichWasm and Stack-Switching. Formally describing and proving the desired properties of these extensions is a strong asset in validating them and encouraging their adoption.