A CLI tool that encodes contract term sheets as Z3 SMT constraints and reports logical contradictions — naming the specific conflicting clauses if unsatisfiable.

Two constraint types implemented:

1. Boolean (vesting acceleration) — A double-trigger acceleration clause marked "automatic" is directly contradicted by a board veto clause requiring prior approval. Z3 models this as n == 0 (no preconditions) vs. n > 0 (approval required) — unsatisfiable.

2. Arithmetic (liquidation preferences) — A 2x liquidation preference floor plus a common shareholder minimum can exceed total exit proceeds. Z3 models this as p ≥ preferred_floor ∧ c ≥ common_floor ∧ p + c ≤ proceeds — unsatisfiable when the floors sum above proceeds.

A rules engine can flag clauses that look suspicious. Z3 proves whether the clauses can all be simultaneously satisfied — and when they can't, it returns an unsat core that names exactly which clauses are in conflict. No false positives from vague heuristics; no false negatives from missing a pattern.

This follows the suite's "Claude extracts, deterministic logic decides" doctrine. Claude (or a human) fills in the JSON schema from a real term sheet. Z3 makes the determination.

pip install z3-solver click
python cli.py examples/ts_01_clean.json
python cli.py examples/ts_02_vesting_conflict.json
python cli.py examples/ts_03_preference_conflict.json
python cli.py examples/ts_02_vesting_conflict.json --json-out

Example output — contradiction found:

  Term Sheet : TS-002
  Description: Series B — Planted contradiction: double-trigger automatic acceleration + board veto

  FAIL — 1 contradiction(s) found.

  Conflict 1:
    Clauses : §4.3 Double-Trigger Acceleration + §5.1 Board Approval
    Detail  : "§4.3 Double-Trigger Acceleration" grants automatic acceleration — no further
              preconditions. "§5.1 Board Approval" requires board approval before any
              acceleration takes effect. An obligation that fires automatically cannot
              simultaneously require prior approval.

Example output — no contradictions:

  Term Sheet : TS-001
  Description: Series A — Clean term sheet (no logical contradictions)

  PASS — No logical contradictions found.

Contract clauses are encoded as JSON matching schema.json. Each clause has a clause_name field — this is what appears in the contradiction output.

{
  "term_sheet_id": "TS-002",
  "clauses": {
    "double_trigger_acceleration": {
      "clause_name": "§4.3 Double-Trigger Acceleration",
      "enabled": true,
      "acceleration_is_automatic": true
    },
    "board_veto": {
      "clause_name": "§5.1 Board Approval",
      "applies_to_all_acceleration": true,
      "approval_threshold": "unanimous"
    }
  }
}

pip install pytest
pytest tests/ -v

20 tests, all passing.

z3_encoder.py   — ContractVerifier: two Z3 checks, each using assert_and_track for named unsat cores
cli.py          — Click CLI: human-readable output + --json-out mode
schema.json     — JSON Schema (draft-07) defining valid clause structure
examples/       — Three term sheets: 1 clean, 2 with planted contradictions
tests/          — 20 pytest tests covering file-based and inline term sheets

• §4.4 Single-Trigger Acceleration + §5.1 Board Approval variant
• Date/period constraints (notice period contradicting exercise window)
• Claude-powered intake: paste a real term sheet, Claude extracts the JSON, Z3 verifies it

Python · z3-solver · click · pytest