What do we do? I have been working with LemmaScript, an annotated version of TypeScript. It can take existing code, such as the roughly 70,000 lines of JavaScript in EtherCalc and SocialCalc, which I maintain with spreadsheet inventor Dan Bricklin, and let us write invariants as cryptographically attested lemmas that AI agents can prove.