Attribute Macro verification_status 

#[verification_status]

When extracting to F*, inform about what is the current verification status for an item. It can either be lax or panic_free.