# Formal Verification

Mathematical verification of agent properties: model checking, theorem proving, and verification for AI systems.

---

## Formal Verification Taxonomy

```
Formal Verification
├── Model Checking
│   ├── Explicit State
│   ├── Symbolic (BDD/SAT/SMT)
│   ├── Bounded Model Checking
│   ├── Probabilistic Model Checking
│   └── Parameterized Model Checking
├── Theorem Proving
│   ├── Interactive (Coq, Lean, Isabelle, Isabelle/HOL)
│   ├── Automated (SMT, ATP)
│   ├── Proof Assistants
│   └── Proof Certificates
├── Deductive Verification
│   ├── Hoare Logic
│   ├── Separation Logic
│   ├── Refinement Types
│   └── Dependent Types
├── Runtime Verification
│   ├── Monitoring
│   ├── Enforcement
│   ├── Predictive
│   └── Statistical
├── Neural Network Verification
│   ├── Robustness
│   ├── Reachability
│   ├── Lipschitz Continuity
│   └── Abstract Interpretation
└── Compositional Verification
    ├── Assume-Guarantee
    ├── Contract-Based
    ├── Interface Theories
    └── Contract-Based Design
```

---

## Model Checking

### Temporal Logic Model Checking
```python
from temporal_logic import LTL, CTL, CTLStar

class ModelChecker:
    def __init__(self, model: TransitionSystem):
        self.model = model
        self.solver = SATSolver()
    
    def check_ltl(self, formula: LTLFormula) -> ModelCheckResult:
        """Check LTL formula on finite-state system"""
        # Translate LTL to Büchi automaton
        buchi = LTL2BA(formula)
        
        # Product construction
        product = self.model.product(buchi)
        
        # Emptiness check (nested DFS)
        return self.emptiness_check(product)
    
    def check_ctl(self, formula: CTLFormula) -> ModelCheckResult:
        """CTL model checking via fixpoint computation"""
        if formula.is_atomic():
            return self.eval_atomic(formula)
        elif formula.is_not():
            return not self.check_ctl(formula.sub)
        elif formula.is_and():
            return self.check_ctl(formula.left) & self.check_ctl(formula.right)
        elif formula.is_ex():
            return self.ex_exists(formula.sub)
        elif formula.is_ax():
            return self.ax_forall(formula.sub)
        elif formula.is_ef():
            return self.ef_reachability(formula.sub)
        elif formula.is_ag():
            return self.ag_invariant(formula.sub)
        elif formula.is_eu():
            return self.eu_until(formula.left, formula.right)
        elif formula.is_au():
            return self.au_until(formula.left, formula.right)

class SymbolicModelChecker:
    def __init__(self, model: SymbolicTransitionSystem):
        self.model = model
        self.bdd = BDDManager()
    
    def check_ctl(self, formula: CTLFormula) -> BDD:
        """Symbolic CTL model checking with BDDs"""
        if formula.is_atomic():
            return self.bdd.var(formula.name)
        elif formula.is_not():
            return ~self.check_ctl(formula.sub)
        elif formula.is_and():
            return self.check_ctl(formula.left) & self.check_ctl(formula.right)
        elif formula.is_ex():
            return self.ex_preimage(self.check_ctl(formula.sub))
        elif formula.is_ex():
            return self.ex_preimage(self.check_ctl(formula.sub))
        elif formula.is_ef():
            return self.reachability(self.check_ctl(formula.sub))
        elif formula.is_af():
            return self.inevitability(self.check_ctl(formula.sub))
```

