feat(crucible): add Z3 sidecar MCP verifier

- add crucible_mcp_server.py with Z3-backed proof tools
- ship scheduling, dependency ordering, and capacity templates
- log SAT/UNSAT proof trails to ~/.hermes/logs/crucible/
- wire crucible MCP server into config.yaml
- teach deploy.sh to ensure z3-solver is installed
- add verified-logic playbook and docs for first cut

docs/crucible-first-cut.md

@@ -0,0 +1,82 @@
+# Crucible First Cut
+
+This is the first narrow neuro-symbolic slice for Timmy.
+
+## Goal
+
+Prove constraint logic instead of bluffing through it.
+
+## Shape
+
+The Crucible is a sidecar MCP server that lives in `timmy-config` and deploys into `~/.hermes/bin/`.
+It is loaded by Hermes through native MCP discovery. No Hermes fork.
+
+## Templates shipped in v0
+
+### 1. schedule_tasks
+Use for:
+- deadline feasibility
+- task ordering with dependencies
+- small integer scheduling windows
+
+Inputs:
+- `tasks`: `[{name, duration}]`
+- `horizon`: integer window size
+- `dependencies`: `[{before, after, lag?}]`
+- `max_parallel_tasks`: integer worker count
+
+Outputs:
+- `status: sat|unsat|unknown`
+- witness schedule when SAT
+- proof log path
+
+### 2. order_dependencies
+Use for:
+- topological ordering
+- cycle detection
+- dependency consistency checks
+
+Inputs:
+- `entities`
+- `before`
+- optional `fixed_positions`
+
+Outputs:
+- valid ordering when SAT
+- contradiction when UNSAT
+- proof log path
+
+### 3. capacity_fit
+Use for:
+- resource budgeting
+- optional-vs-required work selection
+- capacity feasibility
+
+Inputs:
+- `items: [{name, amount, value?, required?}]`
+- `capacity`
+
+Outputs:
+- chosen feasible subset when SAT
+- contradiction when required load exceeds capacity
+- proof log path
+
+## Demo
+
+Run locally:
+
+```bash
+~/.hermes/hermes-agent/venv/bin/python ~/.hermes/bin/crucible_mcp_server.py selftest
+```
+
+This produces:
+- one UNSAT schedule proof
+- one SAT schedule proof
+- one SAT dependency ordering proof
+- one SAT capacity proof
+
+## Scope guardrails
+
+Do not force every answer through the Crucible.
+Use it when the task is genuinely constraint-shaped.
+If the problem does not fit one of the templates, say so plainly.