Hi Andrew,
From the perspective of using TLA+/TLC to establish the correctness of architects' and designers' (something I did for many years in industry), what you are seeing is a desired behavior.
(Allow me to apologize for such a long reply to a simple question. Our team debated ideas surrounding what you touched on many times over multiple projects with lots of customers. I have much to say as a result. Let me know if any of the following doesn't make sense. Hopefully the length won't bore you to death.)
First, I want to say something we had to remind ourselves regularly: We write specifications in TLA+, not programs or informal descriptions.
With that said, let me generalize your Formula action and add a next state relation to it.
Formula ==
/\ \/ A
\/ B
/\ N
where N is the next state relation and A and B are preconditions for N to occur. In this form, what Formula says to the architects and designers I worked with is
If the system is in a state where A is true, then N can occur.
and
If the system is in a state where B is true, then N can occur.
I used "and" there to clarify that A and B are separate conditions even though in our TLA+ specification we would combine them disjunctively. In a specification and in their minds, there is no relationship between A and B. Formula is really two specifications in one because of the disjunction.
Thus, if my customers saw your specific version of Formula, they would interpret that as
If record has a NoRecord value, then the system can act
and
If record.key is true, then the system can act
They would immediately balk at the second specification because there is no check that record has a valid key. And they would be right. So, even before running TLC I would have to rewrite the TLA+ as
Formula ==
/\ \/ record = NoRecord
\/ /\ record # NoRecord
/\ record.key
/\ NextStateStuff
We would write the spec this way instead of using an if-then or implication because the specification is clearer and fully spelled out. When the architects and designers read the specifications, they want to see the clear, specific rules. If the rules require them to think about language semantics or take data construction implications into mind, then they are not good rules and they will rightly push back. They would push back on your second disjunct because it implies record has to be checked first. They don't want to have to figure that out. Their jobs are stressful enough as it is. Plus, leaving the implication for them to figure out provides an effective path for a bug to get into the design, which runs counter to why we write specifications in the first place: To prevent bugs in designs.
For us folks using TLA+/TLC, we want TLC to handle the disjuncts separately. TLC parallelizes disjunction analysis, thank goodness. In our designs, we had so many actions with so many disjuncts that if TLC evaluated them all in order to check for side effects, performance would have tanked. In a fully mature specification, the next state relation is an enormous disjunction (of nested disjunctions of nested disjunctions of...). Evaluating all that in order would be prohibitive.
In short, for the sake of writing clear specifications, the TLC exception you are seeing is a good thing, and for TLC performance, we want it to evaluate disjuncts in parallel.