### Bounded Model Checking (BMC)
```python
class BoundedModelChecker:
    def __init__(self, system: TransitionSystem, solver: SMTSolver):
        self.system = system
        self.solver = solver
    
    def check_safety(self, property: SafetyProperty, max_depth: int) -> BMCResult:
        """Check safety property up to bound k"""
        for k in range(max_depth + 1):
            # Unroll transition relation k times
            formula = self.unroll_transitions(k)
            
            # Add property violation at step k
            formula.add(self.encode_violation(property, k))
            
            # Check satisfiability
            result = self.solver.check(formula)
            
            if result == sat:
                trace = self.extract_counterexample(k)
                return BMCResult(violated=True, counterexample=trace, depth=k)
        
        return BMCResult(violated=False, proof_depth=max_depth)
    
    def unroll_transitions(self, k: int) -> SMTFormula:
        formula = SMTFormula()
        for i in range(k):
            # Add transition relation T(s_i, s_{i+1})
            formula.add(self.system.transition_relation(i, i+1))
        return formula
```

### Probabilistic Model Checking (PRISM)
```python
class ProbabilisticModelChecker:
    def __init__(self, model: ProbabilisticModel):
        self.model = model
    
    def check_pctl(self, formula: PCTLFormula) -> PCTLResult:
        """Probabilistic CTL model checking"""
        if formula.is_p_operator():
            return self.check_probability(formula)
        elif formula.is_steady_state():
            return self.check_steady_state(formula)
        elif formula.is_reward():
            return self.check_reward(formula)
    
    def check_probability(self, formula: PCTLFormula) -> PCTLResult:
        """P_{op}(phi) where op in {<, <=, >=, >}"""
        # Compute probability using linear programming / value iteration
        prob = self.compute_probability(formula.path_formula)
        
        op = formula.operator
        threshold = formula.threshold
        
        satisfied = self.compare(prob, op, threshold)
        
        return PCTLResult(
            satisfied=satisfied,
            probability=prob,
            threshold=threshold
        )

class StatisticalModelChecker:
    def __init__(self, simulator: Simulator):
        self.simulator = simulator
    
    def statistical_model_check(self, formula: PCTLFormula, 
                                alpha: float = 0.05, 
                                delta: float = 0.05) -> SMCResult:
        """Statistical model checking with confidence intervals"""
        # Chernoff-Hoeffding bounds
        n = int(math.log(2/delta) / (2 * epsilon**2))
        
        satisfied = 0
        for _ in range(n):
            trace = self.simulator.simulate()
            if self.evaluate_path(trace, formula):
                satisfied += 1
        
        prob = satisfied / n
        ci = self.confidence_interval(prob, n, confidence=1-alpha)
        
        return SMCResult(
            probability=prob,
            confidence_interval=ci,
            satisfied=self.evaluate_threshold(prob, formula)
        )
```

---

## Theorem Proving

### Interactive Theorem Proving (Coq)
```coq
(* Coq: Agent Safety Specification *)

(* State definition *)
Record AgentState := {
  position : Position;
  velocity : Velocity;
  mode : Mode;
  sensors : SensorData;
  goals : list Goal;
}.

(* Safety property: Agent never enters forbidden zone *)
Theorem safety_property : forall (s : AgentState),
  safe_position s.position -> safe_position (next_position s).
Proof.
  intros s Hsafe.
  (* Proof using invariants and case analysis on mode *)
  destruct s as [pos vel mode sensors goals].
  inversion Hsafe.
  case_eq mode; simpl in *; 
  [ (* autonomous mode *)
    apply autonomous_safe | assumption
  | (* manual mode *)
    apply manual_safe | assumption
  | (* emergency mode *)
    apply emergency_safe | assumption ].
Qed.

(* Liveness: Agent eventually reaches goal *)
Theorem liveness_property : forall (s : AgentState) (g : Goal),
  reachable s g -> 
  exists t, reaches_goal (run_for s t) g.
Proof.
  intros s g Hreach.
  (* Use well-foundedness of distance metric *)
  have Hwf : well_founded (distance_to_goal g).
  apply well_founded_induction with (distance_to_goal g).
  intros s IH.
  destruct (step s) as [s' | contradiction].
  - apply IH; assumption.
  - contradiction.
Qed.
```

