For a while now, @kirancodes has been excitedly telling everyone at @BasisOrg who would listen about a crazy idea she's been pursuing. Not everyone thought it was possible, but it's starting to work. See basis.ai/blog/ship-your-inte… TL;DR: The bottleneck in verifying the world's software is shifting from theorem proving to specifications and semantics. We now have a way to verify semantics that can scale across all programming languages. The basic idea: To verify that a program is correct, you need the program, a specification you want to prove, and a semantics that defines what programs and specs mean. Most programming languages (Python, Ruby, Lua…) have no formal semantics, because semantics are painful to write for complex languages. You can ask an LLM to write a semantics for you, but it'll probably have mistakes. But (i) programming languages do have interpreters/compilers, which ultimately are compiled down to machine code, and (ii) some instruction sets do have formal semantics. RISC-V has an official formal model. So, crazy idea: Step 1: Compile your interpreter (e.g. Python's) down to RISC-V. Now its behaviour is formally defined. It's exact, but unreadable: thousands of machine instructions. Step 2: Ask your LLM to write a semantics for your language. Step 3: Ask the LLM to prove, in @leanprover, that its semantics agrees with the compiled interpreter on every possible program. If the semantics is wrong, the proof gets stuck, and the LLM goes back to fix it. Step 4: If the proof goes through, you have a semantics you don't need to trust, and you can verify programs in a language that never had one, with guarantees that reach the binary that actually runs. Kiran has now done this end to end for a simple WHILE language, and we're scaling it up to Lua and OCaml, with Python as the north star.