We are working towards a formally secure compilation framework to compile verified F* programs to an ML language. The framework, itself written and verified in F*, aims to compile verified F* programs and link them with unverified ML programs securely, so that any unverified code cannot inadvertently or maliciously break the internal invariants of the verified code. In previous work on this project we have built formally secure compilation frameworks between shallowly embedded subsets of F*—i.e., we used shallow embeddings not only for the verified code (which is standard in F*) but also for the unverified code. To compile further to OCaml, we relied on F*’s extraction mechanism, which is, however, unverified. In this extended abstract, we present ongoing work on extending our framework with a formally secure compilation step to an ML language deeply embedded in F*, thus achieving end-to-end security guarantees.