Basis beweist per Lean, dass ein LLM geschriebener Interpreter exakt dem C-Binary entspricht

Ship Your Interpreter

Basis-Agenten schrieben eine formale Semantik für die kleine Sprache WHILE und bewiesen in Lean, dass sie mit dem kompilierten C-Interpreter auf RISC-V für jedes Programm übereinstimmt. Ein früher Entwurf bestand alle Tests, scheiterte aber an Funktionsnamen ab 59 Zeichen – ein Fehler, den nur der Beweis aufdeckte. Die Autoren sehen darin einen Weg, Verifikation auf Sprachen ohne formale Semantik auszudehnen.