With formal verification, what you want is correct statement of invariants / things to prove. As long as these are understandable, the readibility of proof doesn't matter much - it's the program job to verify that the proof is correct.