Performant formally verified software

Formally verified complex software brings more than quality assurance: it allows for ultra-performant code, since you can do all sorts of crazy tricks as long as you prove them safe, a luxury that unverified software does not have.

The mechanism is simple: the proof is the review. Nobody has to sit down and audit every aggressive rewrite, so you can point an AI at the code, let it optimize relentlessly, and only require that the proof still goes through. I wrote about this before in provably safe EVM optimizations.

This has been successful before at AWS, with organic humans writing proofs! Now that we can just ask AIs to write Lean proofs for us, we have already seen many instances of such results.

apc-optimizer

We wrote before about formal verification of the autoprecompiles optimizer, and the impact of this new paradigm in software engineering.

The posts above show that the new verified apc-optimizer quickly outperformed the original Rust code base in optimization metrics. The graph below shows that the verified code is also considerably quicker than the unverified code in runtime. Each dot is a circuit, and every dot below the “1” line represents a case where the verified optimizer is faster.

Scatter plot of the runtime ratio between the verified Lean optimizer and the original powdr Rust optimizer, against circuit size, on log-log axes, with most points falling below the 1 line.
Runtime ratio between the verified apc-optimizer and the original Rust implementation, per circuit, plotted against circuit size and colored by workload.

lean-zip

Kim Morrison has written about a similar experience with lean-zip, where the Lean code competes with the Rust code in runtime comparisons.

yul-compiler

yul-compiler is a verified optimizing compiler from Yul to EVM. Experiments with Aave and Uniswap tests show that powdr’s yul-compiler is already able to generate code with better gas performance than solc. This is not surprising, for the same reason presented in the introduction above. A verified compiler is allowed to absolutely send it and heavily optimize codegen in any way possible, which would simply be too dangerous for an unverified code base.

Table comparing gas of powdr's yul-compiler output against solc's across the aave-v4, gasTests, semanticTests and uniswap-v4 corpora.
Gas comparison between powdr's yul-compiler and solc on the Aave and Uniswap test corpora.

Autoresearch challenges

Over the last months, there have been several autoresearch challenges that successfully optimize or harden different systems for different metrics such as circuit size, ZK prover performance, EVM precompile gas usage, etc. See a few examples below:

Conclusion

Verified code means more than correct. With AI, it means more productivity, better metrics, faster runtime, higher quality engineering. All we need are specs and proofs.