Chiasmus

Ce qu'il fait

Chiasmus offre aux modèles de langage un accès à la vérification formelle et au raisonnement neurosymbolique. En s'appuyant sur Z3 (solveur SMT) et SWI-Prolog, il permet aux agents IA de prouver la correction, de détecter des contradictions dans les règles RBAC, d'analyser les graphes d'appels pour le code mort et de vérifier les invariants du système avec une certitude mathématique.

Outils

• chiasmus_verify : Soumettez des spécifications SMT-LIB ou Prolog pour obtenir des résultats vérifiés, y compris les cœurs unsat et les traces de dérivation.
• chiasmus_graph : Effectue une analyse structurelle profonde du code source (TypeScript, JS, Python, Go, Clojure), y compris l'analyse de reachability et d'impact.
• chiasmus_map : Génère un aperçu compact de la base de code pour que les agents puissent le consulter avant de lire les fichiers.
• chiasmus_skills : Recherche dans une bibliothèque de modèles de vérification pour des problèmes courants tels que l'autorisation et la résolution de dépendances.
• chiasmus_formalize : Fait correspondre des problèmes en langage naturel à des modèles de vérification formelle.
• chiasmus_solve : Pipeline de bout en bout qui formalise, résout et corrige les spécifications logiques.
• chiasmus_review : Génère une recette de revue de code phasée basée sur l'analyse structurelle et formelle.
• chiasmus_search : Recherche sémantique de code utilisant des embeddings pour trouver de la logique par le sens.

Installation

{
  "mcpServers": {
    "chiasmus": {
      "command": "npx",
      "args": ["-y", "chiasmus"]
    }
  }
}

Hôtes supportés

• Claude Code
• Claude Desktop
• Crush
• OpenCode