ZetZ、形式的検証機能を備えたCのダイアレクト原文(投稿日：2020/02/27)へのリンク ZetZ、略してZZは、RustにインスパイアされたCのダイアレクト(diarect, 方言)だ。コンパイル時に仮想マシン内でシンボリック実行することによって、コードの形式的検証を行う。 ZZはハードウェアに近い部分で動作するソフトウェアをターゲットにしているが、クロスプラットフォームなANSI-C準拠のライブラリ構築にも使用することができる。実際には、ZZはCコードのトランスパイラとして、処理結果を任意の標準的Cコンパイラに入力することで動作する。多くの言語が行っている安全性へのアプローチとは対照的に、ZZは、例えば生のポインタアクセスのように"安全でない(unsafe)"と見なした機能の除外や制限は行わない。その代わりに静的単一代入(static single assignment, SSA)を使用して、yices2やz3といったSMTプ
