Frequently Asked Questions

JuGeo (Judgment Geometry) is a Python verification framework that applies sheaf theory and formal logic to existing Python codebases. It proves properties — purity, absence of exceptions, type safety, behavioral contracts — about Python functions and modules without requiring you to rewrite your code in a formal language.

The core idea is to model a codebase as a semantic site: a category of code objects equipped with a Grothendieck topology. JuGeo's judgment sheaf on this site assigns verification conditions to each code object and checks that they are compatible across interfaces — exactly the sheaf descent condition from algebraic geometry, applied to software.

No. JuGeo's API is entirely Pythonic. You write annotations like @jugeo.ensures("pure"), run jugeo prove mymod, and read diagnostic output that tells you which functions fail which properties and why. The sheaf-theoretic machinery runs entirely under the hood.

That said, understanding the key concepts — semantic sites, sheaf descent, and cohomological obstructions — will help you interpret diagnostics more effectively, especially for H¹ (interface compatibility) failures. The Concepts page introduces these ideas with minimal mathematical prerequisites.

JuGeo requires Python 3.10 or newer. Core dependencies are:

• z3-solver >= 4.12 — the primary SMT solver
• cvc5 >= 1.1 (optional) — secondary solver for nonlinear arithmetic
• mypy >= 1.8 (optional) — for the static analysis agent
• anthropic >= 0.25 (optional) — for LLM copilot agents

Install the repo from its root with pip install -e . and add optional solver or model dependencies separately as needed.

Three steps:

# 1. Install from the repo root
pip install -e .

# 2. Find the highest-signal problems first
jugeo bugs mymod.py

# 3. Repair or verify against an explicit spec
jugeo repair mymod.py --spec spec.py
jugeo prove mymod.py --spec spec.py

A practical adoption loop is: run jugeo bugs to surface the highest-signal problems, use jugeo repair to preview or apply mechanical fixes, then run jugeo prove with a real spec file. After reviewing and applying those changes, jugeo prove verifies the whole module and reports any remaining obstructions. See the Quickstart for a full walkthrough.

The trust algebra is a partially-ordered set of trust levels that JuGeo assigns to evidence. From lowest to highest:

\(\mathrm{NONE} \prec \mathrm{COPILOT\_SUGGESTED} \prec \mathrm{ANNOTATION} \prec \mathrm{SOLVER} \prec \mathrm{FORMAL\_PROOF}\)

Trust matters because different evidence channels have different reliability. An LLM suggestion is useful but not definitive; an SMT solver proof is much stronger; a Lean proof is strongest. JuGeo uses the trust level to determine whether a judgment is “closed” (sufficient for deployment) and how much weight it carries in composed judgments — the trust of a composition is the meet of its component trusts.

An obstruction is a verification failure classified by cohomological degree:

• H⁰ — a function simply does not satisfy the property. Fix the implementation or add a precondition that excludes the failing case.
• H¹ — two components satisfy the property locally but disagree at their interface. Reconcile the interface contract between them.
• H² — a three-way coherence failure. Rare; usually indicates a design problem with multiple-inheritance or deep typeclass hierarchies.
• H∞ — the property is undecidable for this code. Requires a manual Lean proof or a simplifying refactor.

In practice, 95%+ of obstructions are H⁰ or H¹, and JuGeo provides automatic repair suggestions for both degrees.

Semantic moves are JuGeo's equivalent of proof tactics in a proof assistant like Coq or Lean. Each move is an atomic step that advances a judgment toward closure. The 16 built-in moves include: VERIFY (call the SMT solver), GLUE (assemble local proofs into a global one via descent), CUT (introduce an intermediate lemma), REPAIR (automatic code fix), NEGOTIATE_TREATY (resolve H¹ interface conflicts), and ESCALATE (hand off to a higher-trust channel).

Unlike tactics in a proof assistant, semantic moves operate on judgment states that carry trust, evidence provenance, and obstruction data — not just raw formulas. This makes them “fleet-aware” and able to coordinate across multiple verification agents.

Sheaf descent is the process by which JuGeo assembles local verification results (one per function or class) into a global result for a whole module. Descent succeeds when all local sections are compatible on shared interfaces. It fails when at least one interface is incompatible — producing a cohomological obstruction.

