エディタと言語サーバーはLanguage Server Protocol、略してLSPで通信します。いろいろなエディタと言語サーバーを使っていて、どれも仕様の細かいところを少しずつ外しているように感じていました。ところが、LSPには公式の適合テストがありません。サーバーの一部を検査する道具はありますが、クライアントを検査する道具は見つかりませんでした。

そこで、仕様に厳格なクライアントとサーバーを作り、通信が仕様どおりかを判定できるようにしました。判定の核になる計算はLean 4で書いて正しさを証明し、lean-rsでRustに変換しています。これを5つのエディタとrust-analyzerにつないだところ、思っていたとおり、どれにも仕様に反する動きがありました。

作った道具はlsp-touchstoneです。リポジトリはconao3/rust-lsp-touchstoneで、ライセンスはApache-2.0です。この記事は0.1.0で動かした結果をもとに書いています。

作ったもの

lsp-touchstoneには3つの動かし方があります。

• clientはブラウザのweb UIから言語サーバーを起動し、リクエストや通知を手で送ります。
• proxyはエディタと言語サーバーのあいだに入り、すべてのメッセージを検査しながら中継します。
• serverはエディタの言語サーバーとして動き、仕様にあるサーバーからのリクエストと通知を順に送ります。

3つとも同じ検査を使います。検査に使う型と、各メソッドがどのcapabilityに対応するかは、LSP 3.18の仕様のメタモデル metaModel.json から読みます。指摘は80種類あり、一覧はdocs/rules.mdにあります。仕様が禁じることはerrorにし、仕様が許していても実装によって読み方が分かれることはwarningにしています。

Leanで証明した部分

判定する側が間違っていると、指摘も信用できません。そこで、計算を間違えやすい3つの部分をLeanで書き、性質を証明しました。

• LSPの位置は行と文字のオフセットで表し、UTF-8、UTF-16、UTF-32のどの単位で文字を数えるかを初期化のときに決めます。 😀 はUTF-32では1、UTF-16では2、UTF-8では4と数えます。単位のあいだの変換について、往復すると元に戻ることと、文字の途中を指す位置を見分けられることを証明しています。
• didChange で届いた変更を、手元に持つ文書の写しに当てて範囲を置き換える計算です。範囲の前後が残ること、新しい文字列がその位置に入ること、長さが期待どおりになることを証明しています。
• 進捗の状態の移り方です。サーバーは進捗を begin 、何回かの report 、 end の順に送ります。

進捗の部分は次のように書いています。TokenState と ProgressKind の型の定義と、ほかの定理は省いています。lean! の中のコードは、ビルドのときにLeanが証明を検査し、lean-rsがRustの関数にします。

lean_rust::lean! {
    pub mod proved;
    r#"
    def step : TokenState → ProgressKind → Option TokenState
      | .created, .begin => some .begun
      | .begun, .report => some .begun
      | .begun, .finish => some .ended
      | _, _ => none

    theorem ended_accepts_nothing (k : ProgressKind) : step .ended k = none := by
      cases k <;> rfl
    "#
}

ended_accepts_nothing は、 end のあとはどの進捗も受け付けないことを示しています。proxyは進捗の通知を受けるたびにこの step を呼び、 none が返ったら違反として報告します。

見つかった仕様違反

make check-editors を実行すると、eglot、lsp-mode、Neovim、Helix、VS Codeを人の操作なしに動かします。それぞれのエディタを、lsp-touchstoneのserverと、proxyを通したrust-analyzerに別々につなぎます。そのうえで、hover、補完、定義へのジャンプ、1行の入力、コードアクションによる編集、保存、終了の順に操作します。エディタとrust-analyzerはnixpkgsから入れました。バージョンは次のとおりです。

• Emacs 31.1、eglot 1.24.31、lsp-mode 20261020.1728
• Neovim 0.12.6
• Helix 25.07.1
• VS Codeのクライアントのライブラリ vscode-languageclient 11.0.0。VS Codeをソースからビルドして配布しているVSCodium 1.143.17183で動かしました。
• rust-analyzer 2026-11-02

