TypeScript で実装したワークフローの「正しさ」を Lean とランダムテストで検証する

TypeScript は、ワークフローのような処理を少量のコードで書けます。
たとえば「あるノードから次のノードへ進む」という処理だけなら、数十行で実装できます。

一方で、実装の規模が大きくなると、次のような不安が出てきます。

• ワークフローを扱う関数の間で、ワークフローに期待する意味がずれていないか
• テストしていない入力で、想定外の振る舞いをしないか
• 実装を変更したとき、以前満たしていた性質を壊していないか

この記事では、非常に小さなワークフローを題材にして、定理証明支援系 Lean を使い、TypeScript 実装が Lean で書いた基準となるモデルと一致するかを検査する方法を紹介します。

この記事で行うのは、TypeScript の実装そのものを Lean で完全に証明することではありません。

より具体的には、以下の構成になっています。

1. TypeScript でワークフローを実装する
2. Lean でも同じ仕様を、小さく読みやすい形で定義する
3. Lean 側のモデルが期待する基本的な性質を持つことを証明する
4. TypeScript 実装と Lean で実装されたモデルの出力を、ランダムに生成した入力で比較する
5. その比較を CI で継続的に実行する

つまり、Lean が直接保証するのは、Lean で書いた基準となるモデルの性質です。

TypeScript 実装については、その Lean モデルと多くの入力で一致することを Differential Random Testing で継続的に確認します。

「なら Lean で製品を実装すればよいのでは？」と思うかもしれませんが、パフォーマンス、エコシステム、デバッグ容易性などの理由から、製品の実装は TypeScript や Rust などで行い、Lean は形式化・証明などのために使い分けるのが現実的な選択肢となります。

この考え方は、AWS のポリシー言語 Cedar の開発で使われている方法を参考にしています。
Cedar は Lean で書いた形式化と証明、Rust 実装との差分を検査する仕組みを利用しています。

以下では Lean 4 を前提に説明を行います。

小さなワークフローを TypeScript と Lean で表す

今回扱うワークフロー

題材とするワークフローは、かなり単純なものです。

各ノードは、次のノードを 0 個または 1 個だけ持てることにします。

たとえば、次のようなワークフローは扱えます。

A ──▶ B ──▶ C

一方で、次のような分岐は扱いません。

    ┌──▶ B
A ──┤
    └──▶ C

今回の目的は、実用的なワークフローエンジンを完全に形式化することではなく、TypeScript と Lean をどのように接続できるか、その考え方を理解することのため、このように単純化しています。

また、Lean による証明コードは、一般的なプログラミング言語のコードに対して数倍以上になり得ます。題材のワークフローの規模でも、解説にはそれなりの紙幅を割かねばなりません。

今回確認したい性質は、次の 1 つです。

あるノード a から b への辺があり、同時に c への辺もあるなら、b = c である。

言い換えると、

同じノードから出る辺の行き先は一意である。

という性質です。

ただし、ここで証明するのは TypeScript 実装そのものの性質ではありません。
Lean 上でワークフローを Node → Option Node としてモデル化したとき、そのモデルが持つ基本的な性質を証明します。

TypeScript でワークフローを実装する

まず TypeScript で小さなワークフローを実装します。

type Node = {
  id: number
}

type Workflow = (node: Node) => Node | null

const next = (w: Workflow, node: Node): Node | null => {
  return w(node)
}

const hasEdge = (w: Workflow, from: Node, to: Node): boolean => {
  const nextNode = w(from)
  return nextNode !== null && nextNode.id === to.id
}

Workflow は、ノードを受け取り、次のノードがあれば返す関数です。
次のノードがなければ null を返します。

type Workflow = (node: Node) => Node | null

これは直感的には、次のような対応を表しています。

node ──▶ next node

ここでの Workflow は、同じ入力に対して常に同じ結果を返し、外部状態を変更せず、例外を投げない純粋な関数であると仮定します。

TypeScript の型だけではこの性質を強制できません。

