This was a missed opportunity to showcase how to use formal methods for proof of correctness. The author does not even seem to be particularly interested in programming language design; there is no discussion of design goals, or inspiration. Nothing to see here.

One of my experiments was to have Claude write a VM and then generate a verification harness (using a DSL) for it to ensure it was correct with the theory being the same bug would have to exist in the test suite, the static verification and the VM for it to sneak through. Found a few bugs in the verification library and some integer overflows in the VM then it became too much for my poor little laptop to run without cutting some important corners.

It's not an abstract thing they can't do, you just have to tell them to.