IID.systems
プロフィール事業紹介形式手法AIアライメントエッセイ書籍プログラミング教室GitHubEnglish
English

形式手法(Formal Methods)

数学的厳密性でソフトウェアの正しさを追求する

形式手法は、数学的な記法と論理に基づいてソフトウェアの仕様を記述・検証する技術の総称です。航空宇宙、鉄道、医療機器など、高い信頼性が求められる分野で長年にわたり活用されてきました。IID Systemsでは、この形式手法をAI時代のソフトウェア開発にどう活かすかを研究しています。

形式手法とは

入門

モデル検査・定理証明・仕様記述の3分野と実績

形式的仕様記述

技術

VDM-SL、TLA+、B-Methodなど仕様記述言語の解説

AI時代の形式手法

展望

LLMと形式手法の組み合わせがもたらす可能性

手法比較

分析

ウォーターフォール・アジャイル・TDDとの構造的な違い

研究プロジェクト

研究

IID Systemsが取り組む形式仕様駆動AI開発の研究

Formal Agent Contracts

Plugin

VDM-SLでエージェント間契約を定義・検証し、コードと契約テストを生成するClaude Codeプラグイン