Run unit tests for a project and return a summarized result.

Run integration tests for a project and return a summarized result.

Run mutation tests and return summarized mutation statistics. Supports multiple frameworks: stryker (JS/TS), mutmut (Python). If tool is not specified, auto-detects based on project structure.

Return recent unit, integration, and mutation runs for a project and optional region.

Compute PID-like metrics and mutation score for a specific region within a project.

Detect available mutation testing frameworks and project language. Returns detected frameworks with confidence scores and a recommendation for which framework to use.

Parse a region identifier string into its components. Regions use a hierarchical format: file:::class:::func:::lines:-. Useful for understanding region hierarchy.

Check if one region contains or overlaps another. Useful for aggregating metrics across related regions. A file region contains all functions within it; a function region contains its line ranges.

Create a region identifier for a specific code location. Use level='file' for whole file, 'function' for a function, 'class' for a class, or 'lines' for a line range.

Add an assertion to the synthesis theory with evidence grounding. Assertions are typed beliefs about code (type, behavior, invariant, contract). Each assertion must be grounded by evidence (test results, mutation results, etc.).

Contract (remove) an assertion from the theory using AGM contraction. Strategies: 'entrenchment' (removes target and less-entrenched dependents), 'minimal' (target and edges only), 'full_cascade' (target and all descendants).

Get the entrenchment score for an assertion. Entrenchment measures belief resilience (0.0-1.0, higher = more entrenched). Highly entrenched beliefs are harder to remove via contraction.

List all assertions in the synthesis theory. Optionally filter by assertion type (type, behavior, invariant, contract) or by region ID.

Get a snapshot of the current synthesis theory. Returns the world bundle with all nodes, edges, and evidence.

Revise the theory by incorporating a new assertion. If the new assertion contradicts existing beliefs, those are first contracted (via AGM revision / Levi identity) before adding the new belief.

Store a piece of evidence (test result, mutation result, etc.) in the synthesis theory. Evidence is required to ground assertions.

Get the provenance DAG summary for a project's synthesis theory. Shows the history of belief revision operations: expansions, contractions, revisions, and evidence storage events.

Trace the evidence chain for an assertion. Returns the list of evidence IDs that ground (support) a given assertion, answering 'why do we believe this?'.

Measure the stability of an assertion. Returns a score from 0.0 (constantly revised) to 1.0 (never touched). Unstable assertions may need stronger evidence or reformulation.

Revert the synthesis theory to a prior world state. Uses content-addressable storage — no data is lost, only the current world pointer changes.

Undo the last N belief revision operations. Walks backward through the provenance DAG to find the prior world state, then rolls back to it.

Analyze why a synthesis attempt failed. Classifies the failure mode (type mismatch, overfitting, underfitting, etc.) and suggests which assertions to contract to fix the issue.

List all historical world states for a project's synthesis theory. Returns world hashes with timestamps and reasons, useful for understanding theory evolution and choosing rollback targets.

Extract and analyze the call graph of a Python project. Returns summary statistics: node count, edge count, SCC count, connected components, and top-level function list.

Compute Fiedler spectral partitioning of a project's call graph. Recursively bipartitions the graph using the Fiedler vector (2nd eigenvector of the graph Laplacian). Returns a partition tree with node assignments and algebraic connectivity (λ₂) values.

Query reachability between two functions in a project's call graph. Uses Kameda O(1) index for planar subgraphs with BFS fallback for non-planar edges. Returns whether the source can reach the target, the method used, and the path if reachable via BFS.

Get the hierarchical decomposition of a project's call graph. Alternates between SCC condensation and Fiedler spectral partitioning to produce a tree representing the project's modular structure.

Find which partition a function belongs to in the Fiedler partition tree. Returns the partition ID, sibling functions in the same partition, and the entry/exit points of that partition.

Start CEGIS synthesis to generate a patch that kills a surviving mutant. The engine uses LLM candidates + genetic algorithm evolution + counterexample feedback to produce a verified patch. Returns a SynthesisResult dict.

Check the status of a completed synthesis run. Returns iteration count, fitness history, counterexamples resolved, and outcome.

Cancel a running synthesis. Sets a cancellation flag that the CEGIS engine checks between iterations.

List all synthesis runs for a project. Returns a summary of past runs with outcomes, iterations, and fitness.

Detect file changes and update the persisted call graph incrementally. Compares file hashes to find added/modified/removed files, then updates only the affected graph nodes. Much faster than full re-extraction.

Get statistics from the persistent graph store for a project. Returns node count, edge count, whether Kameda index and partitions are stored, backend type, and last update timestamp.

Execute a structured graph query against the persistent store. Supports query types: 'neighbors' (get adjacent nodes), 'reachability' (check if source reaches target via Kameda O(1) index), and 'node' (get node details). Uses stored graph data without re-extraction.

Run formal verification on a binary or constraint set. Supports Z3 (constraint solving), angr (Docker symbolic execution), and mock backends. Returns verification status and any counterexample found.

Run the CEGAR verification orchestrator with budget escalation. Chains verification attempts with progressively larger budgets (10s → 30s → 120s). Returns aggregated result with iteration history.

List available verification backends and their capabilities. Shows which find/avoid predicates and constraint types each backend supports.

Index code nodes into the RAG vector store for semantic search. Each node should have an ID, text content, and optional metadata.

Search the RAG vector store for code relevant to a query. Optionally expands results using the project's call graph.

Get statistics about the RAG vector store.