I will present my results towards a formally secure extraction framework for the proof-oriented language F* that protects verified F* programs against linked unverified ML code. The source language is an F* subset in which a verified effectful program interacts with unverified code via a higher-order interface that includes refinement types as well as pre- and postconditions. The framework supports verified IO programs where pre- and postconditions are in terms of past IO events, and verified stateful programs that can dynamically share ML-style mutable references with the unverified code. The framework enforces the specification on the higher-order interface during extraction using higher-order contracts and a reference monitor. The framework is itself written in F* and offers formal guarantees that it is sound and satisfies Robust Relational Hyperproperty Preservation (RrHP), a very strong secure compilation criterion that implies full abstraction as well as preservation of trace properties and hyperproperties against arbitrary adversarial unverified code.