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.

翻译：尽管在验证底层、高效且安全关键的代码方面取得了诸多成功，但关于此类大规模证明开发的结构、架构和工程方法却鲜有讨论和研究。我们提出了一套基于语言技术的设计、实现与评估方案，使程序员能够以高抽象层级模块化编写和验证代码，同时保持对编译过程的可控性，并生成适合集成至主流软件的高质量、零开销底层代码。我们在F*证明助手中实现了这些技术，特别在其浅嵌入的Low*工具链（可编译为C语言）中部署。通过评估验证表明，我们的技术对推动广受欢迎的HACL*库突破10万行验证源代码规模、显著提升证明工程师生产力起到了关键作用。方法论阐述最终聚焦于一个新颖的案例研究：流式应用程序编程接口——该脆弱接口历史遗留安全缺陷频发，曾导致知名软件出现大量漏洞。采用我们的方法，我们以通用方式捕获流式语义，并将其"零成本"应用于十余种用例场景。其中六种方案已成功部署至Python编程语言参考实现，取代了之前充满安全漏洞的代码。