Nice seeing work from a former professor of mine on HN. A lot of the faculty at KSU work on formal verification tooling but industry seems to avoid it in most cases (yes, Amazon uses TLA+ sometimes, allegedly). And now I work on AI products where correctness is itself an ambiguous idea.

I guess the challenge is that formal verification of an application in some sense depends on the correctness of its dependencies: the OS, the libraries, the compiler, etc. And maybe even hypervisor, silicon, and network switches!

Hey, what kind of work are you currently doing in AI? Just asking out of curiosity. I want to have a brief chat with you about these proof checkers and verification systems. I never got the gist of all these. Stuffs like lean theorem prover. I will be glad If you take out some time.