Understanding the guarantees of a verified program

A persistent challenge with verified software is understanding what, exactly, is being verified and what guarantees are being given. Verified code doesn’t run in a vacuum; verified code ofter interacts with unverified code, possibly in either direction. This chapter documents technical information need to properly understand how verified code might interact with unverified code.