エディタと言語サーバーは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 から読みます。 指摘はdocs/rules.mdの80種類です。 仕様が禁じることは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のコードは、ビルドのときに証明が検査され、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にあります。