  For all the successes in verifying low-level, efficient, security-critical
code, little has been said or studied about the structure, architecture and
engineering of such large-scale proof developments.
  We present the design, implementation and evaluation of a set of
language-based techniques that allow the programmer to modularly write and
verify code at a high level of abstraction, while retaining control over the
compilation process and producing high-quality, zero-overhead, low-level code
suitable for integration into mainstream software.
  We implement our techniques within the F* proof assistant, and specifically
its shallowly-embedded Low* toolchain that compiles to C. Through our
evaluation, we establish that our techniques were critical in scaling the
popular HACL* library past 100,000 lines of verified source code, and brought
about significant gains in proof engineer productivity.
  The exposition of our methodology converges on one final, novel case study:
the streaming API, a finicky API that has historically caused many bugs in
high-profile software. Using our approach, we manage to capture the streaming
semantics in a generic way, and apply it ``for free'' to over a dozen
use-cases. Six of those have made it into the reference implementation of the
Python programming language, replacing the previous CVE-ridden code.
