Coq

  • 수학적 정리(theorem)를 증명하기 위해 널리 사용되는 대화형 정리 증명기(interactive theorem prover)
  • Gallina라는 내장 언어 사용

WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems

References