Sireum Logika

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!