ソフトウェアを設計段階から安全にするために、研究者はしばしば形式的検証を用いる。これは、数学的証明を用いて特定のクラスのバグを完全に排除するプロセスである。この分野における主要な障害の一つは「仕様」の問題である。プログラムが正しいことを証明するには、まず形式的意味論（すべての文やループがどのように振る舞うかを示す正確な数学的記述）を定義しなければならない。WebAssemblyやCのようないくつかの言語には確立された意味論があるが、他の多くの言語にはない。正確な仕様がなければ、プログラムの安全性を証明するための基準となる「真実」が存在しないことになる。
Basisの研究チームは、WHILEと呼ばれる小さな命令型言語のために、LLMを使用してこれらの意味論を生成することでこの問題に対処した。しかし、LLMは間違いを犯す可能性があるため、欠陥のある意味論はそれ以降のすべての証明を無効にしてしまう。これを解決するために、チームは「急進的」なアプローチを提案した。それは、既存のインタプリタ（コードを実行する実際のプログラム）を真実の基準として扱うことである。彼らはCベースのインタプリタを、形式的に定義された命令セットを持つRISC-Vマシンコードにコンパイルした。その後、LLMに対して、これらのルール（意味論）と、これらのルールがコンパイル済みバイナリの動作を完璧に予測することを証明するLean（証明アシスタント）による数学的証明のセットを記述するよう指示した。
この図は、コンパイルされたインタプリタを真実の基準として使用し、高レベルの意味論をデバッグして洗練させる「急進的」なアプローチを説明している。
この手法により、LLMは人間が書いた仕様からはしばしば省略される微妙な実装の詳細を考慮せざるを得なくなった。例えば、最初の証明は、LLMの意味論がCインタプリタが関数名を文字列にレンダリングする際の63バイトの制限を考慮していなかったために失敗した。証明は、意味論がバイナリの実際の動作と一致するように修正されたときに初めて「完了」した。コンパイルされたインタプリタをアンカーとして使用することで、研究チームは証明プロセス自体が意味論のデバッガーとして機能するシステムを構築した。証明が失敗すれば、それは高レベルのルールと低レベルの実行の間に不一致があることを示し、モデルに対してマシンコードと完全に一致するまでルールを洗練させることを強いるのである。
この視覚資料は、固定されたハードウェア/ソフトウェアのアンカーと、LLMによって生成されたコンポーネントとの間のプロジェクトの構造的な区分を説明している。