Dante: A Case Study in Compiler-Assisted Verification Using Model Checking

Introduction If you're a developer today, chances are you've experienced the “magic” of LLMs in your workflow, whether you realize it or not. That auto-completion in your JetBrains IDE, Visual Studio, or Cursor? There's cases where an LLM working beh...