CLI Reference

Full sheaf-theoretic program verification. Loads spec and implementation into a semantic site, computes descent obstructions, dispatches to Z3/SMT and LLM evidence channels, and attempts to glue local judgments into a global proof certificate.

Static bug detection across six well-defined Python bug classes. Combines AST analysis with Z3-backed data-flow reasoning and optional LLM triage to rank findings by severity and fix cost.

Check a Python implementation against a formal specification file. Extracts pre/post conditions and invariants from the spec, encodes them in SMT, and verifies the implementation satisfies every judgment section.

Check semantic equivalence of two Python programs. Uses sheaf-theoretic judgment transport to compare observable behaviour across all reachable inputs, optionally modulo a relation (e.g. output order, floating-point tolerance).

Suggest minimal, semantically-grounded repairs for buggy code. Analyses detected bugs and failing spec judgments, proposes diffs, and optionally applies them in-place after confirmation.

Evaluate code quality, semantic maturity, and trust tier. Produces a scorecard across multiple dimensions including correctness, robustness, documentation alignment, and cyclic maturity level.

Generate Python code from a formal specification or judgment description. Uses the LLM oracle guided by SMT-checked preconditions to produce implementations that are pre-verified at the judgment level before being returned.

Run a full judgment pipeline from a TOML or JSON configuration file. Useful for multi-step workflows (e.g. load → encode → prove → evaluate) defined declaratively and reproducibly.

Start a local HTTP API server exposing all JuGeo commands as REST endpoints. Designed for IDE plugin integration, CI pipelines, and the JuGeo web dashboard.

Load and analyse a Python program into judgment sections. Produces a human- and machine-readable breakdown of the program's semantic structure: sections, effects, type constraints, and import graph.

Encode a Python program's judgment sections into Z3/SMT. Supports scalar, sequence, tensor, and text encodings. Output is an SMT-LIB2 file or a Z3 Python script.

Classify a problem or code file against the JuGeo problem atlas. Returns the nearest problem families, recommended proof strategies, and analogous theorems from the theorem ecology.

Check documentation (docstrings, README, type annotations) for honest projection against the actual code semantics. Detects outdated docs, misleading claims, and missing coverage.

Run bugs, spec compliance, and equivalence checks simultaneously in a single pass. More efficient than calling each command separately; shares the loaded semantic site and SMT encoding across all three analyses.

Show package version, installed packs, solver versions, trust tier summary, and environment diagnostics. Useful for debugging and support reports.

Run the JuGeo test and benchmark suite. Can run the full internal test suite, a specific experiment, or a user-supplied benchmark configuration.

Run descent and gluing on pre-computed judgment data. Takes a set of local judgment sections (from jugeo load or jugeo encode) and attempts to glue them into a global section via the Cech descent algorithm.

Mathematical ideation and theorem discovery. Given seed theorems or problem families, generates new conjectures, finds analogies via analogy transport, and ranks candidates by plausibility score.

Synthesize a complete program from a natural language idea. Uses sheaf-theoretic elaboration to plan, generate, test, and refine software.

Full synthesis pipeline: mathematical fields → tournament → code generation → textbook generation. Produces a self-contained research artefact including theorems, implementations, and a generated textbook chapter.

Browse and search the JuGeo problem catalog. Lists all registered problem families, their recommended strategies, associated theorems, and example code.

Generate a complete Flask web application from a natural-language prompt. Produces models, routes, templates, static assets, and runs cross-layer descent verification to catch mismatches before deployment.

Improve an existing codebase via an agent-driven descent loop. Scans source files, identifies structural gaps, dispatches an AI agent to make targeted improvements, and verifies each iteration satisfies the stated obligation.

Directed research pipeline: ideate a novel approach, generate an implementation, benchmark against baselines, refine or pivot, and produce a research paper. Runs until descent succeeds (H¹ = 0) on the research site.

Evolutionary tournament to find the best implementation for a canonical problem. Tries multiple competing mathematical theories, keeps copies of what works, and evolves the champion to beat itself on the specified metrics.

Iterative descent on a 7-object delivery site: ideates a novel approach, generates a large-scale implementation, benchmarks against competitive baselines on real data, and refines or pivots until all hard obligations are met (H¹ = 0 on the delivery site).