tlaplus-from-source
ソースコード（C、C++、Rust など）から高レベルの TLA+ モデルを生成します。コードの目的を分析して抽象化を作成し、TLA+ 仕様を記述して、不変式とプロパティを提案します。ユーザーがソースコードを TLA+ でモデル化したい場合、実装から形式仕様を作成したい場合、または並行・分散アルゴリズムを検証したい場合に利用します。
description の原文を見る
Generate a high-level TLA+ model from source code (C, C++, Rust, etc.). Analyzes code to understand its purpose, creates abstractions, writes TLA+ specification, and proposes invariants and properties. Use when the user wants to model source code in TLA+, create a formal specification from implementation, or verify concurrent/distributed algorithms.
SKILL.md 本文
ソースコードから高水準TLA+モデルを生成
ソースコードからコードの意図を理解し、実装の詳細を抽象化し、本質的な並行・分散動作に焦点を当てることでTLA+仕様を作成します。
哲学
TLA+モデルは、システムがどのように動作するかではなく、何をするかを捉える必要があります:
- 状態遷移とその効果に焦点を当てる
- 実装の詳細(メモリ管理、エラーハンドリングの定型文)を抽象化する
- 検証する価値のある本質的な並行・分散動作を特定する
- モデルチェッキングで扱い可能なサイズに保つ
ワークフロー概要
┌─────────────────────────────────────────────────────────────────┐
│ フェーズ1: コードを理解する │
│ → どのような問題を解決するのか? │
│ → 主要な関数とその目的は? │
│ → どのような状態が管理されているか? │
└──────────────────────────────────
...
詳細情報
- 作者
- majiayu000
- ライセンス
- unknown
- 最終更新
- 2026/5/9
Source: https://github.com/majiayu000/claude-skill-registry-data / ライセンス: unknown
関連スキル
agent-browser
AI エージェント向けのブラウザ自動化 CLI です。ウェブサイトとの対話が必要な場合に使用します。ページ遷移、フォーム入力、ボタンクリック、スクリーンショット取得、データ抽出、ウェブアプリのテスト、ブラウザ操作の自動化など、あらゆるブラウザタスクに対応できます。「ウェブサイトを開く」「フォームに記入する」「ボタンをクリックする」「スクリーンショットを取得する」「ページからデータを抽出する」「このウェブアプリをテストする」「サイトにログインする」「ブラウザ操作を自動化する」といった要求や、プログラマティックなウェブ操作が必要なタスクで起動します。
anyskill
AnySkill — あなたのプライベート・スキルクラウド。GitHubを基盤としたリポジトリからエージェントスキルを管理、同期、動的にロードできます。自然言語でクラウドスキルを検索し、オンデマンドでプロンプトを自動ロード、カスタムスキルのアップロードと共有、スキルバンドルの一括インストールが可能です。OpenClaw、Antigravity、Claude Code、Cursorに対応しています。
engram
AIエージェント向けの永続的なメモリシステムです。バグ修正、意思決定、発見、設定変更の後はmem_saveを使用してください。ユーザーが「覚えている」「記憶している」と言及した場合、または以前のセッションと重複する作業を開始する際はmem_searchを使用します。セッション終了前にmem_session_summaryを使用して、コンテキストを保持してください。
skyvern
AI駆動のブラウザ自動化により、任意のウェブサイトを自動化できます。フォーム入力、データ抽出、ファイルダウンロード、ログイン、複数ステップのワークフロー実行など、ユーザーがウェブサイトと連携する必要があるときに使用します。Skyvernは、LLMとコンピュータビジョンを活用して、未知のサイトも自動操作可能です。Python SDK、TypeScript SDK、REST API、MCPサーバー、またはCLIを通じて統合できます。
pinchbench
PinchBenchベンチマークを実行して、OpenClawエージェントの実世界タスクにおけるパフォーマンスを評価できます。モデルの機能テスト、モデル間の比較、ベンチマーク結果のリーダーボード提出、またはOpenClawのセットアップがカレンダー、メール、リサーチ、コーディング、複数ステップのワークフローにどの程度対応しているかを確認する際に使用します。
openui
OpenUIとOpenUI Langを使用してジェネレーティブUIアプリを構築できます。これらはLLM生成インターフェースのためのトークン効率的なオープン標準です。OpenUI、@openuidev、ジェネレーティブUI、LLMからのストリーミングUI、AI向けコンポーネントライブラリ、またはjson-render/A2UIの置き換えについて述べる際に使用します。スキャフォルディング、defineComponent、システムプロンプト、Renderer、およびOpenUI Lang出力のデバッグに対応しています。