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
CoreSpec
CertiCoq
Gallina
Bluespec
Software Foundations
Logical Foundations
Programming Language Foundations
Verified Functional Algorithms
QuickChick: Property-Based Testing in Coq
Verifiable C
Separation Logic Foundations