### Lean 4 (Modern Theorem Proving)
```lean
-- Lean 4: Agent Safety

structure AgentState where
  position : Position
  velocity : Velocity
  mode : Mode
  sensors : SensorData
  goals : List Goal

def safe_position (p : Position) : Prop :=
  ¬ (p ∈ forbidden_zones)

def next_position (s : AgentState) : Position :=
  match s.mode with
  | Mode.autonomous => autonomous_step s
  | Mode.manual => manual_step s
  | Mode.emergency => emergency_step s

-- Safety theorem: Position remains safe
theorem safety_property (s : AgentState) (h : safe_position s.position) : 
    safe_position (next_position s) := by
  have h₁ : safe_position s.position := h
  have h₂ : safe_position (next_position s) := by
    cases s.mode <;> simp_all [next_position, autonomous_step, manual_step, emergency_step]
    <;> try { aesop }
    <;> try { linarith }
    <;> try { aesop }
  exact h₂

-- Liveness: Eventually reaches goal
theorem liveness (s : AgentState) (g : Goal) (h : Reachable s g) :
    ∃ t, ReachesGoal (run_for s t) g := by
  have h₁ : ∃ t, ReachesGoal (run_for s t) g := by
    classical
    by_contra! h
    -- Use well-foundedness of distance metric
    have h₁ : ∀ t, ¬ReachesGoal (run_for s t) g := by simpa using h
    have h₂ : ∀ t, distance (run_for s t).position g > 0 := by
      intro t
      have h₃ := h₁ t
      simp_all [ReachesGoal, distance_pos]
    -- Contradiction with well-foundedness
    exact absurd (by ...) (well_founded_lt_iff.mpr (fun _ _ => by linarith))
  exact h₁
```

### Automated Theorem Proving (SMT/Z3)
```python
from z3 import *

class AutomatedTheoremProver:
    def __init__(self):
        self.solver = Solver()
        self.solver.set("timeout", 30000)  # 30 second timeout
    
    def prove_safety(self, system: TransitionSystem, 
                     invariant: Invariant) -> ProofResult:
        """Prove invariant holds using induction"""
        # 1. Base case: initial states satisfy invariant
        self.solver.push()
        self.solver.add(system.initial_state())
        self.solver.add(Not(invariant.formula()))
        
        if self.solver.check() == sat:
            self.solver.pop()
            return ProofResult(proven=False, counterexample=self.solver.model())
        
        self.solver.pop()
        
        # 2. Inductive step: invariant preserved by transitions
        self.solver.push()
        self.solver.add(invariant.formula())
        self.solver.add(system.transition_relation())
        self.solver.add(Not(invariant.next_formula()))
        
        if self.solver.check() == sat:
            self.solver.pop()
            return ProofResult(proven=False, counterexample=self.solver.model())
        
        self.solver.pop()
        return ProofResult(proven=True)
    
    def verify_liveness(self, system: TransitionSystem, 
                        liveness: LivenessProperty) -> ProofResult:
        """Prove liveness: something good eventually happens"""
        # Use ranking functions / well-foundedness
        ranking_function = self.synthesize_ranking_function(liveness)
        
        self.solver.push()
        self.solver.add(system.transition_relation())
        self.solver.add(liveness.precondition())
        self.solver.add(Not(liveness.eventually_formula()))
        
        if self.solver.check() == unsat:
            return ProofResult(proven=True, ranking_function=ranking_function)
        
        return ProofResult(proven=False)

class VerificationConditionGenerator:
    def __init__(self):
        self.vcg = VCGenerator()
    
    def generate_vcs(self, program: Program, spec: Specification) -> list[VC]:
        """Generate verification conditions from annotated program"""
        vcs = []
        
        # Precondition -> Postcondition for each function
        for func in program.functions:
            if func.has_spec():
                vc = self.generate_vc(func)
                vcs.append(vc)
        
        # Loop invariants
        for loop in program.loops:
            if loop.has_invariant():
                vcs.append(self.generate_loop_vc(loop))
        
        return vcs
```

