tla-review
TLA+仕様の包括的なレビューとチェックリスト、自動検証機能 TLA+を使用して記述された仕様書について、チェックリストに基づいた包括的なレビューを実施します。このスキルは、仕様の完全性や正確性を自動で検証し、潜在的な問題や矛盾を特定するのに役立ちます。形式的検証が必要なシステム設計やアルゴリズムの仕様書を確認する際に、品質保証プロセスを効率化できます。
description の原文を見る
Comprehensive TLA+ specification review with checklist and automated validation
SKILL.md 本文
TLA+ 仕様書レビュー
パース、シンボル抽出、スモークテスト、ベストプラクティスチェックリストを含む、TLA+ 仕様書の包括的なレビューを実行します。
重要: 上記の MCP ツールを常に使用してください。Bash 経由で Java または TLC コマンドを実行することは避けてください。
使用方法
/tla-review test-specs/Counter.tla
/tla-review test-specs/Counter.tla test-specs/Counter.cfg
/tla-review test-specs/Counter.tla --no-smoke
注記: 最初の引数として @path.tla と入力した場合、このスキルは先頭の @ を削除し、ファイルが存在することを検証します。
このスキルの動作
- 引数から仕様ファイルパスを検証および正規化します
- SANY パーサーを実行して構文と意味論をチェックします
- シンボルを抽出して仕様構造を分析します
- スモークテストを実行します(
--no-smokeフラグがない場合) - 推奨事項付きの包括的レビューレポートを生成します
実装
ステップ 1: 仕様パスの正規化
このスキルの引数として指定された仕
...
詳細情報
- 作者
- diegosouzapw
- ライセンス
- unknown
- 最終更新
- 2026/3/2
Source: https://github.com/diegosouzapw/awesome-omni-skill / ライセンス: unknown
関連スキル
doubt-driven-development
重要な判断はすべて、本番環境への展開前に新しい視点から対抗的レビューを実施します。速度より正確性が重要な場合、不慣れなコードを扱う場合、本番環境・セキュリティに関わるロジック・取り消し不可の操作など影響度が高い場合、または後でバグを修正するよりも今検証する方が効率的な場合に活用してください。
apprun-skills
TypeScriptを使用したAppRunアプリケーションのMVU設計に関する総合的なガイダンスが得られます。コンポーネントパターン、イベントハンドリング、状態管理（非同期ジェネレータを含む）、パラメータと保護機能を備えたルーティング・ナビゲーション、vistestを使用したテストに対応しています。AppRunコンポーネントの設計・レビュー、ルートの配線、状態フローの管理、AppRunテストの作成時に活用してください。
desloppify
コードベースのヘルスチェックと技術負債の追跡ツールです。コード品質、技術負債、デッドコード、大規模ファイル、ゴッドクラス、重複関数、コードスメル、命名規則の問題、インポートサイクル、結合度の問題についてユーザーが質問した場合に使用してください。また、ヘルススコアの確認、次の改善項目の提案、クリーンアップ計画の作成をリクエストされた際にも対応します。29言語に対応しています。
debugging-and-error-recovery
テストが失敗したり、ビルドが壊れたり、動作が期待と異なったり、予期しないエラーが発生したりした場合に、体系的な根本原因デバッグをガイドします。推測ではなく、根本原因を見つけて修正するための体系的なアプローチが必要な場合に使用してください。
test-driven-development
テスト駆動開発により実装を進めます。ロジックの実装、バグの修正、動作の変更など、あらゆる場面で活用できます。コードが正常に動作することを証明する必要がある場合、バグ報告を受けた場合、既存機能を修正する予定がある場合に使用してください。
incremental-implementation
変更を段階的に実施します。複数のファイルに影響する機能や変更を実装する場合に使用してください。大量のコードを一度に書こうとしている場合や、タスクが一度では完結できないほど大きい場合に活用します。