Tag
Basis researchers used LLMs to write formal semantics for a small programming language and proved in Lean that the interpreter conforms to those rules after compilation to RISC-V, treating the existing interpreter as ground truth to overcome the specification bottleneck in verified software.