---

## Deductive Verification

### Hoare Logic
```python
class HoareLogicVerifier:
    def __init__(self):
        self.rules = {
            'skip': self.rule_skip,
            'assign': self.rule_assign,
            'seq': self.rule_seq,
            'if': self.rule_if,
            'while': self.rule_while,
            'assert': self.rule_assert
        }
    
    def verify(self, program: Program, pre: Formula, post: Formula) -> VerificationResult:
        """Verify {P} C {Q}"""
        # Generate verification conditions
        vc = self.generate_vc(program, pre, post)
        
        # Discharge with SMT solver
        return self.solver.check(vc)
    
    def rule_while(self, invariant: Formula, condition: Formula, 
                   body: Statement, pre: Formula, post: Formula) -> VC:
        """While rule: {I ∧ B} body {I} ; {I ∧ ¬B} ⇒ {post}"""
        vc1 = VC(pre, f"({invariant} ∧ {condition})")
        vc2 = VC(f"{{{invariant} ∧ {condition}}} {body} {{{invariant}}}")
        vc3 = VC(f"({invariant} ∧ ¬{condition}) ⇒ {post}")
        return [vc1, vc2, vc3]

class SeparationLogicVerifier:
    def __init__(self):
        self.solver = SMTLib2Solver()
    
    def verify_memory_safety(self, program: Program) -> MemorySafetyResult:
        """Verify memory safety using separation logic"""
        # Generate verification conditions with separation logic
        vcs = self.generate_sl_vcs(program)
        
        results = []
        for vc in vcs:
            result = self.solver.check(vc)
            if result == sat:
                return MemorySafetyResult(safe=False, counterexample=self.solver.model())
        
        return MemorySafetyResult(safe=True)
    
    def frame_rule(self, pre: Formula, post: Formula, frame: Formula) -> VC:
        """Frame rule: {P} C {Q} ⇒ {P * R} C {Q * R}"""
        # Frame rule for separation logic
        return VC(pre * frame, post * frame)
```

### Refinement Types / Liquid Types
```python
# Liquid Haskell style refinement types (conceptual)

# @type inc :: x:Int -> {v:Int | v = x + 1}
def inc(x: int) -> int:
    return x + 1

# @type safeDiv :: x:Int -> y:{v:Int | v != 0} -> {v:Int | v = x / y}
def safe_div(x: int, y: int) -> int:
    if y == 0:
        raise ValueError("Division by zero")
    return x // y

# @type sort :: xs:[Int] -> {v:[Int] | sorted v ∧ len v = len xs}
def sort(xs: list[int]) -> list[int]:
    return sorted(xs)

# Verification with LiquidHaskell-style types
# {v:Int | v >= 0} -> {v:Int | v >= 0}
def sqrt(n: int) -> int:
    if n < 0:
        raise ValueError
    return int(math.sqrt(n))
```

---

## Runtime Verification

### Monitoring
```python
class RuntimeMonitor:
    def __init__(self):
        self.monitors: dict[str, Monitor] = {}
    
    def add_monitor(self, name: str, spec: LTLFormula):
        self.monitors[name] = LTLMonitor(spec)
    
    def monitor(self, event: Event):
        for monitor in self.monitors.values():
            monitor.process(event)
    
    def check_violations(self) -> list[Violation]:
        violations = []
        for name, monitor in self.monitors.items():
            if monitor.violated():
                violations.append(Violation(
                    property=monitor.formula,
                    trace=monitor.get_violating_trace(),
                    timestamp=datetime.utcnow()
                ))
        return violations

class LTLMonitor:
    def __init__(self, formula: LTLFormula):
        self.formula = formula
        self.automaton = self.formula_to_automaton(formula)
        self.current_state = self.automaton.initial_state
        self.trace = []
    
    def process(self, event: Event):
        self.trace.append(event)
        self.current_state = self.automaton.transition(self.current_state, event)
    
    def violated(self) -> bool:
        return not self.automaton.is_accepting(self.current_state)
    
    def get_violating_trace(self) -> list[Event]:
        return self.trace

class StatisticalMonitor:
    def __init__(self, window_size: int = 1000):
        self.window_size = window_size
        self.windows: dict[str, SlidingWindow] = {}
    
    def record(self, metric: str, value: float):
        if metric not in self.windows:
            self.windows[metric] = SlidingWindow(self.window_size)
        self.windows[metric].add(value)
    
    def check_thresholds(self, thresholds: dict[str, Threshold]) -> list[Alert]:
        alerts = []
        for metric, window in self.windows.items():
            if metric in thresholds:
                threshold = thresholds[metric]
                value = window.get_statistic(threshold.statistic)
                if threshold.violated(value):
                    yield Alert(metric=metric, value=value, threshold=threshold)
```

### Runtime Enforcement
```python
class RuntimeEnforcer:
    def __init__(self, policy: Policy):
        self.policy = policy
        self.state = EnforcementState()
    
    def enforce(self, action: Action) -> EnforcementResult:
        # Check if action violates policy
        if self.policy.allows(self.state, action):
            self.state.update(action)
            return EnforcementResult(allowed=True)
        
        # Find alternative
        alternative = self.find_alternative(action)
        if alternative:
            return EnforcementResult(allowed=True, modified_action=alternative)
        
        return EnforcementResult(allowed=False, reason="Policy violation")
    
    def find_alternative(self, action: Action) -> Action | None:
        # Find closest safe action
        candidates = self.generate_alternatives(action)
        for alt in candidates:
            if self.policy.allows(self.state, alt):
                return alt
        return None

class Shield:
    """Runtime shield for safety-critical systems"""
    def __init__(self, safety_spec: SafetySpec):
        self.spec = safety_spec
        self.shield_automaton = self.build_shield(safety_spec)
    
    def shield(self, action: Action) -> Action:
        # Check if action is safe
        if self.shield_automaton.is_safe(action):
            return action
        
        # Find safe alternative
        safe_action = self.shield_automaton.find_safe(action)
        if safe_action:
            return safe_action
        
        # Emergency action
        return self.spec.emergency_action
```

---

## Neural Network Verification

### Robustness Verification
```python
class NeuralNetworkVerifier:
    def __init__(self):
        self.abstractor = NetworkAbstractor()
        self.solver = Z3Solver()
        self.refiner = CounterexampleGuidedRefiner()
    
    async def verify_robustness(self, network: nn.Module, 
                                 input_bounds: Bounds,
                                 property: Property) -> VerificationResult:
        # 1. Abstract network to linear constraints
        constraints = self.abstractor.abstract(network)
        
        # 2. Add input bounds
        constraints.add_bounds(input_bounds)
        
        # 3. Add property
        constraints.add_property(property)
        
        # 4. Solve
        result = await self.solver.solve(constraints)
        
        if result == unsat:
            return VerificationResult(verified=True)
        elif result == sat:
            return VerificationResult(
                verified=False, 
                counterexample=self.extract_counterexample()
            )
        else:
            # Unknown - refine abstraction
            return await self.refine_and_reverify(network, input_bounds, property)
    
    async def verify_lipschitz(self, network: nn.Module, 
                                epsilon: float) -> LipschitzResult:
        """Compute Lipschitz constant"""
        # Use power iteration or SVD
        lipschitz = await self.compute_lipschitz(network)
        return LipschitzResult(
            constant=lipschitz,
            robust=lipschitz <= 1/epsilon
        )
```

