Attribute Macro trusted 

#[trusted]

Instructs Creusot to not emit any VC for a declaration, assuming any contract the declaration has is valid.

Example

#[trusted] // this is too hard to prove :(
#[ensures(result@ == 1)]
fn foo() -> i32 {
    // complicated code...
}

These declarations are part of the trusted computing base (TCB). You should strive to use this as little as possible.