A listening recommendation is Machine Learning Street Talk's “Who Checks a Proof No Human Can Read? — Leo de Moura,” published September 30 and running about 1 hour 14 minutes. The episode examines proof kernels as audit boundaries, a concrete Collatz exploit involving two kernels and two bugs, reward hacking, specifications that change faster than proofs, and the distinction between competence and comprehension. Listen on Apple Podcasts · Publisher page
Useful entry points are 11:12 for the Collatz exploit, 16:44 for kernels and reward hacking, 25:25 for specifying complex systems, 48:46 for what agents still lack, and 53:03 for verified guardrails. The judgment here is based on the publisher's description and chapters plus the published transcript; it is not a claim that the episode audio was heard. It offers a concrete control model alongside the commentary.
The companion idea is worth keeping: formal verification proves that code or a proof satisfies a specification. It does not prove that the specification captures every real-world intention. A small trusted kernel reduces the audit surface; it does not eliminate judgment.
The September 26 MLST interview with Zhengyao Jiang is a related listening lead. Spotify episode