Skip to main content

crp.vr

Auto-generated reference for the crp.vr subpackage.

vr

crp.vr

Verification Relay (SPEC-049).

ExecVerifier

Verify arithmetic claims by deterministic, sandboxed execution.

applies(claim)

Apply to arithmetic claims that carry a formal expr field.

verify(claim, context)

Execute formal["expr"] and compare with formal["expected"].

Claim dataclass

A single reasoning step or assertion to be verified.

Verdict

Bases: str, Enum

Possible outcomes of a verification attempt.

VerificationResult dataclass

Result returned by every verifier.

Verifier

Bases: Protocol

Protocol implemented by every verifier plugged into the relay.

applies(claim)

Return True if this verifier can decide claim.

verify(claim, context)

Verify claim and return a VerificationResult.

ProcessRewardVerifier

Step-level reasoning verifier backed by a small classifier.

applies(claim)

Apply to inference steps that are not formally checkable.

verify(claim, context)

Score whether claim is entailed by its premises.

VerificationRelay

Coordinate symbolic and probabilistic verifiers over a reasoning trace.

Parameters:

Name	Type	Description	Default
verifiers	list[Any] | None	Override the default verifier list. Defaults to symbolic verifiers first, then the PRM.	None
max_repairs	int	Maximum repair attempts per claim before giving up.	2
min_depth_for_prm	set[str] | None	Depths at which the probabilistic verifier is run. Symbolic verifiers run regardless of depth (SPEC-049 §1.5).	None

verify_trace(claims, context=None, repair_fn=None, depth='thorough')

Verify every claim, repair INVALID ones, and return a report.

Parameters:

Name	Type	Description	Default
claims	list[Claim]	Reasoning steps/assertions extracted from the trace.	required
context	dict[str, Any] | None	Optional shared context passed to each verifier.	None
repair_fn	Callable[[Claim, str], Claim] | None	fn(claim, critique) -> revised_claim. Defaults to no-op.	None
depth	str	Request depth; PRM is skipped unless depth is in min_depth_for_prm.	'thorough'

Returns:

Type	Description
dict[str, Any]	A report dict containing verification_ratio, tier_cap, risk_floor,
dict[str, Any]	step labels, and counts.

Z3Verifier

Sound SMT verification for arithmetic/constraint claims.

applies(claim)

Apply to constraint-style claims with a formal claim to prove.

verify(claim, context)

Prove or disprove that the claim follows from its premises.

extract_claims(text)

Extract checkable claims from text.

Returns:

Type	Description
list[Claim]	A list of Claim objects suitable for VerificationRelay.verify_trace.

verify_text(text, depth='thorough', context=None)

Convenience helper: extract claims from text and verify them.

Parameters:

Name	Type	Description	Default
text	str	Output text to verify.	required
depth	str	Request depth; PRM is skipped unless thorough/exhaustive.	'thorough'
context	dict[str, Any] | None	Optional verifier context.	None

Returns:

Type	Description
dict[str, Any]	Verification report dict (or a no-op report if no claims extracted).

vr.exec_verifier

crp.vr.exec_verifier

Sandboxed executor verifier for computational claims (SPEC-049 §1.3.3).

Deterministically evaluates arithmetic expressions supplied in a structured formal field. The expression is executed in a locked-down subprocess using the same Python interpreter, isolated with -I and a minimal environment.

ExecVerifier

Verify arithmetic claims by deterministic, sandboxed execution.

applies(claim)

Apply to arithmetic claims that carry a formal expr field.

verify(claim, context)

Execute formal["expr"] and compare with formal["expected"].

vr.extract

crp.vr.extract

Lightweight claim extraction for the Verification Relay (SPEC-049).

Turns raw model text into checkable Claim objects. This starter extractor is intentionally rule-based: it surfaces arithmetic equations and simple constraint patterns so symbolic verifiers can decide them without a trained model. More sophisticated extraction (NLI parsing, equation detection, etc.) can be plugged in as an additional verifier or extractor.

extract_claims(text)

Extract checkable claims from text.

Returns:

