Isn’t frame conditions quite fragile?

I agree … it is criminally error prone.

I once made a PlusCal like interpreter in the Alloy code base. There I analyzed the branches (implies) and made sure to add instructions when one branch set a var that was not set in the other branch. This seemed to work well but I have no idea how theoretically solid it was and nobody got excited … so it has been lingering since. From a user point of view I think it would be really a huge gain.