### Abstract Interpretation for Neural Networks
```python
class NetworkAbstractor:
    def __init__(self):
        self.abstract_domains = {
            'interval': IntervalDomain(),
            'zonotope': ZonotopeDomain(),
            'polyhedron': PolyhedronDomain()
        }
    
    def abstract(self, network: nn.Module, domain: str = 'zonotope') -> Constraints:
        domain = self.abstract_domains[domain]
        constraints = Constraints()
        
        # Abstract each layer
        for layer in network.layers:
            if isinstance(layer, nn.Linear):
                constraints.add(self.abstract_linear(layer, domain))
            elif isinstance(layer, nn.ReLU):
                constraints.add(self.abstract_relu(layer, domain))
            elif isinstance(layer, nn.Conv2d):
                constraints.add(self.abstract_conv(layer, domain))
        
        return constraints
    
    def abstract_relu(self, layer: nn.ReLU, domain: AbstractDomain) -> Constraints:
        # Relu: y = max(0, x)
        # Abstract using interval/zonotope
        return domain.relu_constraint()
    
    def abstract_linear(self, layer: nn.Linear, domain: AbstractDomain) -> Constraints:
        # y = Wx + b
        return domain.linear_constraint(layer.weight, layer.bias)

class ZonotopeDomain:
    def __init__(self):
        self.generators = {}
    
    def relu_constraint(self) -> Constraints:
        # Zonotope ReLU: approximate with linear constraints
        return Constraints(type='relu_zonotope')
    
    def linear_constraint(self, weight: Tensor, bias: Tensor) -> Constraints:
        # Affine transformation of zonotope
        return Constraints(type='linear', weight=weight, bias=bias)
```

### Verification Tools Integration
```python
class VerificationTools:
    @staticmethod
    def alpha_beta_crown(network: nn.Module, spec: VerificationSpec) -> VerificationResult:
        """alpha-beta-CROWN: Fast verified robustness"""
        # Use alpha-beta-CROWN for fast verified robustness
        pass
    
    @staticmethod
    def auto_lirpa(network: nn.Module, spec: VerificationSpec) -> VerificationResult:
        """auto-LiRPA: Automatic LiRPA"""
        pass
    
    @staticmethod
    def nnenum(network: nn.Module, spec: VerificationSpec) -> VerificationResult:
        """NNENUM: Complete verification via enumeration"""
        pass
    
    @staticmethod
    def verinet(network: nn.Module, spec: VerificationSpec) -> VerificationResult:
        """VeriNet: Interval-based verification"""
        pass

class VerificationPipeline:
    def __init__(self):
        self.tools = {
            'alpha_beta_crown': AlphaBetaCROWN(),
            'auto_lirpa': AutoLiRPA(),
            'nnenum': NNEnum(),
            'verinet': VeriNet(),
            'marabou': Marabou(),
            'neurify': Neurify()
        }
    
    async def verify(self, network: nn.Module, spec: VerificationSpec) -> VerificationReport:
        results = {}
        for name, tool in self.tools.items():
            try:
                result = await tool.verify(network, spec)
                results[name] = result
            except Exception as e:
                results[name] = VerificationResult(error=str(e))
        
        return VerificationReport(results=results, consensus=self.consensus(results))
```

---

## Compositional Verification

### Assume-Guarantee Reasoning
```python
class AssumeGuaranteeVerifier:
    def __init__(self):
        self.solver = SMTLib2Solver()
    
    async def verify_composition(self, components: list[Component], 
                                  spec: SystemSpec) -> CompositionResult:
        """Verify composition using assume-guarantee reasoning"""
        # 1. Generate assume-guarantee contracts for each component
        contracts = await self.generate_contracts(components)
        
        # 2. Check compatibility
        compatibility = self.check_compatibility(contracts)
        if not compatibility.compatible:
            return CompositionResult(compatible=False, conflict=compatibility.conflict)
        
        # 3. Verify each component against its contract
        for component, contract in zip(components, contracts):
            result = await self.verify_component(component, contract)
            if not result.verified:
                return CompositionResult(
                    compatible=False, 
                    failing_component=component.name,
                    reason=result.counterexample
                )
        
        # 4. Compose guarantees
        system_guarantee = self.compose_guarantees(contracts)
        
        # 5. Check system spec
        if system_guarantee.implies(spec):
            return CompositionResult(verified=True)
        else:
            return CompositionResult(verified=False, missing=spec.diff(system_guarantee))
```

