Clawq follows a Coq-first architecture: core properties are machine-checked in Coq, extracted to OCaml, and wrapped by a runtime that provides I/O, networking, and channel integrations.

Build Pipeline

The extracted OCaml is tracked in git so the project builds without Coq installed. Run make extract to regenerate from Coq sources, and make extract-check to verify no drift.

Coq Theories

File	Role
Interfaces.v	7 record-based interface definitions: Provider, Channel, Tool, Memory, RuntimeAdapter, Tunnel, Security
Config.v	Configuration records (GatewayConfig, MemoryConfig, SecurityConfig, ClawqConfig) with defaults and validation
Cli.v	Command ADT, parse_command, dispatch, and usage string for 18 commands
Extract.v	Extraction directives: type mappings and function list

Extracted OCaml

File	Role
clawq_core.ml	Auto-generated OCaml from Coq. Contains command parsing, dispatch, config validation.
clawq_core.mli	Auto-generated interface. Both files are tracked in git.

Runtime Module Map

Module	Role
main.ml	CLI entry point and top-level Cmdliner command registration
main_cmd_common.ml	Shared Cmdliner helpers for command modules
main_audit_cmds.ml	Cmdliner definitions for clawq audit subcommands
main_background_cmds.ml	Cmdliner definitions for clawq background and clawq subagents subcommands
main_models_cmds.ml	Cmdliner definitions for clawq models subcommands
main_plan_cmds.ml	Cmdliner definitions for clawq plan subcommands
main_session_cmds.ml	Cmdliner definitions for clawq session subcommands
command_bridge.ml	Bridges CLI to extracted Coq dispatch; handles runtime-only commands
command_bridge_cron.ml	Runtime command bridge implementation for clawq cron
command_bridge_room_ledger.ml	Runtime command bridge implementation for clawq rooms ledger
runtime_config_defaults.ml	Default runtime configuration values for all subsystems
runtime_config.ml	Configuration loading, validation, and defaults for all subsystems
config_loader.ml	File-based config loading: reads JSON, merges with env vars
session.ml	Public facade over split session lifecycle modules
session_core.ml	Session manager state, queueing, locks, notifier registration, context, and persistence helpers
session_management.ml	Session config/model management, reset, compaction, and debug dumps
session_postmortem.ml	Session stuck-pattern postmortem circuit breaker and launcher hook
session_postmortem_launcher.ml	Postmortem agent launch implementation installed by the turn loop
session_turn.ml	Shared buffered/streaming session turn orchestration, queue draining, skill injection, and room-policy snapshots
provider.ml	LLM provider abstraction: streaming text/thinking/tool events, model selection
memory.ml	Key-value memory backend: SQLite-backed store/recall/forget with namespace support and per-session archive files for forgotten memories
vector.ml	Local vector index: embedding storage, cosine similarity, hybrid FTS+vector merge
tool.ml	Tool type definitions and invocation framework with risk-level enforcement
tool_registry.ml	Dynamic tool registration: register, lookup, list by name or category
tools_builtin.ml	Built-in tool implementations: file I/O, shell exec, web fetch, search
agent.ml	Thin public buffered/streaming turn entry points
agent_turn_core.ml	Shared agent turn loop, provider-call adapters, streaming emission, and cost tracking
agent_compact_support.ml	Agent state, exceptions, token estimates, and compaction preservation helpers
agent_0_compact.ml	Agent history compaction, memory flush, and compact-plan execution
agent_memory_context.ml	Agent scoped and legacy memory-context injection
agent_2_tools.ml	Agent tool-call validation, execution, and tool-result history integration
agent_profile.ml	Agent room-profile and scoped-memory helper logic
agent_provider_ledger.ml	Agent provider request/error/response room-ledger events
agent_room_budget.ml	Agent room-budget guard and reservation helpers
agent_turn_setup.ml	Agent construction and turn-history preparation
mcp_server.ml	MCP server: exposes tools over JSON-RPC with configurable filtering
skills.ml	Skill loader: discovers and loads skill definitions from the filesystem
http_server.ml	HTTP server: gateway, SSE chat streaming, pairing, slash-command metadata, and web UI endpoints
ui_server.ml	Web UI asset manager: embedded bundle extraction, dev-mode disk serving, and version hashing
http_client.ml	HTTP client: shared Cohttp-lwt client for provider and API calls
telegram.ml	Telegram channel update handler and turn dispatch
telegram_attachments.ml	Telegram inbound voice, image, and document attachment handling
telegram_rich_notifier.ml	Telegram rich message delivery for buttons, polls, and file attachments
discord.ml	Discord channel: WS gateway mode, REST rate limit buckets, reconnect loop
discord_gateway.ml	Discord gateway protocol state machine (Hello, Identify, Resume, Heartbeat, Dispatch)
slack_api.ml	Slack Events API parsing, HMAC verification, and Web API helpers
slack.ml	Slack event handler
slack_socket.ml	Slack Socket Mode: WSS-based event receiving via app_token
teams_webhook.ml	Microsoft Teams webhook orchestration and turn dispatch
teams_attachments.ml	Microsoft Teams inbound audio and file attachment handling
teams_command_cards.ml	Microsoft Teams Adaptive Card slash-command rendering
teams_command_text.ml	Microsoft Teams text-only slash-command reply rendering
teams_debug_dump.ml	Microsoft Teams session debug dump file-consent/download delivery
teams_rich_notifier.ml	Microsoft Teams rich message delivery for Adaptive Cards
ws_client.ml	Shared TLS WebSocket client (httpun-ws, gluten, tls-lwt, ca-certs)
daemon_config_watch.ml	Daemon config-file watcher and live reload loop
daemon_channels.ml	Non-Telegram daemon channel startup fanout
daemon_startup.ml	Daemon database/schema initialization, room-profile reconciliation, and tool/skill registry bootstrap
daemon_heartbeat.ml	Periodic HEARTBEAT.md processing for opted-in channel sessions
daemon_background_loops.ml	Auxiliary model-discovery, search-health, quota-refresh, and subagent-status daemon loops
daemon_runtime_loops.ml	Database-backed scheduler, repo-fetch, maintenance, and background-task daemon loops
daemon.ml	Supervisor: gateway + Telegram lifecycle, signal handling, SIGHUP reload, and EC process lifecycle
provider_quota_state.ml	Provider quota state types, cache, persistence, history, and status formatting
provider_quota.ml	Provider quota fetchers and provider-specific usage parsers
error_watcher.ml	Error correction shared types, helpers, and EC process lifecycle management
ec_process.ml	EC process entry point: daemon log/session/background-task error scanning, correlation
ec_diagnosis.ml	Multi-model diagnosis pipeline: parallel LLM queries, voting, planning, fix spawning
service.ml	Service orchestrator: starts/stops subsystems (server, tunnel, scheduler)
scheduler_schedule.ml	Schedule parsing and cron/interval run matching helpers
scheduler_output_guard.ml	Cron run output hashing and consecutive-identical-output auto-disable guard
scheduler_routine_target.ml	Routine target display formatting shared by scheduler job and run history views
scheduler.ml	Scheduled tasks: cron-like recurring job execution
audit.ml	Audit logging: append-only log of tool invocations and security events
secret_store.ml	Secret encryption at rest: AES-256-GCM, PBKDF2 key derivation, $ENC: prefix format
sql_util.ml	Shared SQLite plumbing: exec_exn/exec_with_params, bind_params, column accessors, and a query_rows combinator used across store modules
time_util.ml	Shared ISO-8601/RFC-3339 timestamp formatting (iso8601_utc, iso8601_utc_micros/_millis, sql_datetime_utc, date_utc, iso8601_local), consolidating the hand-rolled Printf.sprintf "%04d-%02d-%02dT…" variants
migrate.ml	Database migrations: versioned schema upgrades for SQLite stores
resilience.ml	Reliability policies: timeout, retry (exponential backoff), fallback
runtime_native.ml	Native runtime adapter: wraps daemon/service for start/stop/status/health
runtime_docker.ml	Docker runtime adapter: manages clawq in containers via docker CLI
tunnel_manager.ml	Unified tunnel lifecycle manager: apply/stop/restart, live reconfiguration, daemon hooks
tunnel_cloudflare.ml	Cloudflare tunnel: manages cloudflared process, extracts assigned URL
rate_limiter.ml	Token bucket rate limiter (IP, session, chat)
landlock.ml	Landlock OS sandboxing (C FFI)
bg_shell.ml	Background shell job registry and lifecycle (created when shell_exec is interrupted)
tools_bg_shell.ml	Background shell tools: bg_shell_status, bg_shell_wait, bg_shell_result
slash_commands.ml	Slash command parsing, dispatch, and per-connector rendering
format_adapter.ml	Connector-safe formatting dispatch (markdown tables, code blocks, HTML)
table_format.ml	Markdown and plaintext table rendering
setup_common.ml	Shared TUI helpers for setup wizards (prompts, ANSI, box drawing)
config_wizard_model.ml	Config wizard state machine types
config_wizard_tui.ml	Config wizard terminal I/O loop
config_wizard_update.ml	Config wizard state transitions
model_discovery.ml	API-based model catalog discovery (12h TTL cache)
request_stats.ml	Per-turn token usage and cost persistence
cost_tracker.ml	Model pricing table and cost calculation
runner_framework.ml	Common runner session tracking framework (session ID strategies, command generation)
background_task_spawn.ml	Background task process spawning, worktrees, scheduling, and restart/readoption
background_task_room.ml	Room background task launch and GitHub review launch orchestration
background_task_workflow.ml	Workflow-triggered background task launch orchestration
structured_pipeline_types.ml	Shared structured-pipeline definition, step, run, and result types
structured_pipeline_builtins.ml	Built-in structured pipeline catalogue definitions
structured_pipeline.ml	Structured pipeline parsing, discovery, persistence, and CLI formatting facade
structured_pipeline_run.ml	Structured pipeline execution engine
background_task.ml	Background task public facade over split lifecycle modules
pmodel.ml	Canonical provider:model format parsing (strict + flexible), deprecation warnings
stt.ml	Speech-to-text: audio transcription via Whisper-compatible API
voice_transcription.ml	Shared voice message handling: audio detection, music heuristic, validation, transcribe-with-progress

