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

Ok I would love to know more about how the RTOS code was shrunk by 10x using TLA+ (at 8:28)

Well, that book costs $99: http://www.springer.com/us/book/9781441997357

But there's been more recent work done in TLA+ on another realtime OS, where the mechanical proof system, TLAPS, was used to prove some aspects of the kernel correct, and you can read about it for free here: https://members.loria.fr/SMerz/papers/abz2016-pharos.html

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