returns

The returns clause is syntactic sugar for an ensures clause of a certain form. The returns clause can be provided instead of or in addition to an ensures clause.

The following:

fn example() -> return_type returns $expr { ... }

is equivalent to:

fn example() -> (return_name: return_type) ensures return_name == $expr { ... }

With the #![verifier::allow_in_spec] attribute

The #![verifier::allow_in_spec] attribute attribute can be applied to an executable function with a returns clause. This allows the function to be used in spec mode, where it is interpreted as equivalent to the specified return-value.