Verusはいかにしてプログラムの性質を証明できているか

調査対象

lambda verus
verus verifier implementation
- verification condition generation
related subjects
- RustHornBelt
  - 博論でのVerusの形式モデルに関する議論はRustHornBeltの定式化を拡張する形で行われている
- Verus IR(vir/air/(hir))
  - 検証用の中間表現は特定の計算モデルを念頭に設計されているか？