Most web servers have a plugin system through which third-party software components can be installed to extend the base functionality, but this can be problematic because it comes with security risks. Our goal is to create a mechanism through which a programmer is able to integrate a statically verified component with any unverified piece of code, and still be able to prove safety properties about the whole program. We define a novel Gradual IO Dijkstra monad that allows the seamless interoperability between static and dynamic checking for IO programs in F*.