The most common cause: a function is locally pure but calls a helper that performs I/O, creating a compatibility mismatch at the call-site interface. This is a classic H¹ obstruction: both functions have local sections, but they disagree on the intersection (the call boundary).

JuGeo models each of Python's five effect families as a sheaf-theoretic structure:

• Exceptions are coordinate forks — the function's section splits into success and failure fibers.
• State mutations are scope sections — local sections of a state sheaf over the lexical scope.
• Async functions are suspended morphisms, with each await point as a restriction map.
• Generators yield a fiber restriction sequence, one section per yield.
• Context managers are covering families, with __enter__/__exit__ as the covering pair.

This uniform treatment lets JuGeo check effect compatibility at module boundaries using the same descent machinery as property verification.

JuGeo's fragment classifier recognises 13 fragments: QF_LIA, QF_LRA, QF_BV, QF_AUFLIA, QF_S (strings), QF_NIA, QF_NRA, UFLIA, AUFBVLIA, QF_DT (datatypes), QF_UFLIA, ALL, and UNKNOWN. Each fragment is routed to the most appropriate solver tactic automatically.

Formulas outside the decidable fragments are classified UNKNOWN and escalated to the FORMAL evidence channel or marked as H∞ obstructions. In practice, the vast majority of Python property verification conditions are QF_LIA or QF_AUFLIA and are handled comfortably by Z3.

Yes. CVC5 is supported out of the box and used by default for QF_NRA fragments. You can also register a custom solver:

from jugeo.solver import SolverAgent, register_solver, SolverResult

@register_solver(fragments=["QF_LIA", "QF_LRA"])
class MySolver(SolverAgent):
    def solve(self, formula, timeout_ms):
        # call your solver here
        return SolverResult(status="UNSAT", certificate=...)

Bitwuzla and Yices2 are also available as optional extras via pip install "jugeo[bitwuzla]" and pip install "jugeo[yices]" respectively.

When a solver times out or returns UNKNOWN, JuGeo's routing layer tries the configured fallback chain (e.g., Z3 then CVC5). If all solvers are inconclusive, the judgment remains open with NONE trust and is either:

• Escalated to the FORMAL evidence channel (requiring a Lean proof) if the ESCALATE control law is active.
• Flagged as a potential H∞ obstruction if the formula structure suggests undecidability.
• Left on the frontier for a future tick if the orchestrator has remaining budget.

Solver timeouts are surfaced in the diagnostic report with the fragment classification and estimated complexity, to help you decide whether to restructure the code or increase the timeout budget.

Mypy and pyright are type checkers: they verify that your code uses types consistently but cannot prove properties about values (e.g., that an integer is always positive, or that a function never raises KeyError). JuGeo goes beyond types to verify semantic properties using SMT solvers.

JuGeo is complementary to type checkers, not a replacement. Running mypy and JuGeo together gives you type-level and value-level verification. JuGeo's static analysis agent can invoke mypy internally and incorporate its results as ANNOTATION-trust evidence.

Hypothesis finds bugs by generating random inputs and checking whether properties hold. It is excellent for finding bugs quickly but can never prove a property holds for all inputs.

JuGeo proves properties for all inputs using SMT solvers. For properties within decidable fragments, JuGeo provides definitive VERIFIED or FALSIFIED answers. When a full proof is not achievable, JuGeo can accept Hypothesis-style counterexample evidence as ANNOTATION-trust evidence, combining the strengths of both approaches.

JuGeo is designed for existing Python codebases. You do not need to rewrite your code in any special style. The recommended workflow for adoption:

• Run jugeo bugs on a real file to find the highest-signal failures first.
• Use jugeo repair for mechanical fixes and jugeo spec / jugeo prove when you have an explicit contract.
• Add jugeo prove or jugeo bugs --format json to CI as coverage grows.

Partial annotation is fully supported. Functions without annotations carry NONE trust, which propagates through the module but does not break the tool. Unannotated judgments are simply left open on the frontier.

JuGeo provides a language server (LSP) that exposes inline diagnostics in VS Code, Neovim, and any LSP-compatible editor:

Earlier drafts of the website mentioned a standalone language-server command, but the public interface exposed in this repository today is the CLI itself plus structured JSON output. For editor workflows right now, the reliable path is to run jugeo --format json bugs or jugeo --format json prove and surface those diagnostics in your editor or CI tooling.

