There is also a problem with LAWS.bend. The typechecker only guarantees that your code satisfies what's written in LAWS.bend — not that LAWS.bend says what you actually meant. There is nothing to stop an LLM from "satisfying" a law with a vacuous or narrower-than-intended formalisation — the trust problem simply shifts from the code to the specification (which could be also generated by LLM, and therefore incorrect). The repository even admits that the compiler itself is 99% LLM generated and not yet fully audited, which seems a questionable basis on which to build a "mathematical guarantees" marketing.