### Contract-Based Design
```python
@dataclass
class Contract:
    assumptions: Formula  # What component assumes
    guarantees: Formula   # What component guarantees
    inputs: set[str]
    outputs: set[str]

class ContractBasedVerifier:
    def __init__(self):
        self.solver = Z3Solver()
    
    def verify_contract(self, component: Component, contract: Contract) -> VerificationResult:
        # Check: assumptions -> (component -> guarantees)
        formula = Implies(
            And(contract.assumptions, component.specification()),
            contract.guarantees
        )
        
        result = self.solver.check(Not(formula))
        return VerificationResult(
            verified=(result == unsat),
            counterexample=self.solver.model() if result == sat else None
        )
    
    def compose_contracts(self, contracts: list[Contract]) -> Contract:
        """Compose contracts: assume conjunction, guarantee conjunction"""
        all_assumptions = And(*[c.assumptions for c in contracts])
        all_guarantees = And(*[c.guarantees for c in contracts])
        
        return Contract(
            assumptions=all_assumptions,
            guarantees=all_guarantees,
            inputs=set().union(*[c.inputs for c in contracts]),
            outputs=set().union(*[c.outputs for c in contracts])
        )
```

---

## Verification for AI Systems

### Verification of RL Policies
```python
class RLPolicyVerifier:
    def __init__(self):
        self.verifier = NeuralNetworkVerifier()
        self.mdp_analyzer = MDPAnalyzer()
    
    async def verify_policy(self, policy: Policy, mdp: MDP, 
                           spec: SafetySpec) -> VerificationResult:
        # 1. Extract policy as neural network
        policy_net = self.extract_network(policy)
        
        # 2. Verify robustness
        robust = await self.verify_robustness(policy_net, spec)
        
        # 2. Check value function bounds
        bounds = await self.verify_value_bounds(policy, mdp)
        
        # 3. Check policy constraints
        constraints = await self.verify_constraints(policy, mdp)
        
        return VerificationResult(
            robust=robust,
            bounds=bounds,
            constraints=constraints,
            verified=all([robust.verified, bounds.satisfied, constraints.satisfied])
        )
    
    async def verify_reward_alignment(self, policy: Policy, 
                                       reward_model: RewardModel) -> AlignmentResult:
        """Check if policy optimizes intended reward"""
        # Sample trajectories
        trajectories = self.sample_trajectories(policy, n=1000)
        
        # Compute true reward vs proxy reward
        true_rewards = [self.true_reward(t) for t in trajectories]
        proxy_rewards = [reward_model.score(t) for t in trajectories]
        
        correlation = np.corrcoef(true_rewards, proxy_rewards)[0,1]
        
        return AlignmentResult(
            correlation=correlation,
            aligned=correlation > 0.9,
            reward_hacking_detected=correlation < 0.5
        )
```

### Verification of LLM Outputs
```python
class LLMOutputVerifier:
    def __init__(self):
        self.fact_checker = FactChecker()
        self.logic_verifier = LogicVerifier()
        self.consistency_checker = ConsistencyChecker()
    
    async def verify_output(self, prompt: str, output: str, 
                           spec: VerificationSpec) -> VerificationResult:
        results = await asyncio.gather(
            self.fact_checker.check(output, spec.facts),
            self.logic_verifier.verify(output, spec.logic_rules),
            self.consistency_checker.check(output, spec.context),
            self.check_hallucination(output, spec.known_facts)
        )
        
        return VerificationResult(
            factually_correct=results[0].passed,
            logically_valid=results[1].passed,
            consistent=results[2].passed,
            no_hallucination=results[3].passed,
            overall=all(r.passed for r in results)
        )

class FactChecker:
    async def check(self, text: str, facts: KnowledgeBase) -> FactCheckResult:
        claims = self.extract_claims(text)
        results = await asyncio.gather(*[
            self.verify_claim(claim, facts) for claim in claims
        ])
        return FactCheckResult(
            verified=all(r.verified for r in results),
            claims=results
        )
```