Dune Libraries

Library	Key Modules	Dependencies
clawq_extracted	clawq_core	None (unwrapped, -w -39 for extraction artifacts)
clawq_runtime_core	Config, agent, session, provider, memory, tools, audit, security, rate limiter, scheduler	yojson, sqlite3, lwt, cohttp-lwt-unix, mirage-crypto, digestif, clawq_extracted
clawq_runtime_integrations	HTTP server, telegram, discord, slack, daemon, MCP, WS client, tunnels, runtimes	clawq_runtime_core + httpun-ws-lwt-unix, gluten-lwt-unix, ca-certs
clawq (executable)	main_cmd_common, main_audit_cmds, main_background_cmds, main_models_cmds, main_plan_cmds, main_session_cmds, main	clawq_runtime_core, clawq_runtime_integrations, cmdliner

Both libraries use (wrapped false) so modules are accessible directly (e.g., Clawq_core.dispatch rather than Clawq_extracted.Clawq_core.dispatch).

Interface Inventory

From Interfaces.v, these 7 records define the contract surface:

Interface	Fields	Purpose
Provider	name, complete, health	LLM provider abstraction
Channel	name, start, stop, send	Communication channel (web, telegram, etc.)
Tool	name, invoke, risk_level	Agent tool with risk classification
Memory	store, recall, forget	Key-value memory backend
RuntimeAdapter	name, start, stop	Runtime lifecycle management
Tunnel	name, start, status	Network tunnel (e.g., Cloudflare)
Security	workspace_only, audit_enabled, encrypt_secrets	Security policy flags

Dependency Direction

Runtime Split

The runtime is split into core and integrations to support a minimal build (clawq-min) that excludes network dependencies:

1. Optional integrations stay out of clawq_runtime_core
2. Network/server features belong in clawq_runtime_integrations
3. Integration-only commands return “disabled in minimal build” messages in command_bridge_min.ml
4. New dependencies are evaluated for core vs integration placement before linking

Web UI Surface

The browser chat UI is embedded into the daemon and served from the gateway root.

• GET / serves index.html plus versioned chat.js and chat.css assets.
• POST /chat/stream emits SSE events for reply deltas, thinking deltas, tool starts, streamed tool output, tool results, and final completion.
• GET /commands exposes slash-command metadata for autocomplete.
• GET /ui-version returns the current UI bundle version so the client can offer a reload banner.
• POST /pair exchanges a 6-digit OTP for a bearer token when gateway pairing is enabled.

In normal mode the daemon extracts embedded assets into ~/.clawq/ui/ when the bundle hash changes. If ~/.clawq/ui/DEV exists, the daemon switches to disk-backed dev mode and recomputes the UI version from local files instead of overwriting them.