Skip to content

Formal and Code Verifiers

Formal and code verifier routing converts symbolic formula checks and generated code checks into the shared GuardDecision and SafetyEvent contracts.

Failure Semantics

FormalCodeVerifierAdapter keeps verifier uncertainty explicit:

  • contradictory formulae map to halt
  • invalid generated code maps to halt
  • missing formal backends map to warn
  • verifier exceptions map to warn
  • verifier timeouts map to warn
  • source code and formula text are excluded from audit serialisation
  • generated code is not executed by this adapter
from director_ai.core.formal_verification import (
    And,
    FormalCodeVerifierAdapter,
    Not,
    Variable,
)
from director_ai.core.guard_control import RiskEnvelope

adapter = FormalCodeVerifierAdapter(timeout_ms=1000.0)
result = adapter.verify_formula(
    formula=And(Variable("approved"), Not(Variable("approved"))),
    risk_envelope=RiskEnvelope(
        action_category="code",
        reversibility="reversible",
        domain="regulated",
        calibrated_threshold=0.5,
        no_go_threshold=0.85,
    ),
    policy_id="policy.formal.regulated",
    evidence_ref="formal://claim-1",
)

For code, the adapter delegates to verify_code() by default and keeps execution disabled:

result = adapter.verify_code(
    code=generated_code,
    risk_envelope=risk_envelope,
    policy_id="policy.code.regulated",
    api_manifest={"pd": {"read_csv", "DataFrame"}},
    evidence_ref="code://snippet-1",
)

Theorem Backend Selection

Use with_theorem_backend() when a deployment needs an explicit theorem-prover profile. The built-in dpll profile has no optional dependency. The z3 profile uses the director-ai[formal] extra, and the lean profile accepts a caller owned runner so the operator controls the Lean invocation, sandbox, and file system boundary.

adapter = FormalCodeVerifierAdapter.with_theorem_backend("dpll")

lean_adapter = FormalCodeVerifierAdapter.with_theorem_backend(
    "lean",
    lean_runner=run_lean_in_sandbox,
)

The selected backend is recorded in the result sandbox and verifier id, for example formal.dpll or formal.lean.

Code Contracts

verify_code_contract() first runs the structural code verifier. If the code is invalid, the theorem backend is not called. If the code passes structural checks, the formal contract is verified through the selected backend.

result = adapter.verify_code_contract(
    code=generated_code,
    contract=contract_formula,
    risk_envelope=risk_envelope,
    policy_id="policy.code.contract.regulated",
    evidence_ref="code-contract://snippet-1",
)

Audit payloads include evidence references, backend names, and sandbox metadata; they do not include raw source code or raw formula text.

Full API

director_ai.core.formal_verification.adapter.FormalCodeVerifierAdapter 

FormalCodeVerifierAdapter(*, formal_verifier: ReasoningVerifier | None | object = _DEFAULT_FORMAL_VERIFIER, code_verifier: Callable[..., Any] = verify_code, timeout_ms: float = 1000.0, theorem_backend_name: str = 'formal')

Guard-control adapter for formal claims and generated code.

with_theorem_backend classmethod 

with_theorem_backend(backend: str, *, code_verifier: Callable[..., Any] = verify_code, timeout_ms: float = 1000.0, z3_solver: Any | None = None, lean_runner: Callable[[str], Mapping[str, Any]] | None = None) -> FormalCodeVerifierAdapter

Build an adapter with a named theorem-prover backend.

verify_formula 

verify_formula(*, formula: Formula, risk_envelope: RiskEnvelope, policy_id: str, evidence_ref: str) -> FormalCodeVerificationResult

Verify a formula without treating backend absence as success.

verify_code 

verify_code(*, code: str, risk_envelope: RiskEnvelope, policy_id: str, evidence_ref: str, language: str = 'python', known_modules: set[str] | None = None, api_manifest: dict[str, set[str]] | None = None) -> FormalCodeVerificationResult

Verify code structurally without executing it.

verify_code_contract 

verify_code_contract(*, code: str, contract: Formula, risk_envelope: RiskEnvelope, policy_id: str, evidence_ref: str, language: str = 'python', known_modules: set[str] | None = None, api_manifest: dict[str, set[str]] | None = None) -> FormalCodeVerificationResult

Verify generated code structurally, then verify its formal contract.

director_ai.core.formal_verification.adapter.FormalCodeVerificationResult dataclass 

FormalCodeVerificationResult(kind: str, evidence_ref: str, signal: VerifierSignal, guard_decision: GuardDecision, sandbox: Mapping[str, Any])

Tenant-safe formal/code verifier result.

to_dict 

to_dict() -> dict[str, Any]

Serialise without raw formula or source code text.

to_safety_event 

to_safety_event(*, hook_id: str, hook_scope: str = 'agent', request_id: str = '', tenant_id: str = '', latency_ms: float | None = None) -> SafetyEvent

Convert the guard decision to a shared safety event.