Touchstone

An SMT-based verifier for a subset of Python. Touchstone takes a function and a property and returns PROVED (it holds for all inputs), REFUTED (with a counterexample), or UNKNOWN (with a reason), by translating the code to Z3 rather than running it. Every PROVED is corroborated by a second solver (cvc5) and rests on a trust base machine-checked in Rocq.

pip install touchstone-prover

import touchstone as t

# state the property in Python, over the parameters and `result`
t.prove("def f(x):\n    return x + x\n", "result == 2 * x").status        # 'PROVED'

# or write the contract as decorators on the function itself
t.verify_contracts('''
@require("n >= 0")
@ensure("result == n")
def count(n):
    i = 0
    while i < n:
        i = i + 1
    return i
''').status                                                              # 'PROVED'

# or check two implementations agree on every input
t.verify_equiv("double", "f", "def f(a):\n    return a + a\n",
               "def g(a):\n    return 2 * a\n", {}).status                # 'PROVED'

Benchmarks

On the hand-written TypeEvalPy micro-benchmark, ranked by exact match (a matched type set at the exact source position, the metric the benchmark ranks by):

Tool	Kind	Exact matches
Touchstone	static	841 / 868
Sonnet 4.6	LLM	824 / 868
Opus 4.8	LLM	822 / 868
gpt-4o	LLM	806 / 860
HeaderGen	static	564 / 845
Jedi	static	415 / 845
Pyright	static	405 / 845
HiTyper-DL	hybrid (ML)	369 / 845
Haiku 4.5	LLM	281 / 868 (abstained on 466)
HiTyper	static	250 / 845
Scalpel	static	193 / 845
Type4Py	ML	157 / 845

Sonnet 4.6, Opus 4.8, and Touchstone are scored on the same 868-fact commit, so those three are a controlled comparison: Touchstone leads at 841, ahead of the two frontier models (824 and 822, themselves a two-fact gap inside the noise). gpt-4o's 806 is on a different commit (860 facts) and the paper's tools on a third (845), so their placement is a looser comparison. Haiku 4.5 is the outlier: it answered "unknown" on 466 of the 868 slots, so its 281 reflects abstention rather than wrong inference, and it was about 70 percent accurate on the 402 it did commit to. Touchstone is the only deterministic, reproducible, machine-checked tool at the top, and on the same-commit set it now matches more facts than the frontier LLMs do. The static and ML figures are from the TypeEvalPy paper, gpt-4o from the project's LLM evaluation, and the Claude models through the same emit-and-match harness. The verifier's own gate is python -m touchstone.ci (self-tests, soundness audits against CPython, and a verification benchmark, all required to pass) plus the Rocq proof check.

Command line

The verbs run from the shell, with the process exit status mirroring the verdict (0 PROVED, 1 REFUTED, 2 UNKNOWN) so they compose in CI:

touchstone check  d.py                            # trap freedom (and any asserts) for all inputs
touchstone prove  f.py --ensures 'result == x'    # a postcondition over the parameters and `result`
touchstone verify count.py                        # the @require / @ensure contracts written in a file
touchstone equiv  impl.py spec.py --func f        # two implementations agree on every input
touchstone change before.py after.py              # an edit preserves the code's properties (gate an AI diff)
touchstone repo   pkg/                            # triage trap freedom across a package
touchstone gate   --base HEAD~1                   # gate a diff in CI: only the changed functions
touchstone spec   f.py                            # synthesize a contract the function provably satisfies
touchstone infer  m.py                            # sound over-approximate types of a return and its locals
touchstone covers                                 # what it can prove, the modeled subset, the trust base

A refutation comes back with the counterexample and the path it took; add --repro and the same command also emits a runnable failing test that reproduces it. An UNKNOWN is labeled budget (raise --budget), approximation (a sound over-approximation it will not certify), or unmodeled (a construct outside the subset, named with its line) so the next step is clear.

$ touchstone prove f.py --ensures 'result == x'
REFUTED  [property via verified VC generator (Rocq-extracted wpg)]
  counterexample: x=0
  trace:
    line 2: return x + 1    [x=0]
    => returns 1

What it covers

Functional equivalence and predicates; whole-function and interprocedural reasoning over control flow with multiple loops, arbitrary nesting, break and continue, and any step direction; self-recursion, mutual recursion, and recursion over lists; whole-program verification across module boundaries through the call graph, so a callee's trap is seen at the caller; deductive and synthesized loop invariants; abstract interpretation (interval, zone, octagon, Karr, polyhedra, machine-integer); IEEE-754 floating point total over every double, with Inf and NaN as first-class inputs, exact floor division and modulo, and sound over-approximations of sin, cos, exp, and log; arrays with quantified specifications; termination and cost of counted, container, and data-dependent loops; exceptions; rely-guarantee concurrency for all schedules and depths; and separation logic with the frame rule, the magic wand, and inductive heap predicates.

