> The formal verification wasn't wrong, just incomplete, because modeling complex systems is inherently an intractable problem. I’m not involved in this kind o

> The formal verification wasn't wrong, just incomplete, because modeling complex systems is inherently an intractable problem. I’m not involved in this kind of research or low level auditing, but I have some mathematical training and fascination with the idea of formal verification. I ran across this thing called “K-Framework” that seems to have invested a lot in making formal semantics approachable (to the extent that’s possible). It’s striving to bridge that gap between academia and practicality, and the creator seems to really “get” both the academic and practical challenges of something like that. Here’s a brief overview of one of the features that seems most impressive/useful: https://youtu.be/x_xm69gd3fE https://youtu.be/x_xm69gd3fE The clarity of Grigore’s explanations and the quality of what I’ve found here: https://kframework.org/ https://kframework.org/ makes me think K has a lot of potential, but again, this is not my direct area of expertise, and I haven’t been able to justify a deep dive to judge beyond impressions. You’re correct in pointing out that complex systems are inevitably difficult to verify, but I think stuff like K could help provably minimize surface area a lot.