TScert: TypeScriptのための厳密なコア

［画像: TScert: a sound core for TypeScript］

TScertは、TypeScriptの関数が型安全であることを検証し、証明付きで関数を受け入れます。その健全性がLeanで証明されたチェッカーが、その証明を検証します。TScertはTypeScriptや提案ツールが推論する型を一切信頼せず、受け入れの基準は「受け入れの意味」でリスト化されています。

tscert-launch.mp4［動画］

なぜ

TypeScriptの型チェッカーは、意図的に不健全な部分があります。any、型アサーション、チェックされていないインデックスアクセス、共変配列などにより、tscをパスしたプログラムでも、型がstringを示している場所でundefinedを読み込んでしまう可能性があります。TScertは、それが受け入れるコードに対して、より強力な保証を提供します。アノテーションを満たすすべての入力に対して、関数が形式モデルに変換された際、値が適合しない操作を適用したり、結果の型外の値が返されたりすることはありません。その保証はLeanの定理によって述べられ、受け入れを決定するチェッカーは、その定理が対象とするコードそのものです。

例

［画像: チェッカー、虫眼鏡付きの回転台］

TypeScriptはこの関数を受け入れます（strictモードで、noUncheckedIndexedAccessはオフの状態）。TScertはこれを拒否します。

export function stale(xs: string[]): string {
  const n = xs.length;
  xs.pop();
  return xs[n - 1]; // popの後で配列の範囲外: 実行時にはundefined
}

省略された出力（オフセットは例ファイルを参照）:

"status": "unverified"
reject: source expression obligation at [219,228): evidence search failed: no derivation of its return-contract claim
obligation: The available claim for xs[n - 1] is undefined | string. This return requires string.

結果の型を正直にstring | undefinedと明記した場合、TScertはそれを受け入れます。両方のバージョンはパイプラインケースです。invalid-array-last-after-pop.tsと、array-last-element.tsのafterPopです。

仕組み

［画像: 解析、計画、詳細化はレビューで信頼され、提案と検索は誤りうる提案であり、チェックは健全性が証明され、証明書と生成された同じ要求の詳細化を受け取ります。］

TypeScriptのコンパイラAPIのフロントエンドがソースコードと使用される宣言を読み取り、Leanがその実行を計画します。OCamlプログラムであるproducerが、すべての式と変数の型を提案します。その回答はclaimsと呼ばれ、どれも信頼されません。Leanは、それらの型を持つ関数を、Leanで実行と安全性が定義されている小さな形式言語（calculus）に翻訳します。信頼されない検索がcertificate（プログラムが型を満たすという導出）を提案し、チェッカーは同じ翻訳に対してそれを検証します。ステージが各ステップを説明しています。

受け入れの意味

受け入れは、関数がcalculusに翻訳されたものについて、入力とヒープが宣言された型を満たす場合、スタックしたり、結果の型外の値が返されたりしないことを証明します。例外が発生したり、無限ループしたりする可能性はあります。定理はcheckUnitJson_safeです。証明ではなく信頼されている事柄がいくつかあります。

• TypeScriptからcalculusへの翻訳が忠実であること（レビューとテスト済みであり、証明されていません）。
• ライブラリ関数とホスト関数が、レビューされた契約通りに動作すること。
• 呼び出し元とインポートが宣言された型を満たすこと。
• Lean自体。

信頼の表面積はすべての仮定をリスト化し、「検証済み」の意味は保証を正確に述べています。

ステータス

TScertは研究プロジェクトであり、意図的に未完成です。そのベンチマークは自身のフロントエンドです。v0.94の時点で、tools/の686関数のうち643が検証されており、各関数は自身のユニットで、宣言されたシグネチャで読み取られるもの（2026-11-04付けのae20a6c6の集計）でチェックされています。カバレッジメトリクスとステータステーブルは、定義と日付付きの測定値を提供します。

概要として、サポートされているサブセットは以下をカバーしています。

