We address the challenges of scaling verification efforts to match the increasing complexity and size of systems. We propose a research agenda aimed at building a performant proof engine by studying the asymptotic performance of proof engines and redesigning their building blocks. As a case study, we explore equational rewriting and introduce a novel prototype proof engine building block for rewriting in Coq, utilizing proof by reflection for enhanced performance. Our prototype implementation can significantly improve the development of verified compilers, as demonstrated in a case study with the Fiat Cryptography toolchain. The resulting extracted command-line compiler is about 1000$\times$ faster while featuring simpler compiler-specific proofs. This work lays some foundation for scaling verification efforts and contributes to the broader goal of developing a proof engine with good asymptotic performance, ultimately aimed at enabling the verification of larger and more complex systems.

翻译：我们致力于应对验证工作随系统复杂性与规模递增所面临的扩展挑战。本文提出一项研究路线，旨在通过分析证明引擎的渐近性能并重构其基本构件，构建高性能的证明引擎。以等式重写为例，我们提出一种新型原型证明引擎构件——利用反射证明技术提升Coq中重写操作的性能。通过菲亚特密码学工具链的案例研究表明，该原型实现可显著加速已验证编译器的开发：最终提取的命令行编译器速度提升约1000倍，同时编译器专用证明更为简洁。本工作为规模化验证奠定基础，并推动实现具有良好渐近性能的证明引擎这一更广泛目标，从而最终支持更大规模复杂系统的验证。