Values carry their real types through the symbolic core; the heap models object identity, aliasing, and mutation; a sequence index is checked against the container's length and a dict key against the keys provably present, so a guarded access is proved safe and an unguarded one refuted with the witness. These, with None in arithmetic, type mismatches, division by zero, and (alongside every integer proof) fixed-width overflow, are the traps that refute a totality claim.

A property is stated in Python over the parameters and result (prove), with len, indexing, membership, old(e) for the entry value, and bounded all / any over a concrete range or literal; written as @require / @ensure decorators (verify_contracts); mined from the code's own assertions (check); or given as a Z3 predicate. A counterexample comes back with its execution trace (explain) and, on request, a failing test (repro_test).

The modeled subset

Touchstone is sound by construction in three tiers of trust: a machine-checked core (the integer IR and its weakest-precondition generators, the fixed-width and division/modulo encodings, the interval transfers, and the further encoders below, all proved in Rocq and run as extracted code); an engine-modeled subset (everything in "What it covers", modeled soundly and cross-checked against CPython, but not each individually proved); and everything else, which returns UNKNOWN with a reason rather than a guess. touchstone covers prints the tiers and coverage_report() measures the modeled fraction.

What returns UNKNOWN, always named, never guessed:

a decorator that is not a visible simple wrapper (an @D(args) factory, an attribute or invisible decorator), and a custom metaclass or __init_subclass__ hook (the resolvable type(name, bases, ns) form is modeled);
dynamic reflection that is not statically resolvable: getattr / setattr with a non-literal name, hasattr, and eval / exec / compile;
*args / **kwargs beyond a constant f(*tuple) splat, and a call into a body the engine cannot see (a C extension, an unmodeled builtin) with no value or result-type model;
exception control flow beyond raise / try / except / finally over the named trap types;
operators with no sound encoding in the active theory: float **, matrix @, and bitwise & | ^ between unbounded-integer variables outside the a & (2**k - 1) idiom; min / max over a possibly-empty iterable; round(float, n) to an exact value;
a generator with branching control flow (the object is total; its lazily-yielded elements are left to the consumer), and a possible read-before-assignment;
a nonlinear or hard query left undecided within the deterministic budget, where a larger one is available with --budget high.

Soundness

Every construct is encoded soundly or returned as UNKNOWN with a reason, so an unsupported feature is never silently skipped or assumed away. A PROVED is confirmed by a second independent solver (cvc5); a verdict cvc5 actively refutes is reported as a prover bug rather than trusted, and when cvc5 is absent the PROVED degrades to a clearly-labeled single-solver result rather than vanishing. Verification runs under a deterministic resource bound, so identical input yields an identical verdict on every machine, and carries a reproducibility certificate; proof_bundle exports it as a re-checkable bundle (the discharged SMT-LIB queries, the solver versions, the configuration, and a content hash) that recheck_bundle or any SMT solver re-verifies independently. prove / verify / check establish partial correctness (no trap and the postcondition holds, not termination, which is the separate verify_total / check --total); a true property that exceeds the default bound and comes back UNKNOWN can be retried at --budget high, so incompleteness is visible.

The trust base is machine-checked in Rocq (proofs/), every theorem closed under the global context with no axioms and no Admitted: the operational semantics of the modeled subset; the VC generator over it (sound and complete for straight-line assignment and conditionals, sound for while-loops carrying an invariant, trap-aware); a fixed-width two's-complement model proven to agree with unbounded arithmetic exactly when no operation overflows; the division and modulo encoding proven to refine the SMT-LIB theory for every conforming solver; the abstract-domain transfers; the type-inference lattice join; the string, container, and heap McCarthy-array (read-after-write and frame) laws; the separation-logic frame rule; the rely-guarantee concurrency principle; the float divmod laws (over the rationals the IEEE-754 doubles inhabit, so the proof is axiom-free); the translation as a semantics-preserving functor; and the end-to-end theorem that a discharged verification condition implies the property. SMTCoq additionally re-checks each integer obligation's certificate inside Coq's kernel.

The VC generators, the interval operators, the // / % encoding, and the type-lattice join are extracted from those proofs; the engine runs the Python image of that extraction directly, and a shipped audit holds each module byte-for-byte equal to the committed JSON extraction on every install with no Coq toolchain. So the code that runs is the one proven correct in Rocq. With that core verified, the random differential checks against CPython are a completeness regression measuring precision, and machine-generated fuzz corpora (integer, sequence, recursion, while-invariant, and interprocedural) feed code no human wrote through the same CPython oracle, holding the trap-freedom verdicts sound on inputs no human chose.

Type inference

The same symbolic core infers types in two modes. infer_types is over-approximating and sound: the reported set of type names is guaranteed to contain the value's runtime type, or the location is left UNKNOWN, so a stated type is never narrower than the truth. emit_facts is best-effort exact in the TypeEvalPy schema and discovers its own targets, carrying argument types across call boundaries, following a value through reassignment and is None / isinstance narrowing, and resolving container element types, dict keys, constructor-set attributes, decorators, and generators.

