News for hackers. Stuff that matters.
Re:Applying the Linus Torvalds “Good Taste” Coding Requirement by nickpsecurity on Wednesday October 26, 2016 @01:16PM (#12798382)
SPARK does that with efficient, system code. Then proves the code free of common errors in C. Then other tools can generate unit tests from the specs just in case. Frama-C does something similar for C. I'm not sure what the usability or thoroughness is like vs SPARK, though.

http://www.spark-2014.org/about

There are no comments on this comment yet.