You do it by comparing to something that is “known” to be good.

I didn’t read the whole article, just the appendix. There they talked about having Claude write a python interpreter. Then they had it write a set of properties to test and they vetted the properties against accepted existing python interpreters.

Proving two things are equivalent is a major component of formal.

For everything else, formal is only as good as the properties you specify. A long standing problem. But it’s a problem for all verification. If you write a shitty tests, you get shitty verification.

A key difference I think is that the same skills used for evaluating and reviewing application code apply to reviewing test code. That’s not really true for formal.