Tunable Automation in Automated Program Verification

TL;DR

Quantifier instantiation is the bottleneck in SMT-based automated verification, forcing a trade-off between automation and performance. The authors introduce a broadcast mechanism to publish quantified facts on demand (via broadcast and broadcast use), enabling fine-grained automation control across modules, functions, and proofs, implemented in Verus. They evaluate automation-time tradeoffs on several real Verus projects, showing that ambient facts can reduce manual hints but may slow verification in some contexts, and that trigger strategies further modulate the automation-performance balance. The work contributes a practical approach to scalable, user-tunable automation in program verification and informs guidelines on when to broaden context or rely on trigger-driven instantiation.

Abstract

Automated verification tools based on SMT solvers have made significant progress in verifying complex software systems. However, these tools face a fundamental tension between automation and performance when dealing with quantifier instantiation -- the primary source of incompleteness and verification slowdown in SMT-based verifiers. Tools choose between aggressive quantifier instantiation that provides more automation but longer verification times, or conservative instantiation that responds quickly but may require more manual proof hints. We present a mechanism that enables fine-grained control over the availability of quantified facts in verification contexts, allowing developers to selectively tune the level of automation. Our approach lets library authors provide different pre-defined automation levels while giving end-users the ability to further customize quantifier availability at the module, function, or proof context level. We implement our techniques in Verus, a Rust-based verification tool, and evaluate them on multiple openly available codebases. Our empirical analysis demonstrates the automation-performance tradeoff and that selective quantifier management enables developers to select the appropriate level of automation in different contexts.

Figures (5)

• Figure 1: The spectrum of quantifier-based automation.
• Figure 2: Excerpt from the definition of IronKV's key trait: the example has been simplified for ease of presentation but without hiding any relevant details.
• Figure 3: Cumulative distribution of verification time ratio between ambient facts (minimized) and original verification time for each function. We removed two extreme cases of 10x+ verification slowdown, one in Splinter, where the runtime bumped from 34ms to 669ms (19.1x), and one in Anvil, where the runtime bumped from 3508ms to 43563ms (12.4x).
• Figure 4: Runtime Ratio for 20 runs (each with one of the randomly sampled asserts removed) against successful verification.
• Figure 5: Cumulative distribution of verification time, and verification "slowdown" ratio for 20 sampled asserts for IronKV with enabled. Detailed descriptions of the two figures can be seen in \ref{['fig:all']} and \ref{['fig:failure-sample']}.