[codepie]

TLA+ is mentioned a lot here and many people point out how it's practically infeasible to use it in real world systems. Just curious, is there any alternative to write specifications which are more closer to common programming languages and can be used by an average programmer to formally prove correctness?

[Taikonerd]

I've heard Alloy is easier to learn. That being said, Alloy and TLA+ are both languages for specifications, so they can't prove an implementation is correct.

[ALLTaken]

Nobody mentioned Agda. I had to use Alloy in the university and it was easy, but it doesn't cover all bases as the previous commenter said.