For many software engineering researchers, the need to verify software formally does not take much convincing. Between intellectual acceptance to practical application, however, the gap is wide. With notable exceptions, particularly in life-critical software, industry does not use much formal verification. For several decades Eiffel users have been convinced that at least a degree of formality is essential, and have seen the benefits in the quality of the systems they produce. This experience has largely been based on run-time verification, but the development of the AutoProof environment is making the goal of static proofs more realistic.

To succeed, static verification (that is to say, proofs) should move from its current “heroic” status to a normal, almost casual, component of the software engineer’s everyday routine, at the same level of obviousness and acceptance as, for example, type checking or configuration management: it should become “Verification As A Matter Of Course” (VAMOC) or, to coin a shorter name, Invisible Verification.

How realistic a goal is it? This talk will examine lessons from the Eiffel experience including the automated proofs of entire libraries, present the AutoProof architecture, examine frankly the remaining scientific and engineering obstacles, and sketch a possible path towards widespread Invisible Verification.