Quickstart Guide

Installation

JuGeo requires Python 3.10 or later and runs on Linux, macOS, and Windows (WSL2 recommended on Windows). It has no mandatory binary dependencies — the SMT solver backend is optional and can be added later.

Clone and install in editable mode

git clone https://github.com/thehalleyyoung/jugeo.git
cd jugeo
pip install -e .

The -e flag installs JuGeo in editable mode so you can pull updates with git pull without reinstalling.

Optional: SMT solver support (Z3)

For solver-backed verification (trust level SOLVER), install Z3:

pip install z3-solver

Verify the installation

jugeo --version

jugeo 0.9.0
Python 3.11.4 · Platform darwin
SMT backend: z3 4.12.2 (available)
Lean backend: leanc 4.3.0 (available)

Choose Your Quickstart Path

JuGeo now has three especially important surfaces. If you are not sure where to begin, pick the one closest to what you want to build or verify:

pip install -e .
jugeo prove --spec spec.py --impl impl.py

pip install -e .
python jugeo-agents/examples/coding_agents_demo.py

from jugeo.webapp.trust.bundle import WebTrustBundle, WebJudgment

bundle = WebTrustBundle()
bundle.add_judgment(WebJudgment(stage="browser", language="javascript",
    claim="email field validates format", trust="CLIENT_VALIDATED"))
bundle.add_judgment(WebJudgment(stage="handler", language="python",
    claim="email field validates format", trust="SERVER_VALIDATED"))
print(bundle.summary_text())

Your First Verification

A JuGeo verification checks that an implementation satisfies a specification. Both are ordinary Python functions. JuGeo builds a judgment — a formal statement of the claim — and routes it through available evidence channels (static analysis, SMT solving, runtime testing) to produce a trust-annotated result.

# impl.py
def positive_sum(xs: list[int]) -> int:
    """Return the sum of all positive elements in xs."""
    total = 0
    for x in xs:
        if x > 0:
            total += x
    return total

# spec.py
def positive_sum(xs: list[int]) -> int:
    """Reference: sum of elements greater than zero."""
    return sum(x for x in xs if x > 0)

jugeo prove --spec spec.py --impl impl.py

JuGeo Verification Engine v0.9.0
────────────────────────────────────────────────────────

Coordinate  impl::positive_sum
Proposition BEHAVIORAL: positive_sum(xs) == spec::positive_sum(xs)

  [1/4] Static analysis ................... pass
  [2/4] Type-level reasoning ............. pass
  [3/4] SMT descent (Z3) ................. verified (0.18 s)
  [4/4] Runtime witness sampling (n=256) . pass

────────────────────────────────────────────────────────
Judgment

  Proposition : positive_sum(xs) ≡ spec.positive_sum(xs)  ∀ xs : list[int]
  Trust tier  : SOLVER
  Trust scope : impl::positive_sum
  Evidence    : static(pass), smt(z3, unsat, 0.18s), runtime(256/256)

VERIFIED — judgment holds at trust tier SOLVER

Bug Detection

jugeo bugs performs multi-pass static analysis on a Python file, building a semantic site from its call graph and checking for structural anti-patterns, type-level inconsistencies, and common runtime hazards. No spec required.

Example: code with known issues

Create mycode.py with two classic Python pitfalls:

# mycode.py

# Bug 1: mutable default argument
def append_item(item, collection=[]):
    collection.append(item)
    return collection


# Bug 2: bare except swallows all exceptions, including KeyboardInterrupt
def load_config(path):
    try:
        with open(path) as f:
            return f.read()
    except:
        return None


# Bug 3: loop variable leaks out of comprehension scope (Python 2 compat issue
#         that trips up developers migrating code, and also a logic error here)
def first_match(items, predicate):
    result = [x for x in items if predicate(x)]
    # Intended: return first match or None
    # Actual bug: always returns the full list, not just the first element
    return result

jugeo bugs mycode.py

JuGeo Bug Detector v0.9.0
Analyzing: mycode.py  (3 functions, 1 site)
────────────────────────────────────────────────────────

WARN  mycode::append_item  [mutable-default-arg]
      Line 4: parameter collection has mutable default value [].
      The list is shared across all calls. Pass None and assign
      inside the body.
      Evidence: static(ast-pattern), trust=UNVERIFIED

WARN  mycode::load_config   [bare-except]
      Line 12: bare except: clause catches BaseException, including
      KeyboardInterrupt and SystemExit. Use except Exception: or
      a more specific type.
      Evidence: static(ast-pattern), trust=UNVERIFIED

WARN  mycode::first_match    [return-type-mismatch]
      Line 22: function name suggests a single element return but the
      body returns list. Inferred return type: list[T].
      Consider returning result[0] if result else None.
      Evidence: static(type-inference), trust=UNVERIFIED

────────────────────────────────────────────────────────
Summary  3 warnings, 0 errors  (mycode.py)
Run jugeo repair mycode.py --auto-apply to apply suggested repairs.

