Formal Model Checking
Prüft nebenläufige Abläufe, Wiederholungen und Prozessabbrüche mit endlichen Zustandsmodellen. Hält Grenzen und Gegenbeispiele fest und leitet bei beauftragter Implementierungsprüfung passende Tests ab.
Installation
Wähle einen unterstützten Installationsweg. Paketumfang, Einbindung in den Agent und benötigte Laufzeitwerkzeuge können sich unterscheiden.
-
Claude Code über diesen Marketplace /plugin install formal-model-checking@netresearch-claude-code-marketplaceZuerst den Marketplace einmal in Claude Code hinzufügen:
/plugin marketplace add netresearch/claude-code-marketplace. Danach das gewünschte Plugin installieren. Einrichtung und Geltungsbereich beschreibt dieClaude-Code-AnleitungEin Plugin kann mehrere Skills und zusätzliche Bestandteile enthalten. -
npx Skills gezielt auswählen npx skills add https://github.com/netresearch/formal-model-checking-skillBenötigt Node.js 22.20+. Im Zielprojekt ausführen und anschließend Skills und Agents im Installer auswählen. Verwendet den skills-Installer von
skills.shInstalliert Skill-Anweisungen. Zusätzliche Plugin-Hooks, Befehle und externe Laufzeitwerkzeuge werden damit nicht eingerichtet. -
composer skills:add PHP-Projekt, direkte Quelle composer skills:add netresearch/formal-model-checking-skillZuerst netresearch/composer-agent-skill-plugin installieren und aktivieren; die Skill-Einbindung der gewählten Quelle freigeben. Wird bereitgestellt von
netresearch/composer-agent-skill-pluginBezieht Quell-Repositories ohne Packagist-Paket und hält sie in composer.skills.lock fest. Laufzeitabhängigkeiten werden getrennt eingerichtet.
Wofür du das Paket einsetzt
- Unterbrochene Schreibvorgänge auf eine fehlende Zuordnung zwischen Mutation und Audit prüfen.
- Leases, Wiederholungen und den Abschluss konkurrierender Worker anhand eines endlichen Modells untersuchen.
- Prüfen, ob ein grüner Modelllauf nur durch unerreichbaren Erfolg oder ungeeignete Gegenproben zustande kommt.
Ergebnisse und Beispiele
- Ein endliches Modell mit konkreter Eigenschaft, Konfiguration, Grenzen und Annahmen; dazu ein vollständiges Suchergebnis oder ein nachvollziehbares Gegenbeispiel.
- Bei beauftragter Implementierungsprüfung: eine Zuordnung zwischen Modell und Code sowie getrennte Ergebnisse von Laufzeittests. Offene Pfade und fehlende Prüfungen bleiben benannt.
Voraussetzungen im Projekt
- Eine konkrete Behauptung oder ein Protokoll; für den Bezug zum Code zusätzlich Quellcode und die relevante Speicher- und Transaktionssemantik.
- Ein passender verfügbarer Modellprüfer oder Interpreter. Die Einbindung der Skill-Anweisungen stellt diese Werkzeuge nicht bereit.
- Die Fixturetests des Quell-Repositories benötigen Python 3.11 oder neuer und die Standardbibliothek.