形式手法
證明支援
Curry-Howard 對應
Rocq (a.k.a. Coq)
Welcome! | The Coq Proof Assistant
Extraction of programs in OCaml and Haskell — Coq 8.10.2 documentation
officially supported : OCamlOCaml.icon, HaskellHaskell.icon, Scheme
IDE
Proof General
VSCoq - Visual Studio Marketplace
coq-community/awesome-coq: A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources maintainers=@anton-trunov,@palmskog
Isabelle
Isabelle
officially supported : SML, OCamlOCaml.icon, HaskellHaskell.icon, ScalaScala.icon
Agda
agda/agda-ocaml: OCaml backend for Agda
F*
F*: A Higher-Order Effectful Language Designed for Program Verification
officially supported : OCamlOCaml.icon, F#, C, WebAssemblyWebAssembly.icon
Idris
ziman/idris-ocaml: OCaml back end for Idris
officially : C, ECMAScriptECMAScript.icon
moonad/Formality: An efficient proof language
Lean (theorem prover)
Common Lisp
ACL2
ACL2 Version 8.5
model 檢査
線形時相論理 (LTL)
時相行動論理 (TLA)
Alloy
Z言語 - Wikipedia
VDM++による形式仕様記述
AWSにおける形式手法 - masateruk’s blog
チェシャ猫
形式手法で捗る！インフラ構成の設計と検証
形式手法と AWS のおいしい関係。- モデル検査器 Alloy によるインフラ設計技法 #jawsfesta
分散システム、本当に「正しく」開発できますか？ #JTF2018 / July Tech Festa 2018 - Speaker Deck