ritsu

システムが守るべき決まりを小さな言語で書き、どんな入力にも答えが一つに決まるか、決まりどうしが食い違っていないかを確かめる。確かめた決まりから、コード、人が読むページ、テストに使う入力と答えの組やシナリオを生成できる。

コーディングエージェントは、人が一行ずつ読めるより速く、多くのコードを書くようになりました。そこで問いがはっきりします。誰が、あるいは何がコードを書いても、コードが実現すべきものは何か。サービスのあいだと中の契約。業務の規則。暦と期日。帳簿と、その上限と下限。ワークフローの骨組み。だれが何をしてよいか。要件がどこから来て、いま何がそれを満たしているか。

ritsu は、そのそれぞれに小さな言語を一つずつ与えます。どれも、人が読めるファイルです。各言語は、書いたことを確かめられるところまで確かめます。試しに選んだ例ではなく、すべての入力、すべての日、すべての道筋についてです。コードが要るところではコードを生成し、中身を理解したい人のためのページを作ります。九つが一つの処理系を共有しているので、証明が言語の境目で切れません。ワークフローは呼ぶ規則の前提を知り、規則は暦がとりうる日を知り、帳簿は規則が返しうる額を知っています。

つなぎのコードはエージェントが書き、コードが実現すべきものは ritsu が持ちます。

ブラウザで試す 全画面で試す GitHub

九つの言語

どの言語も、それだけで使えます。.flow を書かずに rulec だけを使うこともできます。一つのファイルに二つの言語を混ぜることはしません。運賃、暦、帳簿、ワークフローを読む人は、それぞれ違うからです。

• rulec では、規則を、表と、そのまわりの計算、例外、ただし書きで書きます。rulec check は、宣言した範囲のすべての入力に答えがちょうど一つあることを証明し、単位とお金を確かめ、Lean の証明が検査し直す証明書を書きます。検査を通った規則だけが、12 の言語の普通の関数になります。
• dandori では、ワークフローが何をどの順に呼ぶか、リトライとタイムアウト、呼び出しが外の案件（注文、支払い、予約）をどう動かすかを書きます。dandori check は、すべての道筋で、案件を手を付けないか終えるかのどちらかで残し、途中で放り出さないことを示します。同じファイルが、Temporal、Step Functions、Argo Workflows、Lambda の durable functions、pydantic-graph のコードになります。
• koyomi では、期日を、契約や法令の言い方のまま書きます。請求日から 30 日後、休みなら次の営業日、というふうにです。koyomi check は、宣言した範囲のすべての日について日付を計算し、書いた条件をその一日ずつで確かめます。検査を通ったファイルだけが、TypeScript、Python、Go、Rust、SQL のコードと、どのホストからも JSON のオブジェクト一つで呼べる Wasm のモジュールになります。
• chobo では、勘定と、それぞれが守る上限と下限、勘定のあいだの振替を書きます。振替、仮押さえ、期限切れをどう重ねても、勘定が上限と下限の外に出ないことを確かめ、PostgreSQL、TigerBeetle、MySQL の系統（MySQL、TiDB、Vitess）を使うクライアントを生成します。
• geas は、プログラムについての主張を一つずつ、動いているプログラム（コマンドライン、HTTP のサービス、ブラウザのページ）に当てて確かめ、差分を渡せば、それがどの主張にかかわるかを答えます。OpenSpec の仕様を渡せば、同じ名前の主張で確かめていないシナリオを挙げます。
• yuen では、要件ごとに、どこから来たか、誰が受け持つか、何が満たし何が確かめるかを書きます。どのリンクも両端のハッシュで固定されます。OpenSpec の仕様の要件も、同じように固定します。
• sakai では、どのコンテキストがどのファイルを持ち、誰が誰に依存してよいかを地図に書きます。コンテキストのあいだをまたぐ参照を、ここにあるすべての言語のファイルと、サービスが契約として持つ OpenAPI と AsyncAPI の文書と、コードについて確かめます。帳簿の use book は数えません。ほかのコンテキストからは、帳簿の前に立つサービスを通して使うからです。
• sekisho では、どの principal がどの resource にどの action をしてよいかを、ゲート（.gate のファイル）に書きます。条件には、役割、属性、関係のほかに、規則の答えと日付の答えを使えます。sekisho check は起こりうる組み合わせを全部たどり、どれも Cedar と同じ決まりで答えを決めます。検査を通ったゲートだけが、Cedar のスキーマとポリシーと、条件の値をサービス自身のデータから計算して Cedar に尋ねる TypeScript、Python、Go のコードになります。規則の答えがゲートから Cedar に届くまでを、sekisho のページで例に沿って読めます。
• kaname は、プログラムのうち入出力を持たない部分（Functional Core）を書く、小さな汎用の言語です。モジュール（.kn のファイル）には、イベントで状態を進める、入力を確かめて形を整える、辞書と集合で数を集めて比べる、木を作り替える、といった計算と、規則の入力を組み立て、一つの答えを次の呼び出しに渡し、額を帳簿に渡すコードを、ritsu の型で書きます。kaname check は、単位とお金、丸め、int64 を確かめ、渡す値がどれも相手の範囲に入るかを確かめます。total と書いた関数が、宣言した範囲のどの入力にも答えることも示します。ritsu gen は、ホストが呼ぶ TypeScript、Python、Go のコードを、呼ぶもののコードの横に書きます。kaname のページでは、書き方、TypeScript、Python、Go から呼ぶ Functional Core の四つの例、検査が保証すること、規則・日付・帳簿を呼ぶことを読めます。

言語が出会うところ

九つが一つの処理系を共有しているのは、ある言語が確かめたことを、別の言語が前提にできるようにするためです。たとえば返金の規則は、支払った額より多くを求める人はいない、と決めてかかっています。

rule refund_check v1
description "Whether a refund is paid at once or reviewed. A refund never asks for more than was paid, which the rule takes for granted"

enum path = at_once | review

inputs
  paid  : number  range >=0 <=10000
  asked : number  range >=0 <=10000

constraint asked <= paid

outputs
  route : path

table pick
policy unique
| asked | -> route : path |
| <=100 | at_once         |
| >100  | review          |

ワークフローは、客が求めた額をそのまま渡して、この規則を呼びます。

workflow refund v1
description "Pays a refund back at once or sends it to review, as the rule decides"

use rule check from "refund_check.rule"
  lambda "arn:aws:lambda:us-east-1:123456789012:function:refund-check"

inputs
  order : string
  paid  : int  range >=0 <=10000

task ask_amount(order: string) -> int range >=0 <=10000
  lambda "arn:aws:lambda:us-east-1:123456789012:function:ask-amount"
  idempotent

task pay_back(order: string, amount: int range >=0 <=10000)
  lambda "arn:aws:lambda:us-east-1:123456789012:function:pay-back"
  key

flow
  let asked = ask_amount(order: order)
  let decision = check(paid: paid, asked: asked)
  match decision.route
    at_once => pay_back(order: order, amount: asked)
    review => pass

どちらのファイルも、それぞれの言語の検査は通ります。合わせると通りません（この二つのファイルは、ritsu explain E201 が出す再現のものです。再現には、同じ規則を kaname のモジュールから呼ぶファイルもあります）。

$ ritsu check . --lang ja
ok refund_check.rule
refund.flow: 検査を通りました
エラー[ritsu E201]: refund.flow:21:1: 規則 check を呼ぶところで、前提 `asked <= paid` を破る値を渡すことがあります
    21 |   let decision = check(paid: paid, asked: asked)
  = `asked` は `>=0 <=10000`、`paid` は `>=0 <=10000` で、asked = 10000, paid = 0 のとき `asked <= paid` が成り立ちません
  = 規則から生成したコードは、前提を破る呼び出しを入口で受け付けません。この呼び出しは、ワークフローを走らせたときに初めて落ちます。値の範囲は、dandori がその値を入れるすべての場所から集めたものです。
  = 値を渡す前に前提を保つよう分岐するか、範囲を狭めてください（入力やタスクの結果の `range`）。
ritsu check: ファイル 2 個（rulec 1、dandori 1）。検査を通らないもの 1 個（エラー 1 件）。言語の境目: 確かめた 1 か所、決められない 0 か所

言語をまたぐ検査の答えは、いつも三つのどれかです。成り立つ、成り立たない例がここにある、決められない（そのときは理由を言う）。黙って通すものはありません。たとえば次のものを確かめます。

• ワークフローが規則を呼ぶすべての場所で、規則の前提が成り立つか
• koyomi の日付がとりうる日を、規則の入力の範囲にすること（range from koyomi）。規則が宣言した範囲に収まるか
• 規則の出力を chobo の振替の額に渡すとき、その額で振替が拒否されうる理由
• chobo の仮押さえの有効期限と、ワークフローが営業日で数える待ちの長さ
• kaname のモジュールが規則、日付、振替に渡すどの値も、相手が宣言した範囲に入るか
• rulec、dandori、chobo、kaname で一つの型になったお金と単位
• sakai の地図のコンテキストが公開する操作に、それを守るゲートの action があるか。ワークフローが呼ぶ操作を、ゲートがそのワークフローに許しているか
• yuen は表、日付、主張、タスク、関数を一つずつハッシュで固定し、sakai はコンテキストをまたぐ参照を行番号つきで確かめる

人のためのページ

コードが実現すべきものを理解し、確かめたい人（業務の担当者、経理や法務、運用する人、コードをレビューする開発者）のためのページも、同じファイルから英語か日本語で作れます。書かれたことを読み、自分の知っていることと照らし合わせられます。

• rulec doc：規則の表、ただし書き、証明できたこと（Markdown か HTML）
• dandori doc：ワークフローの図と、走るすべてのシナリオ
• koyomi doc：暦を月ごとに
• chobo doc：帳簿、その上限と下限、振替
• sekisho doc：だれが何をしてよいかを action ごとの表にし、生成する Cedar と並べる
• kaname doc：モジュールの、表にある判断、エフェクトごとの関数とそれぞれが失敗しうる場所、コードにある判断
• yuen trace：要件を出典までさかのぼり、満たすものまでたどる

入れ方

ソースから入れます（新しい stable の Rust が要ります）。

cargo install --git https://github.com/i2y/ritsu --locked ritsu

ritsu check <ディレクトリ> は、各言語の検査と、言語をまたぐ検査を走らせます。各言語のコマンドは ritsu <言語> … で呼びます（例：ritsu rulec doc fee.rule）。リリースは 0.23.0 から（rulec の番号の続き）で、リリースごとに macOS と Linux のアーカイブと、.deb と .rpm をリリースのページに置いています。Homebrew なら brew install i2y/tap/ritsu、GitHub Actions なら uses: i2y/ritsu@v0.37.0 で入ります。アーカイブには、ritsu と、言語の名前を付けたそれへのリンクが入っていて、リンクはその言語として動きます。0.26.0 からは、リリースに npm のパッケージ @i2y/ritsu も付きます。WebAssembly 向けに組んだ ritsu で、ネイティブのバイナリなしに Node で動きます（Node で使う）。

プロジェクトは、ほかのモジュールをディレクトリや OCI のレジストリから足して、そのファイルを @<名前>/… のパスで読めます（モジュール）。ritsu gen は、プロジェクトのコードを言語ごとのパッケージにして書きます。--library を付けると、モジュールを npm、PyPI、Go が受け取るライブラリにして書き、依存のモジュールはそのライブラリから名前で import します（ライブラリとして公開する）。

全体の設計は DESIGN.md にあります。ライセンスは MIT と Apache-2.0 のどちらかを選べます。

AI エージェント向け

ritsu とその言語は、AI エージェントに使ってもらうためのものです。リポジトリに、十の Agent Skills を置いています。ritsu のスキルは二つ以上の言語を使うプロジェクトのためのもので、残りの九つは言語ごとのスキルです（一覧は skills/README.ja.md にあります）。入れ方は四つあります。

• Claude Code：このサイトがプラグインのマーケットプレイスを公開していて、プラグイン ritsu に十のスキルが入っています。/plugin marketplace add https://i2y.github.io/ritsu/marketplace.json を実行してから、/plugin install ritsu@ritsu を実行します。Claude Code が取ってくるのは skills/ のフォルダーだけで、リポジトリ全体はダウンロードしません。
• どのエージェントでも、バイナリから：ritsu skills install が、プロジェクトの .claude/skills/ に書きます。--user を付けると ~/.claude/skills/ に、--dir <dir> を付けると、ほかのエージェントがスキルを読む場所に書きます。名前を挙げると（ritsu skills install rulec dandori）そのスキルだけを書き、ritsu skills list で一覧を出します。
• 手で：skills/ から必要なフォルダーを、~/.claude/skills/ か、プロジェクトの .claude/skills/ にコピーします。
• リリースから：ritsu-skills-v<版>.zip に十のフォルダーが入っています。エージェントがスキルを読む場所に展開します。