Right now, we do not support stubbing methods declared in traits. Consider this example:

trait A {
    fn foo(&self) -> u32;

    fn bar(&self) -> u32;
}

trait B {
    fn bar(&self) -> u32;
}

struct X {}

impl X {
    fn new() -> Self {
        Self {}
    }
}

impl A for X {
    fn foo(&self) -> u32 {
        100
    }

    fn bar(&self) -> u32 {
        200
    }
}

impl B for X {
    fn bar(&self) -> u32 {
        300
    }
}

#[kani::proof]
fn harness() {
    let x = X::new();
    assert_eq!(x.foo(), 1);
    assert_eq!(A::bar(&x), 2);
    assert_eq!(<X as B>::bar(&x), 3);
}

It is currently not possible to stub X's implementation of A::foo, A::bar, or B::bar. To do so, we'd need to do two things.

First, we'd need to come up with a way to refer to trait methods in our kani::stub attributes. In rustc, these are stringified as <X as B>::bar, but paths in attribute arguments are not allowed to have spaces or symbols like < and > (they are simple paths). We could accept string arguments or come up with some other convention, e.g.:

#[kani::stub("<X as B>::bar", ...)]
// or
#[kani::stub(X__as__B::bar), ...)]

Second, we'd need to improve our path resolution algorithm to also search through trait implementations.