Specification code, proof code, executable code

Verus classifies code into three modes: spec, proof, and exec, where:

• spec code describes properties about programs
• proof code proves that programs satisfy properties
• exec code is ordinary Rust code that can be compiled and run

Both spec code and proof code are forms of ghost code, so we can organize the three modes in a hierarchy:

• code
  • ghost code
    • spec code
    • proof code
  • exec code

Every function in Verus is either a spec function, a proof function, or an exec function:

spec fn f1(x: int) -> int {
    x / 2
}

proof fn f2(x: int) -> int {
    x / 2
}

// "exec" is optional, and is usually omitted
exec fn f3(x: u64) -> u64 {
    x / 2
}

exec is the default function annotation, so it is usually omitted:

fn f3(x: u64) -> u64 { x / 2 } // exec function

The rest of this chapter will discuss these three modes in more detail. As you read, you can keep in mind the following relationships between the three modes: