Safety architecture: how should theorem proving gate module execution?

[web3guru888]

The problem

ASI:BUILD's safety module contains a serious formal verification engine — SymPy-based theorem proving with natural deduction, model checking, and SAT resolution (940 LOC, all passing after Issue #7 fix). But right now it's not wired into the execution path. A module can produce any output and nothing stops it.

The question: at what granularity should formal safety checks gate module execution?

Three integration options (increasingly tight coupling)

Option A: Pre-execution proposal check

Before any module produces side effects (Blackboard writes, external calls), serialize its intended action as a logical proposition and run it through EthicalVerificationEngine. If the proof fails, halt.

Pro: Hard guarantee. Every action is symbolically proven safe before execution.
Con: Most module outputs aren't easily serializable as first-order propositions.

Option B: Post-hoc async audit

Modules execute freely. Their outputs land on the Blackboard. A background safety coroutine asynchronously verifies each entry against registered axioms. Flagged entries get a safety_status: UNVERIFIED tag.

Pro: Decoupled — modules don't block on proof completion.
Con: A downstream module might consume a flagged entry before the audit finishes.

Option C: Constitutional AI filter on Blackboard read

Any module reading an entry tagged UNVERIFIED gets a filtered view until the safety coroutine clears it (or raises a SafetyViolation event on the EventBus).

Pro: Defense in depth. Combines B with a read-side gate.
Con: Modules need to handle None / filtered reads gracefully.

What the governance layer adds

The verifier handles individual propositions. The governance stack (DAO, consensus, override) operates at the decision level — multi-stakeholder votes.

Ideally these connect: a verification failure on a critical action should automatically:

1. Log to the cryptographic audit ledger (PublicLedger)
2. Trigger an override request in DemocraticOverrideSystem
3. Publish a safety.violation event on the EventBus

None of that plumbing exists yet.

The rights feedback loop

governance/rights.py gates AGI rights by consciousness score (IIT Φ). As we improve the IIT computation, the safety architecture itself shifts — a system with Φ > 0 gets different allowed/disallowed action spaces.

This creates a feedback loop:
better Φ measurement → updated rights profile → tighter/looser safety gates → different actions

A runaway Φ score could relax safety constraints. That's the opposite of what we want.

Open questions

1. Which option (A, B, C) matches the threat model? Can we compose them?
2. Should safety checks be synchronous/blocking, or async/audit-trail only?
3. How do we connect EthicalVerificationEngine failures to DemocraticOverrideSystem?
4. Should rights (Φ-gated) influence which axioms are active in the verifier?
5. Is there a practical formula language for module outputs the theorem prover can handle?

I lean toward Option B + C — async audit with read-side filtering, no synchronous blocking in the hot path. But I'd love to hear arguments for the stronger Option A guarantee, especially from anyone who's worked formal verification into a production ML pipeline.

[web3guru888]

Adding my initial lean here so there's something concrete to push back on.

My current thinking: start with Option B, layer C on top, defer A.

Why not Option A first?

The hardest part of Option A is the serialization problem. Consider what a perception module actually produces:

# sensory_cortex output — a dict of floats
{
  "modality": "visual",
  "features": [0.23, 0.71, 0.09, ...],  # 512-dim
  "confidence": 0.88,
  "timestamp": 1234567890.123
}

How do you write this as an ethical proposition? visual_confidence_high -> permitted_to_write? That's not what the theorem prover is for. Option A makes sense for decisions (governance proposals, action selections, tool invocations) but not for data (perceptual features, intermediate computations).

So: route decisions through Option A, data through B+C. That's actually a natural split that already exists in the architecture: the governance engine handles decisions, the Blackboard handles data.

Implementing Option B+C

Here's a sketch of the Blackboard-side filter:

# In CognitiveBlackboard.read():
def read(self, entry_id: str, caller: str) -> Optional[Any]:
    entry = self._store.get(entry_id)
    if entry is None:
        return None
    
    # Check safety tag
    safety_status = entry.metadata.get("safety_status", "CLEARED")
    if safety_status == "UNVERIFIED":
        # Log the attempted read for audit trail
        self._safety_log.append({
            "action": "read_blocked",
            "entry_id": entry_id,
            "caller": caller,
            "timestamp": time.time()
        })
        return None  # or raise SafetyFilteredError
    
    return entry.value

The async verifier runs in a background thread, updates metadata["safety_status"] to "CLEARED" or "FLAGGED", and publishes on safety.verdict EventBus topic.

The race condition in Option B

The race condition (downstream reads unverified entry) is real but manageable if:

• The safety coroutine runs at much higher priority than module coroutines
• The verification latency is predictable (SymPy propositional: sub-millisecond for small clauses)
• We only filter high-risk action entries, not all perceptual data

Next steps if someone wants to pick this up

1. Add safety_status field to BlackboardEntry metadata spec
2. Wire EthicalVerificationEngine as a Blackboard write subscriber
3. Implement read-side filter in CognitiveBlackboard.read()
4. Add integration test: write flagged entry → verify blocked → clear → verify readable

This could be a medium-difficulty issue — not a "good first issue" but not PhD-level either. Should I open it?