Auto-repair

Use jugeo repair to turn a failing file into ranked repair suggestions. Add --auto-apply when you want JuGeo to apply the top mechanical fix:

jugeo repair mycode.py --auto-apply

Equivalence Checking

jugeo equiv checks whether two Python programs are behaviorally equivalent — that is, for every valid input they produce identical outputs. This is useful when refactoring, migrating between implementations, or auditing optimisations.

Create two implementations of the same algorithm — one naive, one optimised:

# prog1.py  — naive O(n²) deduplication
def unique_sorted(xs: list[int]) -> list[int]:
    seen = []
    for x in xs:
        if x not in seen:
            seen.append(x)
    return sorted(seen)

# prog2.py  — O(n log n) using set
def unique_sorted(xs: list[int]) -> list[int]:
    return sorted(set(xs))

jugeo equiv prog1.py prog2.py

JuGeo Equivalence Check v0.9.0
────────────────────────────────────────────────────────

Pair   prog1::unique_sorted  ↔  prog2::unique_sorted
Claim  BEHAVIORAL equivalence ∀ xs : list[int]

  [1/3] Structural diff ....... different (O(n²) vs O(n log n))
  [2/3] SMT encoding (Z3) ..... unsat — no counterexample (0.31 s)
  [3/3] Runtime sampling (n=512) 512/512 pairs agree

────────────────────────────────────────────────────────
Judgment

  Verdict     : EQUIVALENT
  Trust tier  : SOLVER
  Counterex.  : none found
  Evidence    : smt(z3, unsat, 0.31s), runtime(512/512)

When a counterexample is found

If the two programs diverge, JuGeo prints a concrete counterexample so you can inspect the discrepancy immediately:

NOT EQUIVALENT  — counterexample found

  Input  xs = [-1, 0, 1]
  prog1  →  [0, 1]   # filters negatives too
  prog2  →  [-1, 0, 1]

  Trust  : SOLVER (counterexample is SMT-certified)

Using the Python API

All CLI commands have a first-class Python API. This is useful for integrating JuGeo into test suites, notebooks, or CI pipelines that need programmatic access to judgment objects and evidence bundles.

Build a semantic site

A site is a Grothendieck-style topology over the coordinate space of your codebase. You build one by listing the coordinates (function identities) you want to reason about.

from jugeo.geometry import Coordinate, CoordinateKind, build_site

# A coordinate uniquely identifies a callable in the semantic space
coord = Coordinate(
    components=("mymodule", "positive_sum"),
    kind=CoordinateKind.FUNCTION,
)

# build_site accepts a list of coordinates and constructs the
# covering topology for descent computations
site = build_site([coord])

Create a judgment

A judgment packages a proposition, its trust profile, and all contributing evidence into a single auditable object.

from jugeo.easy import spec

review = spec(
    "def inc(x):\n    return x + 1",
    "def spec(result, x):\n    return result > x",
    input_cover=[
        {"args": [1], "kwargs": {}},
        {"args": [2], "kwargs": {}},
    ],
    entrypoint="inc",
)

print(review)
print(review.satisfied, review.witness_count)

Route through the solver

SolverRouter dispatches the judgment to whichever backends are available and merges their evidence into a final verdict:

from jugeo.solver.router import SolverRouter, RoutingStrategyKind

router = SolverRouter()
print(type(router).__name__)
print([strategy.name for strategy in RoutingStrategyKind][:4])

Run descent to glue local sections

Descent checks that locally-verified facts about sub-modules are consistent when glued together — the sheaf condition for your codebase.

from jugeo.geometry.descent import DescentEngine, DescentStrategy

engine = DescentEngine()
print(type(engine).__name__)
print([strategy.name for strategy in DescentStrategy])

Inspecting evidence bundles

from jugeo.evidence.channels import RuntimeChannel, SolverChannel, CopilotChannel

runtime_channel = RuntimeChannel()
solver_channel = SolverChannel()
copilot_channel = CopilotChannel()

print(runtime_channel.channel.default_trust_floor())
print(solver_channel.channel.default_trust_floor())
print(copilot_channel.channel.default_trust_floor())

CLI Commands Overview

All commands accept --help for detailed flag documentation. Global flags like --verbose, --format json, --output DIR, and --no-llm are supplied before the subcommand.

Common flags

# Output machine-readable JSON for scripting
jugeo --format json prove --spec spec.py --impl impl.py

# Increase verbosity to see more diagnostics
jugeo --verbose bugs mycode.py

# Disable model-backed fallbacks
jugeo --no-llm prove --spec spec.py --impl impl.py

# Write command output into a results directory
jugeo --output ./results prove --spec spec.py --impl impl.py

# Show every global option
jugeo --help

Next Steps

You've seen the ecosystem entry points and walked through the core Python flow. Here are the best next pages, depending on which surface you want to go deeper on: