Proof Modes
JuGeo operates in four distinct verification modes. Each targets a different class of properties and generates a corresponding certificate embedded in the output Python module.
Every JuGeo invocation selects exactly one proof mode. The mode determines which judgment forms are constructed, how the SMT encoding is built, what certificate structure is emitted, and which scaffold functions appear in proof-carrying Python output. The four modes correspond to four fundamental properties in judgment geometry:
- Does this function satisfy its specification? (Specification Satisfaction)
- Are two implementations semantically equivalent? (Equivalence Checking)
- Does this function contain a reachable bug? (Bug Detection)
- Does one implementation refine another relationally? (Relational Refinement)
Specification Satisfaction spec
Prove that an implementation satisfies a declarative specification expressed as pre/post-conditions and invariants.
What it does
In specification satisfaction mode, JuGeo constructs a satisfaction judgment \(\vdash_{\mathcal{S}} f : \sigma\) where \(f\) is the implementation and \(\sigma\) is the specification sheaf. The judgment holds when every open \(U\) in the cover of \(\sigma\) admits a section \(s_U\) such that \(f\big|_U \models s_U\).
Internally, JuGeo encodes preconditions into Z3 path constraints, encodes postconditions as verification conditions, and invokes the solver to discharge each VC. When all VCs are SAT-free, a certificate is emitted.
CLI command
# Basic usage
jugeo spec specs/pricing.py mymodule.py
# Equivalent spelled-out flags
jugeo spec --spec specs/pricing.py --impl mymodule.py
# Strict mode fails on any residual obligation
jugeo spec specs/pricing.py mymodule.py --strictPython API
from jugeo.easy import spec
review = spec(
"""
def compute_price(x):
if x <= 0:
return 0.0
return x * 0.9
""",
"""
def spec(result, x):
return result >= 0 and result <= max(x, 0)
""",
input_cover=[{"args": [x], "kwargs": {}} for x in [0, 1, 10, 100]],
)
print(review.satisfied)
print(review.witness_count)
print(review.mode)
jugeo spec mymodule.py::compute_price specs/pricing.yaml JuGeo Specification Satisfaction ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ Target mymodule:compute_price Spec specs/pricing.yaml Cover size 8 opens Solver z3 4.13.0 Building cover... open[0] pre: x > 0 ∧ x ≤ 100 open[1] pre: x > 100 ∧ x ≤ 1000 open[2] pre: x > 1000 ... Encoding verification conditions... 8 VCs generated, 3 non-trivial Discharging VCs... VC[0] ✓ UNSAT (1.2 ms) VC[1] ✓ UNSAT (0.8 ms) VC[2] ✓ UNSAT (2.1 ms) ✓ VERIFIED Certificate: cert_a3f8b2c1 Total: 4.1 ms | 3 VCs discharged | trust: MACHINE_VERIFIED
Equivalence Checking equiv
Prove that two implementations are semantically equivalent on all inputs, or produce a distinguishing counterexample.
What it does
Equivalence checking constructs a bisimulation judgment \(\vdash_{\mathcal{B}} f \sim g\) using a product cover. JuGeo builds a joint semantic site \(\mathcal{S}(f) \times \mathcal{S}(g)\) and checks that for every open \(U\) in the product cover, the sections of \(f\) and \(g\) agree: \(f\big|_U = g\big|_U\).
This is particularly useful for validating refactors — you can confirm that an optimized implementation is provably equivalent to a reference implementation without writing any specifications.
CLI command
# Compare two files symmetrically
jugeo equiv sort_v1.py sort_v2.py
# Ask only whether the left refines the right behaviorally
jugeo equiv sort_v1.py sort_v2.py --direction left-to-right
# Or only check the opposite direction
jugeo equiv sort_v1.py sort_v2.py --direction right-to-leftPython API
from jugeo.easy import equiv
left = """
def sort_v1(xs):
return sorted(xs)
"""
right = """
def sort_v2(xs):
out = list(xs)
out.sort()
return out
"""
result = equiv(left, right)
print(result.equivalent)
print(result.counterexample)
print(result.obstructions)
JuGeo Equivalence Checking ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ Reference mymodule:sort_v1 Impl mymodule:sort_v2 Domain len(xs) ≤ 100 ∧ ∀i. 0 ≤ xs[i] ≤ 1000 Building product cover... 16 opens Encoding product VCs... 16 equivalence conditions Discharging... VC[0..7] ✓ UNSAT (bulk, 3.8 ms) VC[8..15] ✓ UNSAT (bulk, 4.1 ms) ✓ EQUIVALENT Certificate: equiv_7d4a1f09 Total: 8.2 ms | 16 VCs | trust: MACHINE_VERIFIED
Bug Detection bugs
Search for reachable inputs that trigger assertion failures, exceptions, or property violations.
What it does
Bug detection mode constructs obstruction classes in the Cech cohomology \(\check{H}^1(\mathcal{U}, \mathcal{F})\) of the function's semantic sheaf. Non-trivial obstructions correspond to inputs where a local invariant fails to extend to a global section — i.e., bugs.
The engine performs a semantic-directed search, preferring paths through the cover that are most likely to contain obstructions. When a bug is found, it provides a concrete triggering input, a trace, and a ranked list of suggested fixes.
CLI command
# Basic bug scan
jugeo bugs mymodule.py
# Restrict to higher-signal findings
jugeo bugs mymodule.py --severity high
# Emit structured output for automation
jugeo bugs mymodule.py --format jsonPython API
from jugeo.easy import bugs
report = bugs("""
def append_item(item, collection=[]):
collection.append(item)
return collection
""")
print(report.count)
for bug in report:
print(bug.kind, bug.line, bug.message)
print(bug.fix_hint)
JuGeo Bug Detection ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ Target mymodule:process_data Properties 2 user-defined Building semantic sheaf... Computing Cech cohomology H¹... 3 potential obstruction classes found Resolving obstructions... [1/3] ⚠ Spurious — globally extendable [2/3] ✗ BUG FOUND [3/3] ✗ BUG FOUND ✗ 2 BUGS FOUND Bug 1: ZeroDivisionError (property: result is not None) Triggering input: input=[] Location: mymodule.py:47 total / len(input) Suggested fix: guard with `if len(input) == 0: return []` Bug 2: Length invariant violation Triggering input: input=['', 'x', None] Location: mymodule.py:61 result.append(item.upper()) Suggested fix: filter None before processing: `input = [i for i in input if i]`
Repair Suggestions repair
Turn failing files and specification mismatches into concrete repair plans.
What it does
Repair mode starts from bug reports or specification failures and ranks the smallest edits that would restore compatibility. It keeps the evidence trail attached to each recommendation so you can see which diagnostic, overlap, or specification clause motivated the proposed change.
By default, jugeo repair previews the plan without
touching source files. Add --auto-apply only when you want JuGeo
to commit the safe, mechanical subset of those repairs directly.
CLI command
# Suggest repairs for a buggy file
jugeo repair buggy.py
# Repair against an explicit specification
jugeo repair buggy.py --spec spec.py --max-repairs 3
# Apply machine-safe repairs automatically
jugeo repair buggy.py --spec spec.py --auto-applyPython API
import subprocess
completed = subprocess.run(
["jugeo", "repair", "buggy.py", "--spec", "spec.py", "--format", "json"],
check=True,
capture_output=True,
text=True,
)
print(completed.stdout)
JuGeo Relational Refinement ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ Concrete mymodule:sort_concrete Abstract mymodule:sort_abstract Relation sorted_refinement (2 conditions) Building abstract semantic sheaf... Building concrete semantic sheaf... Computing sheaf morphism phi... Encoding refinement VCs... 12 conditions over 6 opens Discharging refinement conditions... phi[0..5] ✓ Valid descent (5.4 ms) phi[6..11] ✓ Valid descent (4.7 ms) ✓ REFINES Morphism: phi_c0d2e3f1 Total: 10.4 ms | 12 VCs | trust: MACHINE_VERIFIED
Mode Summary
The table below summarizes the key properties of each mode, the mathematical structure used, and when to choose it.
| Mode | CLI flag | Judgment form | Use when |
|---|---|---|---|
| spec Specification Satisfaction | jugeo spec | \(\vdash_{\mathcal{S}} f : \sigma\) | You have a written specification (YAML / decorator) and want to prove the implementation meets it. |
| equiv Equivalence Checking | jugeo equiv | \(\vdash_{\mathcal{B}} f \sim g\) | You refactored or optimized a function and want to confirm the new version behaves identically. |
| bugs Bug Detection | jugeo bugs | \(\check{H}^1(\mathcal{U},\mathcal{F}) \neq 0\) | You want to find inputs that violate properties, trigger exceptions, or cause assertion failures. |
| repair Repair Suggestions | jugeo repair | \(\mathcal{R}(\text{bugs/spec})\) | You want JuGeo to turn a failing file or specification into a concrete repair plan. |