Proof for aerospace, satellites and smart contracts.

// The payload may power on only while the battery,
// the temperature and the flight mode all allow it.
pub fn payload_active(
  battery_mv: i32, temp_c: i32, mode: i32
) -> bool {
  return battery_mv >= 3300
    && temp_c >= -20 && temp_c <= 60
    && mode == 1;
}

spec PayloadSafety {
  // forall: the property must hold on every path.
  fn low_power_inhibits_payload() forall {
    // @ stands for every value of its type.
    let battery_mv: i32 = @;
    let temp_c: i32 = @;
    let mode: i32 = @;
    assume {
      assert(battery_mv >= 0 && battery_mv < 3300);
      assert(temp_c >= -80 && temp_c <= 120);
    }
    // Below 3.3 V the payload never powers on.
    assert(!payload_active(battery_mv, temp_c, mode));
  }
}