Tunable Automation in Automated Program Verification
summary
A Rust-based verifier (Verus) adds a broadcast lemmas mechanism to let libraries export grouped, universally quantified facts and users import them at module, function, or local proof level; an unsat-core guided shrinking step trims imported sets to the actually used lemmas. Evaluation on four Varys/Verus codebases finds broadcasting removes about 2–8% of manual asserts and that most functions keep similar verification time (only ~1.8% slow down >2×). Exploring freer triggers (an all-trigger style) helps one project but breaks one proof and risks instantiation explosion.
AI-written summary · about