Recall is the fraction of ground-truth facts matched; precision the fraction of emitted facts that match one. The commit rate is the fraction of locations the heuristic types rather than abstaining, and accuracy where committed is the fraction of those that match; recall is their product.

Evaluation (emit-and-match)	Recall	Precision	Commit	Accuracy (committed)
TypeEvalPy micro-benchmark	804 / 868 (92.6%)	37.5%	95.9%	96.6%
TypeEvalPy autogen suite	73,413 / 77,268 (95.0%)	49.4%	95.5%	99.5%
CPython standard library	1069 / 1218 (87.8%)	92.8%	93.1%	94.3%

Sound mode (infer_types)	Commit rate	Soundness	Exact
TypeEvalPy micro-benchmark	101 / 868 (11.6%)	100%	99.0%
TypeEvalPy autogen suite	13,829 / 77,268 (17.9%)	100%	98.5%
CPython standard library	54 / 1218 (4.4%)	100%	83.3%

The sound mode commits only where the type is fixed independent of the inputs, so its reach is narrower than the heuristic's, but a committed bound is a proven over-approximation, and the runtime type fell inside every one. The TypeEvalPy figures are scored against commit 3719de1; the CPython cross-check ran on 3.13.2 and is the held-out, out-of-distribution measurement (the autogen suite is generated from templates the heuristic was tuned against). Counts and rates move with the benchmark commit and the standard-library version, so the tables are snapshots python -m touchstone.typeeval reproduces. Every type is spelled by its runtime __name__, so a match reflects an inferred type, not a naming convention.

Run

pip install touchstone-prover    # z3-solver and cvc5, pinned in pyproject.toml
python -m touchstone.ci          # self-tests, soundness audits, completeness regressions -> "CI OK"
python -m touchstone.examples    # one runnable example per capability, each verdict asserted
python -m touchstone.typeeval    # type-inference recall + precision (CPython cross-check)
python -m touchstone             # a demonstration

The machine-checked proofs run under the Rocq 9.0 opam switch; verify_coq.sh also runs the SMTCoq certificate check when its separate toolchain (see proofs/toolchain.lock) is present, and skips it cleanly otherwise:

eval "$(opam env --switch=rocq9)" && cd proofs && bash verify_coq.sh

Layout

touchstone/      package: core, domains, engines, theories, vcgen, audit, ci, examples (_impl is the engine)
proofs/          Rocq + SMTCoq proofs, the extracted VC generators + interval operators, verify_coq.sh
.github/         continuous integration: the audits and the proof gate on every change
pyproject.toml   package metadata and pinned Python dependencies

License

MIT. See LICENSE.

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

touchstone_prover-0.14.2.tar.gz (402.2 kB view details)

Uploaded Jun 22, 2026 Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

The dropdown lists show the available interpreters, ABIs, and platforms. Enable javascript to be able to filter the list of wheel files.

touchstone_prover-0.14.2-py3-none-any.whl (413.4 kB view details)

Uploaded Jun 22, 2026 Python 3

File details

Details for the file touchstone_prover-0.14.2.tar.gz.

File metadata

Download URL: touchstone_prover-0.14.2.tar.gz
Upload date: Jun 22, 2026
Size: 402.2 kB
Tags: Source
Uploaded using Trusted Publishing? Yes
Uploaded via: twine/6.1.0 CPython/3.13.12

File hashes

Hashes for touchstone_prover-0.14.2.tar.gz
Algorithm	Hash digest
SHA256	`d3c7b2d8c92a4cc6bb3b4f03bdc963fcb9916ee54de5c345721d7158446214b8`
MD5	`0774aab3366ab7d4567eb73fca8e5b9a`
BLAKE2b-256	`ee03825b24db7d04f8ccb2e303f2ed94b098387fc9b5c15594c4d38b7abac95c`

See more details on using hashes here.

Provenance

The following attestation bundles were made for touchstone_prover-0.14.2.tar.gz:

Publisher: publish.yml on CharlesCNorton/touchstone

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Statement:
- Statement type: https://in-toto.io/Statement/v1
- Predicate type: https://docs.pypi.org/attestations/publish/v1
- Subject name: touchstone_prover-0.14.2.tar.gz
- Subject digest: d3c7b2d8c92a4cc6bb3b4f03bdc963fcb9916ee54de5c345721d7158446214b8
- Sigstore transparency entry: 1911700172
- Sigstore integration time: Jun 22, 2026
Source repository:
- Permalink: CharlesCNorton/touchstone@921cb846ada8012decc86a236a18aef6ad2467de
- Branch / Tag: refs/tags/v0.14.2
- Owner: https://github.com/CharlesCNorton
- Access: public
Publication detail:
- Token Issuer: https://token.actions.githubusercontent.com
- Runner Environment: github-hosted
- Publication workflow: publish.yml@921cb846ada8012decc86a236a18aef6ad2467de
- Trigger Event: push