Verification

Z3 and angr backends, CEGAR orchestrator, verification types, and harness builder.

Verification backends for formal property checking (M5).

Provides abstract verification interface with Z3 (constraint solving), angr (Docker-based symbolic execution), and mock backends.

Decision: D-016

class curate_ipsum.verification.Budget(timeout_s=30, max_states=50000, max_path_len=200, max_loop_iters=5)

Bases: object

Resource bounds for a single verification run.

Mirrors the budget schema in angr_adapter_baseline/schemas/request.schema.json.

Parameters:

• timeout_s (int)

• max_states (int)

• max_path_len (int)

• max_loop_iters (int)

timeout_s: int = 30

max_states: int = 50000

max_path_len: int = 200

max_loop_iters: int = 5

escalate(factor=2.0)

Return a new Budget with all limits scaled by factor.

Parameters:

factor (float)

Return type:

Budget

to_dict()

Return type:

dict[str, Any]

classmethod from_dict(d)

Parameters:

d (dict[str, Any])

Return type:

Budget

class curate_ipsum.verification.Counterexample(model=<factory>, trace=<factory>, path_constraints=<factory>, notes=<factory>)

Bases: object

A concrete counterexample found by a verification backend.

Parameters:

• model (dict[str, Any])

• trace (list[dict[str, Any]])

• path_constraints (list[str])

• notes (dict[str, Any])

model: dict[str, Any]

trace: list[dict[str, Any]]

path_constraints: list[str]

notes: dict[str, Any]

to_dict()

Return type:

dict[str, Any]

classmethod from_dict(d)

Parameters:

d (dict[str, Any])

Return type:

Counterexample

class curate_ipsum.verification.SymbolSpec(name, kind='int', bits=64, length=None)

Bases: object

A symbolic variable declaration for the verification request.

Parameters:

• name (str)

• kind (str)

• bits (int)

• length (int | None)

name: str

kind: str = 'int'

bits: int = 64

length: int | None = None

to_dict()

Return type:

dict[str, Any]

classmethod from_dict(d)

Parameters:

d (dict[str, Any])

Return type:

SymbolSpec

class curate_ipsum.verification.VerificationRequest(target_binary, entry, symbols=<factory>, constraints=<factory>, find_kind='addr_reached', find_value='', avoid_kind=None, avoid_value=None, budget=<factory>, metadata=<factory>, notes=None)

Bases: object

A complete verification request, matching request.schema.json.

Parameters:

• target_binary (str)

• entry (str)

• symbols (list[SymbolSpec])

• constraints (list[str])

• find_kind (str)

• find_value (str)

• avoid_kind (str | None)

• avoid_value (str | None)

• budget (Budget)

• metadata (dict[str, Any])

• notes (str | None)

target_binary: str

entry: str

symbols: list[SymbolSpec]

constraints: list[str]

find_kind: str = 'addr_reached'

find_value: str = ''

avoid_kind: str | None = None

avoid_value: str | None = None

budget: Budget

metadata: dict[str, Any]

notes: str | None = None

to_dict()

Return type:

dict[str, Any]

to_json()

Return type:

str

classmethod from_dict(d)

Parameters:

d (dict[str, Any])

Return type:

VerificationRequest

class curate_ipsum.verification.VerificationResult(id=<factory>, status=VerificationStatus.NO_CE_WITHIN_BUDGET, counterexample=None, stats=<factory>, logs=None)

Bases: object

Result from a verification backend, matching response.schema.json.

Parameters:

• id (str)

• status (VerificationStatus)

• counterexample (Counterexample | None)

• stats (dict[str, Any])

• logs (str | None)

id: str

status: VerificationStatus = 'no_ce_within_budget'

counterexample: Counterexample | None = None

stats: dict[str, Any]

logs: str | None = None

to_dict()

Return type:

dict[str, Any]

classmethod from_dict(d)

Parameters:

d (dict[str, Any])

Return type:

VerificationResult

class curate_ipsum.verification.VerificationStatus(*values)

Bases: StrEnum

Outcome of a verification run.

CE_FOUND = 'ce_found'

NO_CE_WITHIN_BUDGET = 'no_ce_within_budget'

ERROR = 'error'

Core data models for the verification subsystem.

Uses dataclasses consistent with synthesis.models pattern (D-012). All models support dict serialization for JSON exchange with Docker runners.

