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 often interacts with unverified code, possibly in either direction. This chapter documents technical information needed to properly understand how verified code might interact with unverified code.