Systems are usually implemented in a high-level language, compiled to machine instructions and run on a dedicated hardware architecture. The goal of end-to-end verification is to prove a system meets its intended specification at the high-level language, and preserve such a property across the lower, more concrete layers, all the way down to the hardware. Large scale end-to-end verification of a system therefore requires:

1. A program logic for the language in which the system is implemented.
2. A compilation chain that preserves properties of the system from the high-level source language down to the target language, e.g., machine code.

We propose a strategy for end-to-end verification based on a compilation chain that preserves the properties provable in a weakest precondition calculus for the source language.