  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.