たとえば、次のような関数も TypeScript の型上は Workflow です。

let toggle = false

const badWorkflow: Workflow = () => {
  toggle = !toggle
  return toggle ? { id: 1 } : { id: 2 }
}

この badWorkflow は、同じ入力に対して異なる結果を返す可能性があります。
そのため、Lean の Node → Option Node が表す数学的な関数とは対応しません。

next は、ワークフローにノードを渡して次のノードを得るだけです。

const next = (w: Workflow, node: Node): Node | null => {
  return w(node)
}

hasEdge は、あるノード from から別のノード to への辺があるかを判定します。

const hasEdge = (w: Workflow, from: Node, to: Node): boolean => {
  const nextNode = w(from)
  return nextNode !== null && nextNode.id === to.id
}

ここでは Node 同士を直接比較せず、id を比較しています。

次に、具体的なノードとワークフローを定義します。

const nodeA: Node = { id: 0 }
const nodeB: Node = { id: 1 }
const nodeC: Node = { id: 2 }

const exampleWorkflow: Workflow = (node) => {
  switch (node.id) {
    case 0:
      return nodeB
    case 1:
      return nodeC
    default:
      return null
  }
}

これは次のワークフローを表しています。

A ──▶ B ──▶ C

簡単な確認は、一般的なテストで書けます。

expect(next(exampleWorkflow, nodeA)?.id).toBe(nodeB.id)
expect(next(exampleWorkflow, nodeB)?.id).toBe(nodeC.id)
expect(next(exampleWorkflow, nodeC)).toBeNull()

expect(hasEdge(exampleWorkflow, nodeA, nodeB)).toBe(true)
expect(hasEdge(exampleWorkflow, nodeA, nodeC)).toBe(false)

しかし、これだけではいくつかの具体例を試しただけです。

「この形のワークフローなら、あるノードから出る辺は高々 1 つである」という一般的な性質を確認したわけではありません。

そこで Lean を使います。

Lean でワークフローを定義する

Lean では、まず Node を定義します。

structure Node where
  id : Nat
deriving DecidableEq, Repr

TypeScript の次の定義に近いものです。

type Node = {
  id: number
}

ただし、Lean の Nat は自然数、つまり 0 から始まる整数です。

TypeScript の number は -1、1.5、NaN、Infinity なども表せますが、Lean の Nat は非負整数だけです。（この違いは、後で TypeScript と Lean を比較するときに重要になります。）

また、今回の Node は id だけを持つため、Lean における b = c は実質的に b.id = c.id と同じ意味になります。

将来 Node に label など別のフィールドを追加した場合、Lean の構造体としての等値性はすべてのフィールドの一致を要求します。

その場合、TypeScript 側で id だけを比較している実装とは意味が一致しなくなるため、ノードの同一性を別途 sameNode のような述語として定義する必要があります。

次に、ワークフローを定義します。

abbrev Workflow := Node → Option Node

Lean の Option Node は、TypeScript の Node | null に相当します。

abbrev は既存の式に読みやすい名前をつけるコマンドです。^[1]

対応は次のとおりです。

TypeScript	Lean
Node | null	Option Node
null	none
node	some node

Lean の記法に慣れない場合は、Option が Node を「包んでいる」と捉えると、理解しやすいかもしれません。

つまり、

abbrev Workflow := Node → Option Node

は、

ノードを受け取り、次のノードがあれば some nextNode、なければ none を返す関数

という意味です。

TypeScript の Workflow と並べると、かなり近い形になっています。

type Workflow = (node: Node) => Node | null

abbrev Workflow := Node → Option Node

次に、next と HasEdge を定義します。

namespace Workflow

def next (w : Workflow) (a : Node) : Option Node :=
  w a

def HasEdge (w : Workflow) (a b : Node) : Prop :=
  w a = some b

end Workflow

next は単に w a を返すだけです。

def next (w : Workflow) (a : Node) : Option Node :=
  w a

HasEdge は、a の次が b であることを表します。

