Adam Sampson's verification bookmarkshttps://bookmarks.offog.org/ats/verificationAdam Sampson2015-03-14T14:26:44ZProving that Android’s, Java’s and Python’s sorting algorithm is broken (and showing how to fix it) | Envisage: Engineering Virtualized Serviceshttps://bookmarks.offog.org/edit?url=http%3A%2F%2Fenvisage-project.eu%2Fproving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it%2F2015-03-14T14:26:44ZUsing formal methods to find a pretty serious bug.Language-theoretic Securityhttps://bookmarks.offog.org/edit?url=http%3A%2F%2Flangsec.org%2F2015-01-03T18:34:17Z"The Language-theoretic approach (LANGSEC) regards the Internet insecurity epidemic as a consequence of ad hoc programming of input handling at all layers of network stacks, and in other kinds of software stacks." Some interesting work, although it's obviously focussing on one class of problem...miTLS - Homehttps://bookmarks.offog.org/edit?url=http%3A%2F%2Fwww.mitls.org%2Fwsgi%2Fhome2014-04-28T13:40:41ZA formally verified implementation of TLS. (Being written in F# means it's a bit impractical to use as a library, though...)Quark : A Web Browser with a Formally Verified Kernelhttps://bookmarks.offog.org/edit?url=http%3A%2F%2Fgoto.ucsd.edu%2Fquark%2F2013-11-12T22:58:14ZBuilding a formally-verified sandbox for browser components. Neat!