TLA+: Format Verification Language And Toolkit

[Thomas Passin]

I always thought that formal verification (FV) of programs would be too hard and error prone beyond simple programs.  Apparently I was wrong about that, and one reason is that FV should be applied above the program level - e.g., to algorithms.

"TLA+ is a language for modeling software above the code level and hardware above the circuit level. It has an IDE (Integrated Development Environment) for writing models and running tools to check them."  

Formal Verification With TLA+

[Thomas Passin]

Darn, the title was supposed to say "Formal Verification ...".

[Edward K. Ream]

On Thu, May 9, 2024 at 9:17 AM Thomas Passin <tbp1...@gmail.com> wrote:

I always thought that formal verification (FV) of programs would be too hard and error prone beyond simple programs.  Apparently I was wrong about that, and one reason is that FV should be applied above the program level - e.g., to algorithms.

Thanks for the link :-)

Edward