def HasEdge (w : Workflow) (a b : Node) : Prop :=
  w a = some b

ここでは Workflow 名前空間の中で next と HasEdge を定義しています。

TypeScript では hasEdge は boolean を返しました。

const hasEdge = (w: Workflow, from: Node, to: Node): boolean => {
  const nextNode = w(from)
  return nextNode !== null && nextNode.id === to.id
}

一方、Lean の HasEdge は Prop を返しています。

Prop は、実行時の真偽値というより、証明の対象になる命題です。^[2]
つまり、HasEdge w a b は、「w a = some b である」という命題を表しています。

Lean でワークフローの性質を証明する

HasEdge w の右一意性を証明する

ここからが Lean を使う理由です。

証明したい性質は次でした。

あるノード a から b への辺があり、同時に c への辺もあるなら、b = c である。

この性質は、二項関係の用語では右一意性（right uniqueness）と呼ばれます。
ワークフローにおいては、「各ノードの次ノードが高々 1 つである」、つまり遷移が決定的である、という性質です。

Lean では次のように書けます。

namespace Workflow

theorem HasEdge.right_unique
    (w : Workflow) (a b c : Node)
    (hab : HasEdge w a b)
    (hac : HasEdge w a c) :
    b = c := by
  unfold HasEdge at hab hac
  rw [hab] at hac
  exact Option.some.inj hac

end Workflow

順に見ていきます。

theorem HasEdge.right_unique
    (w : Workflow) (a b c : Node)
    (hab : HasEdge w a b)
    (hac : HasEdge w a c) :
    b = c := by

これは次の意味です。

任意のワークフロー w とノード a, b, c について、

hab : HasEdge w a b

つまり a から b への辺があり、

hac : HasEdge w a c

つまり a から c への辺もあるなら、

b = c

が成り立つ、という定理です。

証明本体は次の 3 行です。

  unfold HasEdge at hab hac
  rw [hab] at hac
  exact Option.some.inj hac

まず、

unfold HasEdge at hab hac

で HasEdge の定義を展開します。

ここで使っている unfold は Lean の tactic です。

tactic とは、「式を書き換える」「補題を適用する」などの操作を Lean に指示し、証明を対話的に進めるためのコマンドです。

Lean の証明は、tactic を使わずに項として直接書くこともできますが、複雑な証明では tactic を使う方が、人間の証明手順に近い形で書きやすくなります。

HasEdge w a b は、定義上、

w a = some b

でした。

そのため、展開後は次のようになります。

hab : w a = some b
hac : w a = some c

次に、

rw [hab] at hac

で、hac の中に出てくる w a を、hab を使って some b に書き換えます。

rw は等式や同値を [] 内の式で置き換える tactic です。

もともと hac は、

hac : w a = some c

でした。

hab により w a = some b なので、書き換え後は、

hac : some b = some c

になります。

最後に、

exact Option.some.inj hac

を使います。

exact はゴールそのものを証明する項を与えて証明を閉じる tactic です。

Option.some.inj は Option.some コンストラクタの単射性（injectivity）を表す定理であり、直感的には次の性質です。

some b = some c → b = c

some b と some c が等しいなら、中身の b と c も等しい、ということです。

これで b = c が得られます。

この定理により、Workflow := Node → Option Node について、

同じノードから出る辺の行き先は一意である

ことが証明できました。

ただし、この性質は Workflow := Node → Option Node というモデル化を選んだ時点で、かなり自然に得られる性質です。

つまり、今回の証明は TypeScript 実装の正しさを直接証明しているというより、まず Lean 上でワークフローをどのような数学的対象として扱うかを明確にし、そのモデルが期待する基本的な性質を持つことを確認するものです。

next と HasEdge の対応も確認する

次に、next と HasEdge が同じ意味を持つことも確認しておきます。

namespace Workflow

theorem hasEdge_iff_next_eq_some
    (w : Workflow) (a b : Node) :
    HasEdge w a b ↔ next w a = some b := by
  rfl

end Workflow

