[NovemberWhiskey]

I am not sure that static analysis is ever going to give answers to those questions. I think the best you can hope to do is surface knowledge about the tacit assumptions about dependencies in order to explore their behaviors through simulation or testing.

I think it often boils down to "know when you're going to start queuing, and how you will design the system to bound those queues". If you're not using that principle at design stage then I think you're already cooked.

[amw-zero]

Who brought up static analysis?

I think simulation is definitely a promising direction.

[NovemberWhiskey]

I mean, the fundamental premise of formal methods is that assurance of correctness is achieved through unambiguous specification/modeling and mathematical proof. The extent to which you're dependent on dynamic testing of actual code to achieve assurance does speak to the extent to which you're really relying on formal methods.

[amw-zero]

That’s literally what the post is about. I don’t see your point. The post is saying that formal tools currently do not handle performance and reliability problems. No one said otherwise.