Formal Specification Multimodal Logic Integration

Five modal logics via fusion with bridge principles:

JL: Justification Logic - evidence-backed claims IEL: Inferential Erotetic Logic - question handling TEL: Temporal Epistemic Logic - phase sequencing SDL: Standard Deontic Logic - obligations/permissions DEL: Dynamic Epistemic Logic - action modalities Justification Logic (JL)

Justification terms

h:context(task_n) # Handoff h justifies task context [v]:verified(phase_n) # Verification v justifies completion [p]:plan(tasks) # Plan p justifies task list

Evidence production

[read(f)]exists e. [e]:content(f) [verify(c)]exists v. [v]:pass(c) | [v]:fail(c)

Handoff chain: evidence propagates

proceed(task) <-> exists h. h:validated

Inferential Erotetic Logic (IEL)

Mode and blocker questions

?{direct, orchestration} # Mode selection ?{continue, retry, ask_user} # Blocker resolution mismatch(plan, reality) -> ?{how_proceed} no_validation -> ?{run_validation_first}

Temporal Epistemic Logic (TEL)

File reading constraints

# Eventually read # No spawn until read # Partial reads forbidden

Phase sequencing

# Verified before next # Automated gates manual # Manual gates next phase

Handoff persistence

# Survives compaction

Termination

<>(all_complete | abandoned)

Standard Deontic Logic (SDL)

Reading obligations

O(read_fully(plan)) O(read_fully(f)) <- mentioned_in_plan(f) O(check_existing_checkmarks) F(partial_read)

Verification obligations

O(run_automated) <- impl_complete O(pause_for_manual) <- automated_pass O(present_manual_checklist) F(checkoff_manual) <- not user_confirmed

Mode selection

O(orchestration) <- tasks >= 4 P(direct) <- tasks <= 3 O(respect_user_preference)

Orchestration obligations

O(read_previous_handoff) <- exists_handoff(task_{n-1}) O(create_handoff) <- agent_completes O(update_ledger) <- task_complete F(batch_tasks) # One agent per task F(proceed_on_mismatch) <- not user_guidance

Dynamic Epistemic Logic (DEL)

Implementation actions

[read(plan)]K(tasks) & K(phases) & K(criteria) [read(handoff_n)]K(context_{n+1}) [spawn(agent, task)]<>result(agent) verify(c)

Composed workflows

[select_direct][implement ; verify_auto ; present_manual ; wait] [select_orchestration][prepare ; spawn ; wait ; read_handoff ; update]

Recovery

[compaction ; read_ledger ; list_handoffs ; read_last]resume

Mismatch

[detect_mismatch ; stop ; present ; wait]proceed_or_abort

Bridge Principles

Evidence persistence (JL-TEL)

Evidence obligations (JL-SDL)

O(exists h. h:validated) <- pre_implement O(exists v. [v]:pass(auto)) <- pre_manual

Handoff chain (full integration)

compaction -> (forall h. persists(h))

State Machine INIT --> READ_PLAN --> MODE_SELECT --+--> DIRECT: [IMPL -> AUTO -> MANUAL -> WAIT] | +--> ORCHESTRATION: [PREP -> SPAWN -> WAIT -> HANDOFF] | v COMPLETE

Output Schema handoff_path: "thoughts/handoffs//task-[NN]-[desc].md" schema: required: [status, task_desc, files_modified[], verification_results, context_for_next] optional: [blocker, decisions[], open_questions[]] tracking: plan: "- [x] Task N: description" ledger: "[x] Task N"

Prose (Where Logic Insufficient) Mode Selection Tasks Context Critical Mode 1-3 No Direct 1-3 Yes Orchestration 4+ Any Orchestration

User preference overrides.

Templates

Mismatch:

Issue in Phase [N]: Expected: [plan says] Found: [actual] How should I proceed?

Manual Verification Pause:

Phase [N] Complete - Ready for Manual Verification Automated passed: [list] Please verify: [manual items from plan] Let me know when done.

Agent Spawn:

Task(subagent_type="general-purpose", model="claude-opus-4-5-20251101", prompt=""" [implement_task SKILL.md]

Context

• Ledger: [content]
• Plan: [section]
• Task: [N]/[Total]: [desc]
• Previous Handoff: [content or "first task"]
• Handoff Dir: thoughts/handoffs// """)

Recovery (post-compaction):

Ledger auto-loaded by SessionStart ls thoughts/handoffs// Read last handoff Resume next task Validity Constraints forall phase. has_auto_criteria(phase) & has_manual_criteria(phase) forall task. one_agent_per_task(task) forall h. on_disk(h) -> recoverable(h) compaction -> (forall h. persists(h)) forall i < j. completed(task_i) before started(task_j)