I heard that the outputs of formal verification tools are often unreadable, as they work through the proof mechanically, step-by-step. It means sometimes the computer can tell if the reasoning is flawed, but it takes a lot of effort to understand the counter-argument from the computer. Is there any effort to solve this problem?