これは、

next w a = some b と HasEdge w a b が同値である

という意味です。

つまり、HasEdge w a b が成り立つなら next w a = some b が成り立ち、その逆も同様です。

ここで使っている証明は rfl だけです。

rfl は反射性（reflexivity）、つまり「定義を展開すれば両辺が同じ形になる」ことを示す証明です。

今回の定義をもう一度見ると、next は次のように定義されています。

def next (w : Workflow) (a : Node) : Option Node :=
  w a

また、HasEdge は次のように定義されています。

def HasEdge (w : Workflow) (a b : Node) : Prop :=
  w a = some b

したがって、

next w a = some b

は、next の定義を展開すると、

w a = some b

になります。

一方で、

HasEdge w a b

も、HasEdge の定義を展開すると、

w a = some b

になります。

つまり、左右はどちらも同じ命題に展開されます。

そのため Lean は、追加の推論を必要とせず、rfl だけでこの同値を確認できます。

この定理により、HasEdge w a b という命題は、next w a = some b と同じ内容を表していることが明示されました。

言い換えると、HasEdge は next とは別の意味を持つ新しい関係ではなく、next の結果を「辺がある」という言葉で読み替えたものです。

Lean 側では、このようにして操作と命題の対応を明示できます。

Lean でも具体例を確認する

TypeScript と同じように、Lean でも A → B → C を定義します。

def nodeA : Node := { id := 0 }
def nodeB : Node := { id := 1 }
def nodeC : Node := { id := 2 }

def exampleWorkflow : Workflow :=
  fun n =>
    match n.id with
    | 0 => some nodeB
    | 1 => some nodeC
    | _ => none

そして、期待する性質を確認します。

example : Workflow.next exampleWorkflow nodeA = some nodeB := by
  rfl

example : Workflow.next exampleWorkflow nodeB = some nodeC := by
  rfl

example : Workflow.next exampleWorkflow nodeC = none := by
  rfl

example : Workflow.HasEdge exampleWorkflow nodeA nodeB := by
  rfl

example : ¬ Workflow.HasEdge exampleWorkflow nodeA nodeC := by
  simp [Workflow.HasEdge, exampleWorkflow, nodeA, nodeB, nodeC]

rfl は、先に述べたように「定義を展開すれば左右が同じである」という証明です。

たとえば、

example : Workflow.next exampleWorkflow nodeA = some nodeB := by
  rfl

は、next と exampleWorkflow と nodeA の定義を展開すると、

some nodeB = some nodeB

になるため、rfl で証明できます。

最後の例だけは否定命題です。

example : ¬ Workflow.HasEdge exampleWorkflow nodeA nodeC := by
  simp [Workflow.HasEdge, exampleWorkflow, nodeA, nodeB, nodeC]

これは、nodeA から nodeC への辺は存在しない、という意味です。

HasEdge exampleWorkflow nodeA nodeC を展開すると、

exampleWorkflow nodeA = some nodeC

です。

しかし exampleWorkflow nodeA は some nodeB なので、これは成り立ちません。

simp は、Lean が知っている標準的な書き換え規則を使って、目標や仮定を自動でより単純な形に整理する tactic です。

simp [Workflow.HasEdge, exampleWorkflow, nodeA, nodeB, nodeC]

のように書くと、角括弧内の定義を展開しながら、式を自動的に簡単な形へ書き換えます。

この例では、HasEdge、exampleWorkflow、各ノードの定義を展開し、

¬ Workflow.HasEdge exampleWorkflow nodeA nodeC

という目標について、exampleWorkflow nodeA が some nodeB に簡約され、some nodeB = some nodeC が成り立たないことまで simp が処理します。

ここまでで何が言えたのか

ここまでで言えたことは、次のとおりです。

まず、Lean で書いたワークフローについては、

abbrev Workflow := Node → Option Node

という形により、各ノードに対して返る値は none または some node のどちらか 1 つになります。

さらに、

theorem Workflow.HasEdge.right_unique ...

により、