---

## Related Notes

- [[Frontiers/Self-Improving-Agents.md]] — Verification for self-improvement
- [[Frontiers/Lifelong-Learning.md]] — Verified lifelong learning
- [[Frontiers/Neurosymbolic-Integration.md]] — Neurosymbolic verification
- [[Frontiers/Agent-Computer-Interface.md]] — ACI verification
- [[Frontiers/Agent-Societies.md]] — Multi-agent verification
- [[Frontiers/Research-Directions.md]] — Verification research
- [[ModelArchitectures/Reasoning-Models.md]] — Reasoning model verification
- [[ModelArchitectures/Mixture-of-Experts.md]] — MoE verification
- [[Architecture/Cognitive-Architectures.md]] — Cognitive architecture verification
- [[Architecture/Domain-Driven-Design.md]] — DDD verification
- [[Patterns/Design-Patterns.md]] — Verified patterns
- [[Patterns/Resilience-Patterns.md]] — Verified resilience
- [[Evaluation/Formal-Verification.md]] — Verification evaluation
- [[Evaluation/Red-Teaming.md]] — Red teaming for verification
- [[Production/Security.md]] — Security verification
- [[Production/Reliability.md]] — Reliability verification
- [[Security/Secure-Coding.md]] — Secure coding verification
- [[Security/Supply-Chain-Security.md]] — Supply chain verification

---

*Sources: "Principles of Model Checking" (Baier & Katoen), "Model Checking" (Clarke et al.), "Handbook of Model Checking" (Clarke et al.), "Handbook of Automated Reasoning" (Robinson & Voronkov), "Software Verification" surveys, "Deductive Software Verification" (Leino), "Dafny" (Leino), "F*" (Swamy et al.), "VeriFast" (Jacobs et al.), "VCC" (Cohen et al.), "Frama-C" (Cuoq et al.), "SPARK" (Barnes et al.), "Why3" (Filliâtre & Paskevich), "Coq" (Bertot & Castéran), "Lean" (de Moura et al.), "Isabelle/HOL" (Nipkow et al.), "Isabelle/HOL" (Nipkow et al.), "Agda" (Norell), "Idris" (Brady), "TLA+" (Lamport), "PlusCal" (Lamport), "Alloy" (Jackson), "Z3" (de Moura & Bjørner), "CVC5" (Barbosa et al.), "SMT-LIB" (Barrett et al.), "SMT" (de Moura & Bjørner), "CBMC" (Kroening & Tautschnig), "ESL" (Erich), "CBMC" (Kroening & Tautschnig), "ESL" (Erich), "K-Induction" (Sheeran et al.), "IC3/PDR" (Bradley), "IC3" (Bradley), "Property Directed Reachability" (Bradley), "Probabilistic Model Checking" (Kwiatkowska et al.), "PRISM" (Kwiatkowska et al.), "Storm" (Dehnert et al.), "Statistical Model Checking" (Younes et al.), "Neural Network Verification" (Katz et al.), "Reluplex" (Katz et al.), "Alpha-Beta-CROWN" (Wang et al.), "auto-LiRPA" (Xu et al.), "NNENUM" (Bak et al.), "VeriNet" (Henriksen & Lomuscio), "Neurify" (Wang et al.), "Marabou" (Katz et al.), "VeriNet" (Henriksen & Lomuscio), "NNENUM" (Bak et al.), "Alpha-Beta-CROWN" (Wang et al.), "VeriNet" (Henriksen & Lomuscio), "NNENUM" (Bak et al.), "Alpha-Beta-CROWN" (Wang et al.), "auto-LiRPA" (Xu et al.), "NNENUM" (Bak et al.), "VeriNet" (Henriksen & Lomuscio), "Marabou" (Katz et al.), "Neurify" (Wang et al.).*