Software Fault Isolation is a security-enhancing program transformation for instrumenting an untrusted binary module so that it runs inside a dedicated isolated address space, called a sandbox. To ensure that the untrusted module cannot escape its sandbox, existing approaches such as Google’s Native Client relies on a binary verifier to check that all memory accesses are within the sandbox. Instead of relying on a posteriori verification, Portable Software Fault Isolation proposes to insert a program instrumentation phase as part of a certified compiler, and leverage the soundness proof of this compiler to enforce a sandboxing security property. This eliminates the need for a binary verifier. In this paper, we describe the design, implementation and proof of an efficient, machine-checked \compcert implementation of Portable Software Fault Isolation. We propose a novel sandboxing transformation that has a well-defined C semantics and which supports arbitrary function pointers. Experiments show that our formally verified technique is a competitive way of implementing Software Fault Isolation.