同じノードから出る辺の行き先は一意である

ことを Lean で証明しました。

ただし、これは Lean 側のモデルについての性質です。
まだ TypeScript 実装そのものについては証明していません。

たとえば TypeScript 側で、誤って次のような実装をしても、Lean の証明は壊れません。

export const hasEdge = (w: Workflow, from: Node, to: Node): boolean => {
  const nextNode = w(from)
  // バグ: to を見ていない
  return nextNode !== null
}

この実装では、nodeA の次が nodeB であっても、hasEdge(exampleWorkflow, nodeA, nodeC) が true になってしまいます。

このケースは、TypeScript の単純なテストやコードレビューでも防げます。
しかし、コードが大規模化したら、厳格な安全性が必要になったら、そのようなテストでは見落とすケースが出てくるかもしれません。

Lean の証明は Lean のコードに対して成立しているだけです。
TypeScript のコードが Lean で書いた定義と同じ振る舞いをしているかは、別途確認する必要があります。

そこで Differential Random Testing を行います。

Differential Random Testing で TypeScript と Lean を比較する

TypeScript 実装が Lean モデルに一致しているか比較する

Differential Random Testing は、同じ入力を複数の実装に与え、その出力が一致するかを比較する方法です。

今回であれば、比較対象は次の 2 つです。

1. TypeScript 実装
2. Lean で書いた、基準となる実装

構成は次のようになります。

random input
    │
    ├──▶ TypeScript implementation ──▶ output1
    │
    └──▶ Lean model ─────────────────▶ output2

compare output1 output2

ランダムにワークフローとクエリを生成し、TypeScript と Lean の両方に渡します。
両方が同じ結果を返せば、その入力については一致していると判断できます。

Cedar の開発でも、Lean で書いたモデルで重要な性質を証明し、製品コードとの一致を Differential Random Testing で確認しています。^[3]

ただし、今回の Lean 実装には少し問題があります。

abbrev Workflow := Node → Option Node

この形は定義としては綺麗ですが、ランダムテストの入力としては扱いにくいです。
関数そのものを JSON として生成するのは手間がかかるためです。

そこで、テスト用にはワークフローを JSON で表せる形にします。

ランダムテスト用の JSON 形式

テスト時には、ワークフローを辺のリストとして表します。

type WorkflowJson = {
  edges: Array<{ from: number; to: number }>
}

たとえば、

{
  "edges": [
    { "from": 0, "to": 1 },
    { "from": 1, "to": 2 }
  ]
}

は、

0 ──▶ 1 ──▶ 2

を表します。

以降では、edges の from が重複しないものを well-formed な WorkflowJson と呼びます。

今回比較対象にするのは、well-formed な WorkflowJson だけです。
from が重複する JSON は、今回のワークフローモデルの入力としては不正とみなします。

たとえば、次のような入力は well-formed ではありません。

{
  "edges": [
    { "from": 0, "to": 1 },
    { "from": 0, "to": 2 }
  ]
}

この JSON は、0 から 1 にも 2 にも進めるように見えます。
しかし今回のモデルでは、各ノードの次ノードは高々 1 つです。

したがって、ランダム生成器は from が重複しない入力だけを作るか、生成後に重複を取り除く必要があります。
実運用で外部から JSON を受け取る場合は、明示的に検証するのが安全です。

function isNodeId(id: number): boolean {
  return Number.isSafeInteger(id) && id >= 0
}

function isWellFormedWorkflow(wf: WorkflowJson): boolean {
  const seen = new Set<number>()

  for (const edge of wf.edges) {
    if (!isNodeId(edge.from) || !isNodeId(edge.to)) {
      return false
    }

    if (seen.has(edge.from)) {
      return false
    }

    seen.add(edge.from)
  }

  return true
}

クエリは、たとえば次の 2 種類にします。

type Query =
  | { kind: "next"; node: number }
  | { kind: "hasEdge"; from: number; to: number }

next は、指定したノードの次を返します。

{ "kind": "next", "node": 0 }

