Post #2985139

@shieldsy05@aus.social @bignose@social.chinwag.org @stilgherrian@eigenmagic.net The verification process involves building a mathematical proof that the software has all of the specified behaviors and has no undefined behaviors. It’s concrete proof of exact match. Writing a sufficiently detailed specification is difficult, of course, but there are tools to help. It’s mostly worthwhile in the embedded space, industrial process control, and in situations where the hardware is exceptionally difficult to access to update (e.g, satellites). These things are widely deployed, though. This message definitely goes through at least four formally-verified OS kernels on its way to you.