Výzkumníci z Basis popsali experiment, v němž jazykové modely pomáhaly vytvořit formální pravidla malého programovacího jazyka a ověřit jeho interpret. Nástroj Lean kontroloval matematické důkazy, že program tato pravidla zachovává i po překladu do nízkoúrovňových instrukcí pro architekturu RISC-V. Nešlo jen o porovnání výsledků na několika testovacích příkladech.
Práce se soustředí také na specifikaci: správný důkaz má omezenou hodnotu, pokud ověřuje pravidla, která neodpovídají zamýšlenému chování. Autoři proto oddělují vytvoření pravidel od prokázání, že je implementace skutečně dodržuje. Výsledek je ukázkou na malém jazyce, nikoli důkazem správnosti libovolného softwaru nebo celého používaného počítače. Pro vývoj s AI je podstatný posun od věrohodně vypadajícího kódu k vlastnostem, které lze strojově zkontrolovat.