class curate_ipsum.verification.types.VerificationStatus(*values)

Bases: StrEnum

Outcome of a verification run.

CE_FOUND = 'ce_found'

NO_CE_WITHIN_BUDGET = 'no_ce_within_budget'

ERROR = 'error'

class curate_ipsum.verification.types.Budget(timeout_s=30, max_states=50000, max_path_len=200, max_loop_iters=5)

Bases: object

Resource bounds for a single verification run.

Mirrors the budget schema in angr_adapter_baseline/schemas/request.schema.json.

Parameters:

• timeout_s (int)

• max_states (int)

• max_path_len (int)

• max_loop_iters (int)

timeout_s: int = 30

max_states: int = 50000

max_path_len: int = 200

max_loop_iters: int = 5

escalate(factor=2.0)

Return a new Budget with all limits scaled by factor.

Parameters:

factor (float)

Return type:

Budget

to_dict()

Return type:

dict[str, Any]

classmethod from_dict(d)

Parameters:

d (dict[str, Any])

Return type:

Budget

class curate_ipsum.verification.types.SymbolSpec(name, kind='int', bits=64, length=None)

Bases: object

A symbolic variable declaration for the verification request.

Parameters:

• name (str)

• kind (str)

• bits (int)

• length (int | None)

name: str

kind: str = 'int'

bits: int = 64

length: int | None = None

to_dict()

Return type:

dict[str, Any]

classmethod from_dict(d)

Parameters:

d (dict[str, Any])

Return type:

SymbolSpec

class curate_ipsum.verification.types.VerificationRequest(target_binary, entry, symbols=<factory>, constraints=<factory>, find_kind='addr_reached', find_value='', avoid_kind=None, avoid_value=None, budget=<factory>, metadata=<factory>, notes=None)

Bases: object

A complete verification request, matching request.schema.json.

Parameters:

• target_binary (str)

• entry (str)

• symbols (list[SymbolSpec])

• constraints (list[str])

• find_kind (str)

• find_value (str)

• avoid_kind (str | None)

• avoid_value (str | None)

• budget (Budget)

• metadata (dict[str, Any])

• notes (str | None)

target_binary: str

entry: str

symbols: list[SymbolSpec]

constraints: list[str]

find_kind: str = 'addr_reached'

find_value: str = ''

avoid_kind: str | None = None

avoid_value: str | None = None

budget: Budget

metadata: dict[str, Any]

notes: str | None = None

to_dict()

Return type:

dict[str, Any]

to_json()

Return type:

str

classmethod from_dict(d)

Parameters:

d (dict[str, Any])

Return type:

VerificationRequest

class curate_ipsum.verification.types.Counterexample(model=<factory>, trace=<factory>, path_constraints=<factory>, notes=<factory>)

Bases: object

A concrete counterexample found by a verification backend.

Parameters:

• model (dict[str, Any])

• trace (list[dict[str, Any]])

• path_constraints (list[str])

• notes (dict[str, Any])

model: dict[str, Any]

trace: list[dict[str, Any]]

path_constraints: list[str]

notes: dict[str, Any]

to_dict()

Return type:

dict[str, Any]

classmethod from_dict(d)

Parameters:

d (dict[str, Any])

Return type:

Counterexample

class curate_ipsum.verification.types.VerificationResult(id=<factory>, status=VerificationStatus.NO_CE_WITHIN_BUDGET, counterexample=None, stats=<factory>, logs=None)

Bases: object

Result from a verification backend, matching response.schema.json.

Parameters:

• id (str)

• status (VerificationStatus)

• counterexample (Counterexample | None)

• stats (dict[str, Any])

• logs (str | None)

id: str

status: VerificationStatus = 'no_ce_within_budget'

counterexample: Counterexample | None = None

stats: dict[str, Any]

logs: str | None = None

to_dict()

Return type:

dict[str, Any]

classmethod from_dict(d)

Parameters:

d (dict[str, Any])

Return type:

VerificationResult

Abstract verification backend interface.

Mirrors D-001/D-012/D-014 pattern: abstract base class with factory function for runtime backend selection.

Decision: D-016

class curate_ipsum.verification.backend.VerificationBackend

Bases: ABC

Abstract interface for verification backends.