終わり方

LSPでは、クライアントが shutdown を送り、応答を受けてから exit を送って終わります。shutdown を送ったあとのクライアントは、 exit のほかにリクエストも通知も送ってはいけません。6つの実装は、それぞれ違う形でこの手順から外れていました。「回によって」と書いたものは、何回か実行したうちの一部で出たものです。

• eglotは exit に "params": {} を付けて送ります。 exit はparamsを持たない通知なので、warningにしています。
• lsp-modeは exit を送らずにサーバーのプロセスを終わらせ、回によっては "params": null を付けた exit を送ります。JSON-RPC 2.0のparamsはオブジェクトか配列で、 null は仕様に合いません。
• Neovimはrust-analyzerとつないだとき、回によって shutdown のあとに textDocument/semanticTokens のリクエストを送ります。
• VS Codeのクライアントは回によって shutdown のあとに $/cancelRequest を送ります。
• Helixは回によって exit が届く前にサーバーのプロセスを終わらせます。
• rust-analyzerはクライアントから受けたリクエストに答えないまま shutdown に応答し、終了します。

宣言していない機能

LSPでは、クライアントとサーバーが initialize で、自分が扱える機能をcapabilityとして宣言します。相手が宣言していない機能のリクエストは、送っても相手が扱えるとは限りません。

clientのweb UIでrust-analyzerを起動し、初期化してからファイルを1つ開くと、次の指摘が出ます。

rust-analyzerが workspace/diagnostic/refresh のリクエストを送っています。仕様はこのリクエストに対応するクライアントのcapabilityを workspace.diagnostics.refreshSupport と定めていて、lsp-touchstoneのclientはこれを宣言していません。

rust-analyzerは5つのエディタのどれとつないでもこのリクエストを送りました。5つのエディタはどれも refreshSupport を宣言していません。それでも、eglot、lsp-mode、Neovim、VS Codeは "result": null で成功を返しました。Helixは「メソッドが見つからない」というエラーを返し、rust-analyzerはそのまま動き続けました。

ほかの振る舞い

• rust-analyzerは window/workDoneProgress/create の応答を受ける前に、そのtokenで進捗を送り始めることがあります。
• lsp-modeは、Emacsが最初の保存でファイルをバックアップの main.rs~ に改名するとき、 workspace/willRenameFiles をサーバーに送ります。
• serverは、位置を数える単位をクライアントが示した中から utf-32 、 utf-8 、 utf-16 の順に選びます。eglot、lsp-mode、Neovim、Helixでは utf-32 になり、VS Codeのクライアントは utf-16 しか示しません。

正しく動いたところ

serverはコードアクションから workspace/applyEdit でエディタに編集を送ります。そのあとエディタが送る didChange から文書の中身を計算し、送った編集を当てた文書と一致するかを確かめます。5つのエディタはすべて、編集を正しく適用しました。

編集の適用のように画面に結果が出る機能は、おかしければ使う人がすぐ気づきます。見つかった違反はどれもエディタを閉じる途中や、画面に何も出ないやりとりの中で起きていました。実際のエディタや言語サーバーは仕様に合わないメッセージを受けても止まらずに受け流すので、違反をした側には何も返りません。違反を見つけるには、受け流さずに指摘する相手が要ります。

使い方

proxyを起動するコマンドを、言語サーバーのコマンドとしてエディタに渡します。eglotなら次のように書きます。

(add-to-list 'eglot-server-programs
             '(rust-ts-mode . ("lsp-touchstone" "proxy" "run-proxy"
                               "--web-ui-port" "4318"
                               "--server-command-args" "rust-analyzer")))

--server-command-args のあとには、本来の言語サーバーのコマンドを書きます。 --web-ui-port を付けると、通信をその場で表示するweb UIのURLを標準エラーに出します。lsp-mode、Neovim、Helix、VS Codeの設定と、エディタごとの結果の詳細はdocs/editors.mdにあります。