hasEdge は、指定した辺が存在するかを返します。

{ "kind": "hasEdge", "from": 0, "to": 1 }

Lean 側ではノード ID を Nat として扱うため、比較対象にする TypeScript の入力も非負整数に制限します。

実際に TypeScript の number を受け取る場合は、少なくとも次の条件を満たす値だけを Lean モデルとの比較対象にする必要があります。

• Number.isSafeInteger(id) が true
• id >= 0
• NaN や Infinity ではない

今回のランダムテストでは、生成する ID の範囲をさらに小さくし、たとえば 0 から 100 までに制限します。

これは「TypeScript のすべての number と Lean のすべての Nat を比較する」という意味ではありません。

あくまで、比較対象にする入力領域を明示的に決め、その範囲で TypeScript 実装と Lean モデルの一致を確認する、という意味です。

TypeScript 側の比較用実装

JSON 形式に対する TypeScript 実装は、たとえば次のように書けます。

type Node = {
  id: number
}

type Workflow = (node: Node) => Node | null

type WorkflowJson = {
  edges: Array<{ from: number; to: number }>
}

type Query =
  | { kind: "next"; node: number }
  | { kind: "hasEdge"; from: number; to: number }

type Output =
  | { kind: "node"; value: number | null }
  | { kind: "bool"; value: boolean }

export const next = (w: Workflow, node: Node): Node | null => {
  return w(node)
}

export const hasEdge = (w: Workflow, from: Node, to: Node): boolean => {
  const nextNode = w(from)
  return nextNode !== null && nextNode.id === to.id
}

export const workflowFromJson = (wf: WorkflowJson): Workflow => {
  return (node: Node) => {
    const edge = wf.edges.find((edge) => edge.from === node.id)
    return edge ? { id: edge.to } : null
  }
}

export const evalQuery = (wf: WorkflowJson, query: Query): Output => {
  if (!isWellFormedWorkflow(wf)) {
    throw new Error("WorkflowJson is not well-formed")
  }

  const workflow = workflowFromJson(wf)

  switch (query.kind) {
    case "next": {
      const result = next(workflow, { id: query.node })
      return { kind: "node", value: result === null ? null : result.id }
    }

    case "hasEdge":
      return {
        kind: "bool",
        value: hasEdge(
          workflow,
          { id: query.from },
          { id: query.to }
        )
      }
  }
}

ここで比較対象にしているのは、任意の TypeScript 関数としての Workflow ではありません。
WorkflowJson から構築される workflowFromJson です。

workflowFromJson は、同じ wf と同じ node に対して同じ結果を返します。
そのため、Lean 側の Node → Option Node というモデルと対応させやすくなります。

Lean 側にも同じ JSON 入力を受け取り、同じ JSON 出力を返す小さな CLI を用意します。

この記事では Lean の JSON パーサ部分までは扱いません。
本質は、Lean と TypeScript の両方が同じ入力を受け取り、同じ結果を返すようにすることです。

比較する出力は、次のように単純にします。

type Output =
  | { kind: "node"; value: number | null }
  | { kind: "bool"; value: boolean }

たとえば、

{ "kind": "node", "value": 1 }

または、

{ "kind": "bool", "value": true }

のような形です。

fast-check でランダム入力を作る

TypeScript 側では、fast-check のような property-based testing ライブラリを使うと、ランダム入力を生成しやすくなります。

import fc from "fast-check"

const nodeIdArb = fc.integer({ min: 0, max: 100 })

Lean の Nat と対応させるため、ここでは非負整数だけを生成します。
また、0 から 100 までの安全な整数に制限しているため、NaN、Infinity、小数、負数は生成されません。

ワークフローを生成します。

const workflowArb = fc
  .array(
    fc.record({
      from: nodeIdArb,
      to: nodeIdArb,
    }),
    { maxLength: 20 }
  )
  .map((edges) => {
    const seen = new Set<number>()
    const uniqueEdges: Array<{ from: number; to: number }> = []

    for (const edge of edges) {
      if (!seen.has(edge.from)) {
        seen.add(edge.from)
        uniqueEdges.push(edge)
      }
    }

    return { edges: uniqueEdges }
  })

