Post #2985137

2026-05-12 03:19 UTC

@bob_zim@infosec.exchange, I would bet money that no system which does something of interest to @stilgherrian@eigenmagic.net has been formally verified to the complete degree you say. Which is why my description includes the requirement that the software does something people are interested in. Yes, there might exist formally-verified systems with no detectable bugs; but likely that doesn't describe any system we directly use.

Replies (2)

@shieldsy05@aus.social 2026-05-12 03:23

@bignose@social.chinwag.org @bob_zim@infosec.exchange @stilgherrian@eigenmagic.net though it sounds like curl is pretty dang close! (To being bug/vulnerability-free, and ubiquitously used) Also assumes that the verification/validation process is flawlessly designed and executed to test all positive cases and all possible negative cases, and I’m gonna hazard a guess that that’s happened only on a handful of systems in the history of the world.

Open ##2985138
@bob_zim@infosec.exchange 2026-05-12 03:50

@bignose@social.chinwag.org @stilgherrian@eigenmagic.net seL4 is formally verified, and it’s extremely widely used. Several other operating systems are, too. Big chunks of the OS used by Qualcomm modems (so, present in ~95% of smartphones sold in the last year) are formally verified.

Open ##2985143