Second day in a row where HN frontpage features formally verified software!<p>If you're like me, and would like to get started, or just see what this is all about, the TLA+ homepage and video course (narrated by Leslie Lamport himself), is a nice resource [1].<p>In about half an hour you will have a brief understanding of what "formal specification languages" are, write and 'prove' your first small program/spec. If you have another hour to spend, keep the cheatsheet [2] near you and follow through, you will write and 'prove' more complex specs, plus you'll start thinking about systems in a more abstract way. Finishing up the video course you'll be able to start reading complex specs others have written, or write a spec for any algorithm you think is fun!<p>[1] <a href="https://lamport.azurewebsites.net/video/videos.html" rel="nofollow">https://lamport.azurewebsites.net/video/videos.html</a>
[2] <a href="https://lamport.azurewebsites.net/tla/summary-standalone.pdf" rel="nofollow">https://lamport.azurewebsites.net/tla/summary-standalone.pdf</a>
Kind of a dumb question: have any operating systems been formally verified? Unless you are running an embedded application, verifying your software seems kind of pointless if you are still at the mercy of "unverified" system calls, memory manager, scheduler, etc etc.
I have wanted to see a real-world use of seL4 in a safety-critical system since I heard about it 2 years ago. This is really impressive, and I'm very happy to see this here.