• const/let、パターンマッチ、if、switch、for...ofやfor...inを含むループ、ラベル付きブロック、throw、try/catch/finally。
• リテラル型を持つプリミティブ、算術演算、比較、テンプレートリテラル、typeof、in、instanceof、厳密等価性。
• スプレッド構文を持つオブジェクトリテラル、レコード、インデックスシグネチャ、配列とタプル、オプショナルチェイニング、列挙型、フィールド、メソッド、基底クラスを持つクラス。
• 関数、クロージャ、オプショナル、デフォルト、レストパラメータ、あらゆる許容される型引数に対して証明されたジェネリック関数、ネイティブPromiseのasyncとawait。
• 宣言された型: エイリアス、インターフェース、ユニオン、インターセクション、レビュー済みの契約を通じたライブラリ型。

anyは拒否され、型アサーション（e as T、e!）は何も決定しません。サポートされていないすべての形式は、理由と場所とともに拒否されます。フラグメント境界は、拒否されるものとその理由をリスト化しています。

肩に乗って

TScertは、型とセマンティクスに関する数十年にわたる研究の上に成り立っています。それらには、証明付きコードの基礎となるAppelとMcAllesterのインデックスモデル、Ahmedのミュータブル状態のための型セマンティクス、WrightとFelleisenの構文的型健全性、Reynoldsのパラメトリック性、AbadiとCardelliのオブジェクト理論、セマンティックサブタイピング、JSCert、ECMAScript仕様、そしてLean 4などがあります。REFERENCESは、TScertがそれらから何を取り入れたか、そしてどこでそれらを参照しているかを含め、すべての作業をリスト化しています。

試してみる

前提条件: Node、ピン留めされたLeanツールチェーン、OCaml、およびDune（producerガイド）。その後：

make setup # node依存関係
make build # Lean verifierとOCaml producer
make check FILE=pipeline/examples/array-last-element.ts

make checkは、結果と実行ドキュメントを保持するディレクトリ（ソース、パーサーの出力、producerのclaims、証明書）を表示します。

開発

make test # 高速チェックとコントロール（偽造ドキュメントとclaims）
make suite # すべてのパイプラインケース：期待される結果を持つソースファイル
make help # すべてのターゲット

次を読む

• DESIGN: 原則、アーキテクチャ、信頼の表面積、およびすべてのドキュメントのドキュメントマップ。
• SEMANTICS, POSITIVE-TYPES, PROGRAM-TYPING: calculus、その型、およびその型付け規則。
• SOURCE-MODEL, SOURCE-ELABORATION, SOURCE-CONTRACTS, SOURCE-FRAGMENT: TypeScriptの値と操作がcalculusにどのようにマッピングされるか、各ソース形式がどのように低下するか、型とライブラリ契約がどのように読み取られるか、そしてフラグメントが何を拒否するか。
• AGENTS: プロジェクトを変更するためのルール：変更は何を運ぶ必要があるか、どのテストを維持するか、コミットがどのように記録されるか。
• WORK: 未完了の作業とそのステータス。
• パイプラインケース: サポートされているすべての構成要素（肯定的および否定的）の作業例。
• REFERENCES: TScertが依拠している作業。

ライセンス

NON-AI MIT Licenseの下でライセンスされています。MITの条件に、コードが機械学習システムのトレーニングや改善、またはそのトレーニングのためのデータセットでの使用から除外されるという条項が付加されています。著作権者は、EU指令2019/790第4条(3)に基づき、機械学習システムのトレーニングや改善のためであっても、テキストおよびデータマイニングに対してこのリポジトリ内の権利を留保します。ai.txtは、同じ予約を機械可読形式で示しています。

著作権者は、EU指令2019/790第4条(3)に基づき、機械学習システムのトレーニングや改善のためであっても、テキストおよびデータマイニングに対してこのリポジトリ内の権利を留保します。ai.txtは、同じ予約を機械可読形式で示しています。