ここでは、まず適当な辺リストを作り、その後 from が重複しないようにしています。
これにより、生成される WorkflowJson は well-formed になります。

クエリもランダムに作ります。

const queryArb = fc.oneof(
  nodeIdArb.map((node) => ({ kind: "next" as const, node })),
  fc.record({
    kind: fc.constant("hasEdge" as const),
    from: nodeIdArb,
    to: nodeIdArb,
  })
)

そして、Lean 側をテストオラクル^[4]として結果を比較します。

fc.assert(
  fc.asyncProperty(workflowArb, queryArb, async (wf, query) => {
    const tsOutput = evalQuery(wf, query)
    const leanOutput = await runLeanModel({ workflow: wf, query })

    expect(tsOutput).toEqual(leanOutput)
  })
)

runLeanModel は、Lean 側の CLI を呼び出す関数です。

イメージとしては、次のような処理です。

async function runLeanModel(input: {
  workflow: WorkflowJson
  query: Query
}): Promise<Output> {
  // 1. input を JSON として Lean CLI に渡す
  // 2. Lean CLI から JSON 出力を受け取る
  // 3. JSON.parse して Output として返す
}

この比較により、ランダムに生成された多数の入力について、TypeScript 実装と Lean モデルの出力が一致するかを確認できます。

CI で継続的に実行する

この仕組みは、CI で実行して価値が生まれます。

たとえば GitHub Actions では、次のような構成にできます。

name: workflow-drt

on:
  pull_request:
    branches:
      - main
  push:
    branches:
      - main
  schedule:
    - cron: "0 0 * * *"
  workflow_dispatch:

jobs:
  drt:
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v4

      - uses: pnpm/action-setup@v4
        with:
          version: 10

      - uses: actions/setup-node@v4
        with:
          node-version: 24
          cache: pnpm

      - name: Install pnpm dependencies
        run: pnpm install --frozen-lockfile

      - name: Install Lean
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

      - name: Build Lean code
        run: lake build

      - name: Run differential random tests
        run: pnpm test

プルリクエストの作成・マージなどのタイミングや、定期実行で次を確認します。

1. Lean 側のコードがビルドできるか
2. TypeScript のテストが通るか
3. ランダムに生成された入力で、TypeScript と Lean の結果が一致するか

ランダムテストで大事なのは、失敗した入力を必ず再現できるようにすることです。

そのため失敗時には少なくとも次の情報をログに残します。

• seed
• 失敗した workflow
• 失敗した query
• TypeScript の出力
• Lean の出力

たとえば、次のようなログが出ると調査しやすくなります。

{
  "seed": 12345,
  "workflow": {
    "edges": [
      { "from": 0, "to": 1 },
      { "from": 1, "to": 2 }
    ]
  },
  "query": {
    "kind": "hasEdge",
    "from": 0,
    "to": 2
  },
  "typescriptOutput": {
    "kind": "bool",
    "value": true
  },
  "leanOutput": {
    "kind": "bool",
    "value": false
  }
}

この場合、TypeScript 実装、Lean 側の実装、JSON 変換層のどこかに不一致があります。

何が検証されたのか

どこまで信頼できるか

この方法では、Lean 側の定義が設計者の意図した仕様を表していること、Lean のカーネルが証明を正しくチェックしていることを信頼しています。

また、TypeScript と Lean 間の JSON 変換の正しさや、ランダム入力の生成器が確認したい入力領域を十分にカバーしていることも前提としています。

一方で、任意の TypeScript 関数が純粋であること、TypeScript 実装がすべての可能な入力で Lean モデルと一致することは保証しません。

JSON 変換にエラーが無いこと、そもそも Lean 側の仕様が本当に十分であるかは不明です。

