I'm curious how their approach compares with what Theorem & Anthropic are trying to do with formally proving nixpkgs: https://theorem.dev/blog/verified-software-stack/