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.

proof_assert!

#[trusted] can also be used with proof_assert! to not emit a proof obligation for it. It becomes just a trusted assumption.