verification package

Reviewed against commit 8a2cb42ad on 2026-10-23.

Reference: generated package page orchestrata_ultimate.verification (66 modules in 9,151 lines of code across the root and 16 subpackages); key modules types, spec_completeness, implementation_scanner, traceability, review, verification engine. The orchestrator reaches the package through its verification_gate (orchestrator); the RTM and spec model it checks against are explained in the orchestrata overview (section 9), and the requirement-checklist parser is in openspec.

The story

orchestrata_ultimate.verification is the Verification Agent (Spec 035, historically Spec 007b) — the part of the pipeline whose job is to refuse to take generated work on faith. Orchestrata's volks produce code and artifacts at speed; something has to answer, formally and repeatably, the question "does this actually satisfy the requirements?" This package is that answer. It turns natural-language requirements into formal constraints, evaluates them (with Prolog and a chain of LLM judges), advances the work through named checkpoints, verifies proofs, runs a deterministic no-LLM code review, applies automated fixes, and — when attempts are exhausted or a requirement is genuinely impossible — escalates to a human rather than declaring false success.

A verification pass flows through a few clearly separated stages. Requirements enter through requirements/requirements_parser.py, which converts natural language into Constraint objects (the shared vocabulary of the whole package lives in types.py: ConstraintType, VerificationStatus, CheckpointName, ProofType, SessionStatus, plus dataclasses like Constraint, VerificationResult, Proof and Suggestion). requirements/prolog_generator.py translates those constraints into Prolog predicates so constraints/evaluator.ConstraintEvaluator can check them mechanically. From there the work advances through the checkpoint machinery — checkpoints/definitions.py names the stages and their criteria, checkpoints/verifier.CheckpointVerifier performs the state transitions, and checkpoints/concurrent.ConcurrentCheckpointEvaluator evaluates them in parallel — while proofs/verifier.ProofVerifier validates the four proof types that supervisors attach to their claims. orchestration/coordinator.VerificationCoordinator conducts this whole workflow, and verification/engine.VerificationEngine is the core engine that produces VerificationResults, with verification/feedback.FeedbackGenerator converting failures into actionable Suggestions that flow back to the executing agent for another attempt.

The package deliberately keeps two verification styles side by side. The LLM side is embodied by three cooperating agent roles in agents/ (an ExecutionAgent that implements, a SupervisorAgent that reviews and generates proofs, and a VerificationAgent that verifies), whose model calls route through the models/ subpackage — an LLMModel protocol behind a ModelRegistry and ModelFallbackChain, with concrete wrappers for Claude Opus, Deepseek R1, Grok/MiniMax and Qwen Max, configured by config/verification_config.py. The deterministic side is the review/ subpackage: run_deterministic_review collects the workspace and runs four check families (correctness, quality, safety, structure) without any model in the loop, then issue_triage.prioritize_issues sorts and caps the findings. When failures are mechanical, autofix/run_all_autofixes repairs them automatically — format, import and Redis fix families each returning an AutofixResult — before the work is re-verified. edge_cases/ and impossibility/ guard the boundaries: known edge cases are stored and detected, and requirements that cannot be satisfied are routed to the ImpossibilityHandler instead of an infinite retry loop, with escalation_handler.EscalationHandler handing the case to a human once max attempts are spent.

Around the edges, the package collaborates with the rest of orchestrata through thin adapters rather than direct coupling: protocols/verification_cxp.VerificationCXPAdapter speaks the CXP message protocol to other agents, integrations/intent_broker.IntentBrokerAdapter connects to the Intent Broker, integrations/redis_manager.VerificationRedisManager persists verification state in Redis, and session/verification_session.VerificationSessionManager tracks long-running verification sessions. Finally, the package root re-exports its spec-conformance surface used project-wide: traceability.py (the standalone @traces-decorator engine that scans source for requirement traces and generates the Requirements Traceability Matrix) and spec_completeness.evaluate_spec_completeness (Prolog-based checklist evaluation) — which is why nearly every module in the dependency graph points at traces and types.

