Hacker News new | past | comments | ask | show | jobs | submit login

If you don't have any concurrency or nondeterminism in your spec, then you'll probably want different tools. It's not that TLA+ is bad at modeling single-threaded algorithms, it's just that makes a lot of design decisions around representing concurrency, and there's an opportunity cost to that. I'd consider a code-level formal verification language, like Liquid Haskell or Dafny.



Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: