DeepSpec
CompCert
を調べてたら見つけた
The Science of Deep Specification
ソフトウェアとハードウェアの完璧な仕様を求める的な壮大な目標を持った団体っぽい
LLVM
、
Haskell
、
Coq
https://gyazo.com/5e48dd90d980cdbb9a0b3e4b855f4c24
ref:
https://deepspec.org/page/Research/_
CertiKOS
形式検証とセキュリティを重視したOS
Vellvm
The Science of Deep Specification
Vellvm: Verified LLVM
GitHub:
vellvm/vellvm: The Vellvm (Verified LLVM) coq development.
CoreSpec
CertiCoq
Gallina
Bluespec
「ソフトウェアの基礎(Software Foundations)」シリーズ