I think, maybe some formalism could exist for the task which makes it significantly easier.
My problem to solve is that I invented a reentrant algorithm for a task. It is relative simple (its pure logic is around 10 lines in C), but this 10 lines to construct was around 2 days to me. I am 99% sure that it is reentrant (which is not the same as thread-safe!), but the remaining 1% is already enough to disrupt my nights.
Of course I could start to do that on a naive way (using a formalized state space, initial conditions, elemental operations and end-conditions for that, etc.), but I think some type of formalism maybe exists which makes this significantly easier and shorter.
Proving the non-reentrancy is much easier, simply by showing a state where the end-conditions aren't fulfilled. But of course I constructed the algorithm so that I can't find a such state.
I have a strong impression, that it is an algorithmically undecidable problem in the general case (probably it can be reduced to the halting problem), but my single case isn't general.
I ask for ideas which make the proof easier. How are similar problems being solved in most cases? For example, a non-trivial condition whose fulfillment would decide the question into any direction, would be already a big help.