最近形式検証に興味があるので、ACL2を触ってみた。 形式検証とは 仕様を特定の形式で書くと正しさをチェックしてくれる、らしい。 ALC2とは Common Lispで書かれた形式検証のツール。 ACL2 Version 8.3 GitHub - acl2/acl2: ACL2 System and Books as Maint…