Implementations must handle: - Accepting a VerificationRequest - Running verification within budget constraints - Returning a VerificationResult

Follows the same ABC + factory pattern as GraphStore (D-014) and LLMClient (D-012).

abstractmethod async verify(request)

Run verification on the given request.

Returns VerificationResult with status, optional counterexample, and execution statistics.

Parameters:

request (VerificationRequest)

Return type:

VerificationResult

abstractmethod supports()

Declare what this backend supports.

Returns a dict describing supported input types, constraint kinds, find/avoid predicates, etc. Used by the orchestrator to route requests to capable backends.

Example:

{"input": "binary", "constraints": ["comparison"], "find": ["addr_reached"], "avoid": ["addr_avoided"]}

Return type:

dict[str, Any]

async close()

Release backend resources. Override if needed.

Return type:

None

curate_ipsum.verification.backend.build_verification_backend(backend, **kwargs)

Factory: create a VerificationBackend of the requested type.

Parameters:

• backend (str) – “z3”, “angr”, or “mock”

• **kwargs (Any) – Backend-specific configuration

Returns:

VerificationBackend instance

Raises:

• ValueError – Unknown backend

• ImportError – Backend dependencies not installed

Return type:

VerificationBackend

Z3 constraint-solving verification backend.

Handles constraint satisfaction queries using the Z3 SMT solver. This is the “cheap” tier in the CEGAR budget chain (Z3 → angr → KLEE).

Decision: D-016

class curate_ipsum.verification.backends.z3_backend.Z3Backend(**kwargs)

Bases: VerificationBackend

Verification via Z3 SMT solver.

Parses the mini-DSL constraints from VerificationRequest, constructs Z3 bitvector expressions, and checks satisfiability.

Supported find kinds: return_value, assertion_failed, custom. Does NOT support addr_reached (use angr for that).

Parameters:

kwargs (Any)

supports()

Declare what this backend supports.

Returns a dict describing supported input types, constraint kinds, find/avoid predicates, etc. Used by the orchestrator to route requests to capable backends.

Example:

{"input": "binary", "constraints": ["comparison"], "find": ["addr_reached"], "avoid": ["addr_avoided"]}

Return type:

dict[str, Any]

async verify(request)

Run verification on the given request.

Returns VerificationResult with status, optional counterexample, and execution statistics.

Parameters:

request (VerificationRequest)

Return type:

VerificationResult

angr Docker-based symbolic execution backend.

Runs angr inside a Docker container, communicating via JSON files mounted into the container.

Build the image with: docker compose –profile verify build Run standalone: docker compose run –rm angr-runner

The runner script (verification/runners/run_angr.py) is baked into the image via docker/Dockerfile.angr-runner.

Decision: D-016

class curate_ipsum.verification.backends.angr_docker.AngrDockerBackend(docker_image='curate-ipsum-angr-runner', runner_script=None, runner_script_host_path=None, work_dir=None, **kwargs)

Bases: VerificationBackend

Verification via angr symbolic execution in Docker.

Workflow: 1. Write VerificationRequest JSON to a temp directory 2. Run Docker container with request + binary mounted 3. Read VerificationResult JSON from output 4. Clean up temp artifacts

Requires Docker to be available on the host.

Parameters:

• docker_image (str)

• runner_script (str | None)

• runner_script_host_path (str | None)

• work_dir (str | None)

• kwargs (Any)

supports()

Declare what this backend supports.

Returns a dict describing supported input types, constraint kinds, find/avoid predicates, etc. Used by the orchestrator to route requests to capable backends.

Example:

{"input": "binary", "constraints": ["comparison"], "find": ["addr_reached"], "avoid": ["addr_avoided"]}

Return type:

dict[str, Any]

async verify(request)

Run verification on the given request.

Returns VerificationResult with status, optional counterexample, and execution statistics.

Parameters:

request (VerificationRequest)

Return type:

VerificationResult

Mock verification backend for testing.

Mirrors the angr_adapter_baseline mock with additional call logging. Three modes: “ce” (always finds counterexample), “no_ce” (always safe), “error” (always errors).

class curate_ipsum.verification.backends.mock.MockBackend(mode='no_ce', **kwargs)

Bases: VerificationBackend

Mock verification backend for testing and CI.

Modes:

“ce” - Always returns a counterexample “no_ce” - Always returns no_ce_within_budget “error” - Always returns an error

Parameters:

• mode (str)

• kwargs (Any)

supports()

Declare what this backend supports.

Returns a dict describing supported input types, constraint kinds, find/avoid predicates, etc. Used by the orchestrator to route requests to capable backends.

Example:

{"input": "binary", "constraints": ["comparison"], "find": ["addr_reached"], "avoid": ["addr_avoided"]}

Return type:

dict[str, Any]

async verify(request)

Run verification on the given request.

Returns VerificationResult with status, optional counterexample, and execution statistics.

Parameters:

request (VerificationRequest)

Return type:

VerificationResult

Verification orchestrator: CEGAR loop with budget escalation.

Chains cheap verification (Z3) → expensive (angr) with escalating budgets. Optionally checks for spurious counterexamples.

Decision: D-016

class curate_ipsum.verification.orchestrator.OrchestratorResult(status='unknown', counterexample=None, iterations=0, total_elapsed_s=0.0, backend_results=<factory>, logs=<factory>)

Bases: object

Aggregated result from the orchestrator’s CEGAR loop.

Parameters:

• status (str)

• counterexample (Counterexample | None)

• iterations (int)

• total_elapsed_s (float)

• backend_results (list[dict[str, Any]])

• logs (list[str])

status: str = 'unknown'

counterexample: Counterexample | None = None

iterations: int = 0

total_elapsed_s: float = 0.0

backend_results: list[dict[str, Any]]

logs: list[str]

to_dict()

Return type:

dict[str, Any]

class curate_ipsum.verification.orchestrator.VerificationOrchestrator(backend, budget_presets=None, spurious_checker=None, max_iterations=5)

Bases: object

CEGAR-style orchestrator with budget escalation.

Runs verification across one or more backends with progressively larger budgets. Supports spurious CE checking via a callback.

Usage:

orch = VerificationOrchestrator(backend=z3_backend)
result = await orch.run(request)

Parameters:

• backend (VerificationBackend)

• budget_presets (list[Budget] | None)

• spurious_checker (Callable[[Counterexample], bool] | None)

• max_iterations (int)

async run(request)

Run CEGAR loop with budget escalation.

For each budget preset: 1. Run verification with that budget 2. If CE found, check if spurious (if checker provided) 3. If spurious, escalate budget and retry 4. If confirmed CE or budget exhausted, return

Parameters:

request (VerificationRequest)

Return type:

OrchestratorResult

async run_multi_backend(request, backends)

Run verification across multiple backends (cheap → expensive).

Stops at the first backend that finds a confirmed CE or errors. Falls through to the next backend on no_ce_within_budget.

Parameters:

• request (VerificationRequest)

• backends (list[VerificationBackend])

Return type:

OrchestratorResult

Harness builder: generates minimal C harness binaries from function specifications.

Compiles with gcc -O0 -g -fno-inline to preserve symbol information for angr symbolic execution.

Decision: D-016

class curate_ipsum.verification.harness.builder.HarnessSpec(function_name, parameters=<factory>, violation_condition='', includes=<factory>, extra_code='')

Bases: object

Specification for generating a C harness.

Parameters:

• function_name (str)

• parameters (list[dict[str, str]])

• violation_condition (str)

• includes (list[str])

• extra_code (str)

function_name: str

parameters: list[dict[str, str]]

violation_condition: str = ''

includes: list[str]

extra_code: str = ''

class curate_ipsum.verification.harness.builder.HarnessBuilder(cc='gcc', cflags=None)

Bases: object

Builds C harness binaries from specifications.

Usage:

builder = HarnessBuilder()
binary_path = builder.build(spec, output_dir="/tmp/harnesses")

Parameters:

• cc (str)

• cflags (list[str] | None)

generate_source(spec)

Generate C source code for the harness.

Parameters:

spec (HarnessSpec)

Return type:

str

build(spec, output_dir=None)

Generate and compile a harness binary.

Returns the path to the compiled binary.

Parameters:

• spec (HarnessSpec)

• output_dir (str | None)

Return type:

str

build_from_spec(function_name, params, violation, output_dir=None)

Convenience: build a harness from individual arguments.

Parameters:

• function_name (str)

• params (list[dict[str, str]])

• violation (str)

• output_dir (str | None)

Return type:

str