Inconsistent default nullability between Called Methods and Nullness checkers with Lombok

The called methods checker has rudimentary support for Lombok, and it's fantastic. But, some coworkers of mine were recently bitten by this behavior:

A @CalledMethods annotation is placed on the receiver of the build() method, indicating the setter methods that must be invoked on the builder before calling build(). For Lombok, this annotation’s argument is the set of @lombok.NonNull fields that do not have default values.

https://checkerframework.org/manual/#called-methods-framework-details

The second sentence disagrees with the usual rules for nullness, where fields are assumed non-null unless annotated otherwise.

Concretely, it is easy to write code that creates null pointer exceptions even when both the Called Methods and Nullness checkers are enabled:

package misc;

import lombok.Builder;
import lombok.Value;

public class BuilderNullness {

    @Value
    @Builder
    static class Data {
        String value;
    }

    public static void main(String[] args) {
        var data = Data.builder().build();
        System.out.println(data.value.hashCode());
    }

}

Output:

Exception in thread "main" java.lang.NullPointerException: Cannot invoke "String.hashCode()" because "data.value" is null
	at misc.BuilderNullness.main(BuilderNullness.java:16)

Adding an explicit @lombok.NonNull annotation to the String value field is the only way to get the expected compile-time error message:

BuilderNullness.java:[16,39] error: [finalizer.invocation] This finalizer cannot be invoked, because the following methods have not been called: value()

I suspect this policy was chosen to reduce false positives, but I would suggest that the default behavior should align with the nullness checker (fields are non-null unless annotated otherwise).

Start with the Called Methods checker’s Lombok support and the Called Methods framework details in the linked manual section. Reproduce the BuilderNullness example with both Called Methods and Nullness checking enabled, then trace how an unannotated Lombok field is classified. Done means the default nullability behavior is aligned or the intended policy is documented and covered by a regression test.