Attribute Macro formal_method 

#[formal_method]

Mark a function as a contract-honoring formal method and generate backend verification harnesses.

Syntax

use elicitation::formal_method;

#[formal_method(contracts = [InvariantHolds])]
fn advance(state: MyState, proof: Established<InvariantHolds>)
    -> (MyState, Established<InvariantHolds>)
{
    (state.next(), proof)
}

The contracts = [...] argument is optional. The macro adds a doc annotation and emits a #[cfg(kani)] #[kani::proof] harness. Type enforcement is already provided by the FormalMethod blanket impl.