TLAPS-proved invariant violated in TLC?

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

Hello!

During designing a (proprietary) protocol I've reached a point where
I've proved (all highlighted green in TLA+ Toolbox) an invariant like

  THEOREM InvariantHolds == Spec => []Invariant \* All green
  <1>1. Init => Invariant PROOF OMITTED \* For this e-mail
  <1>2. Invariant /\ [Next]_vars => Invariant'
    <2> SUFFICES ASSUME Invariant
                        [Next]_vars
                 PROVE Invariant'
        OBVIOUS
    <2>1. CASE NextComponent BY PTL
    <2>2. CASE NextComponent2 BY PTL
    \* ...
    <2>3. QED BY <2>1, <2>2 (* ... *) DEF Next
  <1>3. QED BY <1>1, <1>2, PTL DEF Spec

But when I run the protocol TLC it reports that the invariant Invariant
is violated. After debugging this for a while I found a bug in my
Invariant which explains why it failed in TLC. Is it incorrect of me to
assume TLAPS has successfully proved the theorem when the TLA+ Toolbox
hightlights the theorem all green a pressing CTRL+G on it twice? Am I
doing something wrong or is this a bug?

Best regards,
Jaak