Type	Description
list[Claim]	A list of Claim objects suitable for VerificationRelay.verify_trace.

verify_text(text, depth='thorough', context=None)

Convenience helper: extract claims from text and verify them.

Parameters:

Name	Type	Description	Default
text	str	Output text to verify.	required
depth	str	Request depth; PRM is skipped unless thorough/exhaustive.	'thorough'
context	dict[str, Any] | None	Optional verifier context.	None

Returns:

Type	Description
dict[str, Any]	Verification report dict (or a no-op report if no claims extracted).

vr.interface

crp.vr.interface

Verification Relay interface (SPEC-049 §1.3.1).

All symbolic and probabilistic verifiers implement the same Verifier protocol so the relay can dispatch uniformly. A Claim is a single reasoning step or checkable assertion extracted from a trace.

Verdict

Bases: str, Enum

Possible outcomes of a verification attempt.

VerificationResult dataclass

Result returned by every verifier.

Claim dataclass

A single reasoning step or assertion to be verified.

Verifier

Bases: Protocol

Protocol implemented by every verifier plugged into the relay.

applies(claim)

Return True if this verifier can decide claim.

verify(claim, context)

Verify claim and return a VerificationResult.

vr.prm

crp.vr.prm

Process Reward Model verifier for non-formal inference steps (SPEC-049 §1.3.4).

This is the probabilistic DPE stage 14. When transformers is available it runs a small text-classifier under the millisecond budget managed by :mod:crp.ml; otherwise it returns UNKNOWN so the relay remains functional in zero-dependency mode. Labels produced by symbolic verifiers can be harvested to fine-tune this model (the verification flywheel).

ProcessRewardVerifier

Step-level reasoning verifier backed by a small classifier.

applies(claim)

Apply to inference steps that are not formally checkable.

verify(claim, context)

Score whether claim is entailed by its premises.

vr.relay

crp.vr.relay

Verification Relay orchestrator (SPEC-049 §1.3.5).

Dispatches verifiers over a reasoning trace, runs a bounded LLM-Modulo generate-critique-repair loop when a verifier returns INVALID, and produces a report that caps the quality tier and raises the risk floor when unrepaired INVALID steps remain.

VerificationRelay

Coordinate symbolic and probabilistic verifiers over a reasoning trace.

Parameters:

Name	Type	Description	Default
verifiers	list[Any] | None	Override the default verifier list. Defaults to symbolic verifiers first, then the PRM.	None
max_repairs	int	Maximum repair attempts per claim before giving up.	2
min_depth_for_prm	set[str] | None	Depths at which the probabilistic verifier is run. Symbolic verifiers run regardless of depth (SPEC-049 §1.5).	None

verify_trace(claims, context=None, repair_fn=None, depth='thorough')

Verify every claim, repair INVALID ones, and return a report.

Parameters:

Name	Type	Description	Default
claims	list[Claim]	Reasoning steps/assertions extracted from the trace.	required
context	dict[str, Any] | None	Optional shared context passed to each verifier.	None
repair_fn	Callable[[Claim, str], Claim] | None	fn(claim, critique) -> revised_claim. Defaults to no-op.	None
depth	str	Request depth; PRM is skipped unless depth is in min_depth_for_prm.	'thorough'

Returns:

Type	Description
dict[str, Any]	A report dict containing verification_ratio, tier_cap, risk_floor,
dict[str, Any]	step labels, and counts.

vr.z3_verifier

crp.vr.z3_verifier

Symbolic SMT verifier for arithmetic and logical constraints (SPEC-049 §1.3.2).

When z3-solver is installed this verifier is sound: a VALID verdict is a proof and confidence is 1.0. Without z3 it falls back to a lightweight, bounded pure-Python evaluator so that symbolic verification still runs in zero-dependency mode (confidence remains 1.0 only for deductive cases that the fallback can close).

Z3Verifier

Sound SMT verification for arithmetic/constraint claims.

applies(claim)

Apply to constraint-style claims with a formal claim to prove.

verify(claim, context)

Prove or disprove that the claim follows from its premises.