JuGeo outputs structured JSON that integrates cleanly with GitHub Actions, GitLab CI, and Jenkins. A typical GitHub Actions setup:

- name: JuGeo prove
  run: |
    pip install -e .
    jugeo --format json prove mymod.py --spec spec.py > jugeo-report.json
- name: Upload report artifact
  uses: actions/upload-artifact@v4
  with:
    name: jugeo-report
    path: jugeo-report.json

Because the CLI returns a non-zero exit status on command failure, the simplest policy is to let your CI step fail naturally and keep the JSON artifact for inspection.

The LLM copilot is an evidence channel with a fixed trust ceiling of COPILOT_SUGGESTED. Evidence from the copilot is always below SOLVER trust: \(\mathrm{COPILOT\_SUGGESTED} \prec \mathrm{SOLVER}\).

This means copilot suggestions cannot directly close a judgment. They are hints that guide the solver: the copilot suggests an annotation or proof strategy, the solver confirms it, and only the solver's confirmation produces a SOLVER-trust closed judgment. This design prevents LLM hallucinations from being silently accepted as verified facts.

JuGeo's current public model surface is the CLI's --model flag rather than a stable public copilot Python package:

import subprocess

subprocess.run(
    [
        "python3",
        "-m",
        "jugeo",
        "--model", "claude-sonnet-4.6",
        "research",
        "Find likely verification gaps in this module",
    ],
    check=True,
)

Proof-carrying Python is a deployment pattern where a Python module is shipped together with its JuGeo certificate — a machine-checkable record of all verified properties, the evidence used to verify them, and the trust levels achieved. Consumers can independently verify the certificate without re-running the solver.

Certificates are stored in .jugeo/certs/ as CBOR-serialised certificate chains. The website drafts previously mentioned a standalone jugeo verify-cert command, but that command is not part of the public CLI surface in this repository today. In practice you inspect the generated artifact metadata and serialized verification outputs instead. This still enables supply-chain trust: a downstream package can require that its dependencies provide SOLVER-trust certificates for their public APIs.

Yes, within limits. JuGeo's tensor encoding sub-package can prove:

• Shape compatibility between layers (matrix dimensions match).
• Weight magnitude bounds (weights in \([-1, 1]\) after initialisation).
• Output range guarantees (softmax outputs in \([0, 1]\)).
• Batch-size invariance (output shape depends only on input batch size).

Proving properties about learned weight values at runtime is currently out of scope — JuGeo reasons about the code structure, not specific weight data. Runtime weight properties require interval arithmetic tools or runtime monitoring.

JuGeo handles unanalysable code gracefully and never silently skips it:

• Functions calling C extensions or ctypes receive an OPAQUE coordinate type. Their properties cannot be inferred and must be manually annotated.
• Functions with undecidable properties (H∞) are flagged with a suggestion to add a Lean proof or simplify the code.
• Code with syntactic errors is skipped with a warning; the rest of the module is still analysed.
• Very large functions (over 500 AST nodes) are analysed in fragments using the REFINE_COVER move to keep solver context sizes manageable.

See the Contributing guide for full details. The short version:

• Bug reports & feature requests: file a GitHub issue.
• Code contributions: fork the repo, make your changes with tests, open a PR.
• New encoding sub-packages: implement EncodingProtocol and submit a PR with benchmarks.
• New model-backed workflows: extend the documented CLI or jugeo.easy surface and add a paper-style evaluation in papers/.
• Theorem and research contributions: add examples, papers, or benchmark cases that strengthen the existing ideation and research flows.

The project follows a research-integrated development model: major new features are accompanied by a short paper in the papers/ directory. See existing papers for the expected format.

The discovery engine scans your semantic site and proactively generates candidate theorem statements — properties your code probably satisfies but that you haven't yet specified. It ranks them by leverage: how many other judgments would become easier to close if this theorem were in the ecology.

Running jugeo ideate explores candidate theorem and design spaces, while jugeo bugs, jugeo spec, and jugeo prove remain the concrete verification entry points surfaced by the current CLI. In benchmarks, bootstrapping with the discovery engine reduced the annotation effort required to reach 70% judgment coverage by 58% compared to manual annotation.