Anthropic ClaudeLLM・AI開発⭐ リポ 7品質スコア 69/100

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 本文

注意: このスキルのライセンスは ライセンス未確認 です。本サイトでは本文プレビューのみを表示しています。利用前に GitHub の原本でライセンス条件をご確認ください。

ソースコードから高水準TLA+モデルを生成

ソースコードからコードの意図を理解し、実装の詳細を抽象化し、本質的な並行・分散動作に焦点を当てることでTLA+仕様を作成します。

哲学

TLA+モデルは、システムがどのように動作するかではなく、何をするかを捉える必要があります:

状態遷移とその効果に焦点を当てる
実装の詳細(メモリ管理、エラーハンドリングの定型文)を抽象化する
検証する価値のある本質的な並行・分散動作を特定する
モデルチェッキングで扱い可能なサイズに保つ

ワークフロー概要

┌─────────────────────────────────────────────────────────────────┐
│ フェーズ1: コードを理解する                                      │
│   → どのような問題を解決するのか?                               │
│   → 主要な関数とその目的は?                                     │
│   → どのような状態が管理されているか?                           │
└──────────────────────────────────

...

全文を GitHub の原本で見る →リポジトリ

詳細情報

作者: majiayu000
リポジトリ: majiayu000/claude-skill-registry-data
ライセンス: 不明
最終更新: 2026/5/9

GitHubで原本を見る →フィードバックを送る

Source: https://github.com/majiayu000/claude-skill-registry-data / ライセンス: 未指定