Static Invariants and Initialization: When are static invariants proven?

[WolframPfeifer]

If false is encoded in a static invariant, this can be used to prove arbitrary postconditions.

Consider the following class:

class A {
    //@ static invariant false;

    //@ ensures false;
    A() {}

    //@ ensures false;
    void m() {
    }
}

Of course, in general this could happen accidentally and more sophisticated.

The question is: Where is the static invariant proven?

In my understanding, it would need to be proven whenever the static initialization of the class happens.
However, by default this is disabled, so the static invariant is just an assumption.

KeY has the feature of enabling static intialization (taclet option: initialisation:enableStaticInitialisation). I have never used this until today, and when I tried it, the symbolic execution did not terminate (at least not within 30k steps), and KeY was completely unresponsive, probably because of the heavy branching and huge sequents. Is this expected? How are you supposed to work with this setting? I was not able to prove even the simplest method constructor contract ("ensures true" with no method body).

I would have expected that at least the constructor contract above would not be provable with static initialization enabled.
However, they are! Actually, the static invariant is assumed in the precondition. Is this correct? What am I missing?

Edit: I did a mistake there: I am able to close method contracts, the problem where the symbolic execution runs seemingly endless are constructor contracts.

[WolframPfeifer]

Actually, in recent LLM experiments (by @samysweb and @BookWood7th), the LLMs found this "shortcut" for making method contracts provable by encoding false in the static invariant.

[BookWood7th]

Would the contract for a method like this sufficiently model the proof obligation for the establishment of static invariants?

//@ensures \static_invariant_for();
void /*@helper@*/ invCheck() {}

I would ordinarily like to annotate the class with an initially clause, but this seems to no longer be supported by KeY, at least the implementation of de.uka.ilkd.key.speclang.njml.Translator suggests as much.

Edit: formatting

[WolframPfeifer]

Even for static methods, the static invariant is just implicitly added to the precondition. This seems unsound, at least for the main method.
From a short discussion with @mattulbrich: Do we have a well-foundedness problem here?

[wadoon]

Does anyone have knowledge of how OpenJML handles this case?

[BookWood7th]

Using @WolframPfeifer 's example, verification with OpenJML succeeds. Static invariants are required to hold before each method call (even constructors).
I would expect this to add a requirement for the method call, but seemingly this does not happen, as I could also verify B#b() contract with OpenJML.

class A {
    //@ static invariant false;

    //@ ensures false;
    A() {}

    //@ ensures false;
    void m() {
    }
}

class B {
    //@normal_behavior
    //@ensures false;
    public void b() {
      A a = new A();
      a.m();
    }
}

KeY does require proving that the static invariant for A holds in the precondition branch for B#b().