したがって、この方法は完全な形式検証ではなく、Lean モデルの検証と、TypeScript 実装との差分テストを組み合わせた検査手法です。

この方法で検証されること

この構成で検証されることは、主に 2 つです。

1 つ目は、Lean で書いた定義が、Lean で証明した性質を満たすことです。

今回であれば、

同じノードから出る辺の行き先は一意である

という性質を、Lean 側のモデルについて証明しました。

2 つ目は、ランダムに生成された多数の入力について、TypeScript 実装と Lean モデルの出力が一致したことです。

これは通常のユニットテストを補完します。
特に、生成器が多様な入力を作れる場合、人間が列挙しにくいケースを継続的に試せる点に利点があります。

また、CI に組み込むことで、テストケースのサンプル数を増やしたり、実装変更による振る舞いの変化を早く検出できたりします。

この方法で検証されないこと

一方で、この方法も万能ではありません。

まず、TypeScript 実装がすべての入力で Lean モデルと一致することを数学的に証明しているわけではありません。
Differential Random Testing はあくまでテストです。

ランダムに生成された入力では一致していても、未生成の入力で不一致がある可能性は残ります。
CI はこのリスクを低減することが主な目的です。

また、Lean で書いた定義がほしい意味を表しているかも、Lean は判断しません。
その形式化は意図と異なる可能性があります。

Lean は、与えられた定義と命題に対して、証明が正しいかを確認してくれます。
しかし、「そもそもその命題を証明すれば十分なのか」は、設計者が考える必要があります。

さらに、JSON 変換層にもエラーが混入し得ます。
TypeScript から Lean に渡す入力のエンコード、Lean から返ってくる出力のデコードが間違っていれば、比較結果も信用できません。

この記事の方法は「TypeScript 実装の正しさを Lean で完全に証明する」ものではありません。

あくまで、

• 期待する振る舞いを Lean で定義し、その定義について重要な性質を証明する
• さらに TypeScript 実装が Lean モデルと一致することを、ランダムテストで継続的に検査する

ものであることに留意してください。

まとめ

この記事では、各ノードが次のノードを高々 1 つだけ持つ小さなワークフローを題材に、Lean での形式化と特定の性質の証明を行い、TypeScript 実装とのずれをランダムテストで検出する方法を紹介しました。

TypeScript 側では、ワークフローを次のように表しました。

type Workflow = (node: Node) => Node | null

Lean 側では、対応する考え方を次のように定義しました。

abbrev Workflow := Node → Option Node

そして Lean で、

theorem Workflow.HasEdge.right_unique ...

を証明することで、Lean 側のモデルにおいて、同じノードから出る辺の行き先が一意であることを確認しました。

ただし Lean が直接証明しているのは、Lean で書いたモデルの性質です。
TypeScript 実装そのものがすべての入力で正しいことを証明しているわけではありません。

そこで、TypeScript 実装と Lean モデルに同じランダム入力を与え、出力を比較する Differential Random Testing を使います。
それを CI の組み込むことで、実装の一致をより確かなものとします。

あくまで、Lean で仕様を形式化、それが期待する性質を持つことを証明し、TypeScript など他の言語の実装が Lean モデルに準拠していることを確かめ続けるだけです。

それでも数学的な証明を土台に、より信頼性の高いソフトウェアを作ることができます。

最後に

AI Shift はエンジニアの採用に力を入れています！
少しでも興味を持っていただけましたら、カジュアル面談でお話しませんか？
（オンライン・19時以降の面談も可能です）

【面談フォームはこちら】
https://hrmos.co/pages/cyberagent-group/jobs/1826557091831955459

脚注

1. 公式リファレンスでは "Abbreviations are identical to definitions with def, except they are reducible."（略称は、def による定義と同一ですが、ただし reducible、つまり簡約・展開可能である点が異なります）と記載されています。

2. https://lean-lang.org/theorem_proving_in_lean4/Propositions-and-Proofs/

3. https://arxiv.org/abs/2407.01688

4. https://en.wikipedia.org/wiki/Test_oracle