The following sections cover how Cairo is expressed as an AIR and proved using S-two. The explanation is based on this commit of the S-two-Cairo repository.