[ARCH] Truth Engine v0 — Z3 SMT solver as Hermes tool #34

New Issue

perplexity · 2026-03-27T22:48:31Z

perplexity commented

2026-03-27 22:48:31 +00:00

Source

"Hermes Agent: The Definitive Neuro-Symbolic Blueprint for Mac M3 Max", Sections 3-4.

What

Implement the first "Mechanical Brain" integration: Z3 as a callable tool inside Hermes.

Phase 1: Z3 tool registration

Install z3-solver (pip, Apple Silicon native)
Register a z3_verify tool in Hermes that accepts SMT-LIB v2 input and returns SAT/UNSAT/model
Add to config.yaml as a local tool with no cloud dependency

Phase 2: Logic Router (simple)

Add keyword-based routing in the system prompt: if the query involves constraints, scheduling, or logical verification → emit SMT-LIB → call Z3
Start with hardcoded routing rules before investing in a learned router

Phase 3: Proof-of-Thought prompting

System prompt instructs the LLM to "think in formal logic" for constraint problems
LLM generates SMT-LIB, Z3 verifies, LLM explains the result in natural language

M3 Max resource notes (from blueprint)

Z3 runs on P-cores (CPU), LLM on GPU — no resource contention on UMA
Target: sub-100ms for simple constraint checks via direct Python bindings (no HTTP overhead)

Why

This is the foundational piece of the neuro-symbolic architecture. Z3 gives Timmy deterministic truth-checking for logical claims, constraint satisfaction, and eventually verified code generation. Directly supports the "LLMs are pattern matchers, not reasoners" thesis from the research.

Acceptance

hermes_local("Is it possible to schedule 3 meetings in 2 rooms with no conflicts given these constraints: ...") routes to Z3 and returns a verified answer
Health check reports Z3 availability
No cloud dependency

Issue #22 (sovereignty transition) — Z3 is local-first by nature
Blueprint Section 4.1 contains reference implementation code

## Source "Hermes Agent: The Definitive Neuro-Symbolic Blueprint for Mac M3 Max", Sections 3-4. ## What Implement the first "Mechanical Brain" integration: Z3 as a callable tool inside Hermes. ### Phase 1: Z3 tool registration - Install `z3-solver` (pip, Apple Silicon native) - Register a `z3_verify` tool in Hermes that accepts SMT-LIB v2 input and returns SAT/UNSAT/model - Add to `config.yaml` as a local tool with no cloud dependency ### Phase 2: Logic Router (simple) - Add keyword-based routing in the system prompt: if the query involves constraints, scheduling, or logical verification → emit SMT-LIB → call Z3 - Start with hardcoded routing rules before investing in a learned router ### Phase 3: Proof-of-Thought prompting - System prompt instructs the LLM to "think in formal logic" for constraint problems - LLM generates SMT-LIB, Z3 verifies, LLM explains the result in natural language ## M3 Max resource notes (from blueprint) - Z3 runs on P-cores (CPU), LLM on GPU — no resource contention on UMA - Target: sub-100ms for simple constraint checks via direct Python bindings (no HTTP overhead) ## Why This is the foundational piece of the neuro-symbolic architecture. Z3 gives Timmy deterministic truth-checking for logical claims, constraint satisfaction, and eventually verified code generation. Directly supports the "LLMs are pattern matchers, not reasoners" thesis from the research. ## Acceptance - `hermes_local("Is it possible to schedule 3 meetings in 2 rooms with no conflicts given these constraints: ...")` routes to Z3 and returns a verified answer - Health check reports Z3 availability - No cloud dependency ## Related - Issue #22 (sovereignty transition) — Z3 is local-first by nature - Blueprint Section 4.1 contains reference implementation code

Timmy was assigned by Rockachopa

2026-03-28 03:52:19 +00:00

Timmy referenced this issue

2026-03-28 04:45:17 +00:00

[ARCH] Truth Engine v0 — Z3 SMT solver as Hermes tool #35

Timmy commented

2026-03-28 04:53:02 +00:00

Closing during the 2026-03-28 backlog burn-down.

Reason: this issue is being retired as part of a backlog reset toward the current final vision: Heartbeat, Harness, and Portal. If the work still matters after reset, it should return as a narrower, proof-oriented next-step issue rather than stay open as a broad legacy frontier.

Closing during the 2026-03-28 backlog burn-down. Reason: this issue is being retired as part of a backlog reset toward the current final vision: Heartbeat, Harness, and Portal. If the work still matters after reset, it should return as a narrower, proof-oriented next-step issue rather than stay open as a broad legacy frontier.

Timmy closed this issue

2026-03-28 04:53:03 +00:00

Sign in to join this conversation.

2 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: Timmy_Foundation/timmy-config#34