Real-world programs contain a multitude of concealed components whose formal semantics not available to verification engines, like third-party API calls, inline assembly and SIMD instructions, system calls, sampling assignments from probability distributions and library calls. Albiet the success of program verification, proving correctness of such "open" programs has remained a challenge.

Currently, this problem is handled by manually "closing" the program—by providing hand-written mocks that attempt to capture the behavior of these concealed components. Most often, writing such mock code (stubs) is not only ardious, but are often erroneous, thus raising serious questions on the whole endeavor. In light of this challenge, we came up with a novel technique, almost verification as an attempt to prove correctness for such "open" programs.