Key responsibilities

• Requirements → constraints → Prolog. Parse natural-language requirements into Constraint objects and compile them into Prolog predicates for mechanical, repeatable evaluation.
• Constraint evaluation. Evaluate constraints one at a time, all at once, or in dependency order, yielding VerificationResults (satisfied / not_met / partial / error / pending).
• Checkpoint gating. Advance work through named checkpoints (core_implementation → unit_tests → integration_tests → documentation → final_verification), sequentially or concurrently, transitioning session state on the result.
• Proof verification. Validate the four proof types (exhaustive_search, logical_deduction, mathematical, practical_explanation) that a Supervisor attaches to a claim.
• Two verification styles. A Prolog/deterministic path and an LLM-judge path (Claude Opus, Deepseek R1, Grok/MiniMax, Qwen Max) behind a fallback chain, so verification degrades gracefully when a model is unavailable.
• Deterministic review + autofix. Run a no-LLM review across correctness/quality/safety/structure, triage the issues, and mechanically repair format/import/Redis problems before re-verifying.
• Actionable feedback loops. Turn failed results into Suggestions that flow back to the Execution Agent for another attempt.
• Boundary handling. Detect edge cases and contradictory/impossible requirements, and escalate to a human once max attempts are exhausted — never declare false success.
• Spec conformance surface. Provide the project-wide @traces traceability engine (RTM generation) and Prolog-based spec-completeness evaluation.

Class diagram

Core data model (types.py)

The dataclasses that flow between every stage. A Constraint enters the pipeline; a VerificationResult or CheckpointResult comes out; a Proof/ProofResult pair carries a supervisor's claim and its verdict; a Suggestion carries feedback back to the executor. (Generated from the AST, render-verified.)

Verification engine core

The Prolog/deterministic evaluation spine: the engine composes a constraint evaluator and a checkpoint verifier; the concurrent evaluator fans checkpoints out; the proof verifier validates the four proof types; the feedback generator turns failures into suggestions. (Generated from the AST, render-verified.)

Agents, orchestration and models

The three cooperating agent roles plus the coordinator that conducts the CXP workflow, and the pluggable LLM layer behind them. LLMModel is a Protocol; ModelFallbackChain structurally satisfies it and wraps an ordered list of models so one failure falls through to the next. (Generated from the AST, render-verified.)

Boundary guards

What stops the pipeline from looping forever or lying about success: escalation to a human, contradiction/impossibility detection, and edge-case detection backed by a small store. (Generated from the AST, render-verified.)

Type hierarchy

The package's inheritance is mostly a set of StrEnum vocabularies plus the LLMModel protocol (generated from the AST, render-verified):

Module dependency diagram

Internal module imports within orchestrata_ultimate.verification (generated from the AST, render-verified):

Module inventory

types.py

types.py is the shared vocabulary the entire package is written in, and the reason nearly every arrow in the dependency diagram converges on types. It defines the five StrEnum families — ConstraintType (functional/quality/performance/security), VerificationStatus (satisfied/not_met/partial/error/pending), CheckpointName (core_implementation → final_verification), ProofType (exhaustive_search/logical_deduction/mathematical/practical_explanation) and SessionStatus (active/completed/failed/escalated) — together with the dataclasses that flow between stages: a Constraint enters the pipeline, a VerificationResult or CheckpointResult comes out, a Proof/ProofResult pair carries a supervisor's claim and its verdict, and a Suggestion carries feedback back to the executor. Because every subpackage (constraints, checkpoints, proofs, agents, orchestration, review) speaks these types, they can be composed freely without knowing about each other's internals.

Class map (generated)

Generated from the live source AST by scripts/gen-module-class-diagrams.py — do not hand-edit. Abstract classes have a green border; members listed are those defined on the class itself (inherited members excluded). Solid empty-triangle arrows = in-package inheritance; dashed arrows into dashed boxes = external/stdlib/cross-package bases; filled diamond = composition (constructed in __init__); open diamond = aggregation (annotated/injected reference); diamond edge labels name the owning attribute.