Files

Hermes 8b1b481828 Stages: rename titles, fix execution order, remove all numbered references

2026-06-04 20:04:34 +00:00

18 KiB

Raw Permalink Blame History

Architecture

The four subsystems, one address space.

Passepartout is one system built from four subsystems that share one evaluation semantics, one memory graph, and one proof chain:

Environment — the personal computing environment
Knowledge — the unified memex
Verification — the gate
Social Protocol — provable communication between instances

Each is described below.

The environment: one address space.

The environment eliminates the layered trust model of a conventional OS by eliminating the layers. Instead of an editor that sends keystrokes through a terminal emulator to a shell that forks processes that read files through a kernel VFS layer — each boundary a potential vulnerability — the environment runs everything in a single Lisp address space. (Lisp is a family of programming languages where code and data share the same representation. This property means the machine can verify what code does and modify itself without restarting. It is the foundation that makes the entire architecture possible.)

The editor is a Lisp function that manipulates text buffers in the evaluated memory graph. The shell is a Lisp read-eval-print loop that compiles to the same evaluator. The browser renders HTML through a Lisp-based rendering engine, not a separate process. The agent runtime invokes Lisp functions, not subprocesses. (The specific implementations that realize this today use Lish for the shell and editor, Nyxt for the browser, and SBCL as the host Lisp — but the architectural principle is uniform semantics in one address space, not these particular packages.)

There is no MMU boundary between components because there are no separate processes. There is no IPC because there is nothing to communicate between. Everything shares the same memory graph. Your editor buffer, your shell history, your agent's state, and your social protocol messages all live in the same evaluated object graph, protected by the same gate, verified by the same prover.

The knowledge subsystem: Org-mode as unified memex.

The knowledge subsystem is built on Org-mode — one format for human and machine, with sparse tree retrieval keeping context lean (2,000-4,000 tokens). The Org file IS the data, not a representation of it. See design-decisions.org for the full analysis.

Two indices over the Org prose:

A neural index using vector embeddings for semantic search — the gateway to the full richness of natural language.
A symbolic index storing formal assertions about what the prose says — predicates, relations, constraints — each grounded to a specific heading or block.

The prose is always ground truth. Both indices are derived views that can be rebuilt from scratch. Nothing is lost in the indices that was not already in the Org files.

The same principle extends beyond prose to structured data. Empirical parameters, validity envelopes, provenance chains, and benchmark results live in Org as property drawers and tables — the same format the user reads and edits. The system maintains a derived representation — the provenance store — optimized for machine queries. Like the two indices, it is a derived view rebuilt from Org, not a separate canonical copy. When the system learns something new, it writes back to the Org files, keeping the human layer current.

This is what sovereignty means in technical terms — the user owns the data in a format they can access, and the system operates on the same format. See design-decisions.org for the full argument.

The verification subsystem: the gate.

The gate is a function that takes (action, context, policy) and returns (permit | deny). Every action passes through it — a shell command from the user, a proposal from the LLM, a message from the network, a file write by a scheduled job. There is no privileged path around the gate. Root is not a concept in the gate model — root is a convention enforced by an OS that the gate replaces.

The gate has three decision vectors:

ACL2-verified procedures for security-critical checks — access control, message authentication, capability resolution. (ACL2 is a theorem prover and programming language for formal verification. It proves that code behaves correctly for all possible inputs, not just the ones tested.) This is the deductive layer.
Provenance- and validity-envelope checks for scientific and engineering integrity — does the empirical model apply in the current context? Are the parameters within their validated range? Is the input within the model's training distribution? These are predicates over the provenance store, not formal proofs. The gate queries the store and blocks or flags computations that fall outside validated bounds. This is the empirical layer — see Knowledge Layers for the full framework.
An LLM for natural-language reasoning — parsing the user's intent, evaluating whether an action falls within policy boundaries that require human judgment, interpreting gate flags and failure diagnostics. This is the probabilistic oracle — it proposes, never executes.

The ACL2 layer (vector 1) is deductive and authoritative where it applies — the LLM cannot overrule a verified denial. The provenance layer (vector 2) is authoritative over model validity — the LLM cannot override a validity envelope violation (though it may recommend a different model). The LLM layer (vector 3) is probabilistic and bounded by both lower layers.

The gate does not depend on OS privilege boundaries because it is in the evaluation loop itself. This is the architectural reason for the Lisp machine: a conventional OS interposes between the gate and the hardware. A Lisp machine eliminates that interposition by making the gate part of the evaluator.

How the gate knows which procedure belongs to which domain.

Every action entering the gate carries a domain tag. The tag is set by context — a file write under home/user/documents gets the "documents" domain, a network call to an approved registry gets "network", a shell command running a compiler gets "software-engineering". The domain tags form a tree: "files" has children "documents", "code", "config", "system", each with its own rule set.

The gate maintains a procedure registry mapping domain tags to ACL2-verified boundary functions. When an action arrives, the gate looks up the most specific domain tag that has a registered procedure. If "documents" has one, it uses that. If not, it walks up to "files". If no domain in the tree has a procedure, the action falls under LLM authority bounded only by the generic outer fence.

Domain tags are defined in the policy configuration — a hierarchy of Org headings or YAML that maps path patterns, network destinations, and command prefixes to domain names. New domains can be added at any time with no code changes, just a policy edit. New domains start with no verified procedures and rely entirely on the LLM until experience accumulates and ACL2 boundaries are written.

How the verified procedure registry grows.

Verified procedures are not all written upfront. The initial gate ships with a minimal set of obviously correct outer boundaries — three to five rules that prevent catastrophic, irreversible actions. The registry grows through three mechanisms:

Mistake-driven hardening: when the LLM's provisional authority causes harm, that action is logged, a human or automated process writes an ACL2 conjecture to prevent it, the Prover verifies it, and the resulting boundary function is added to the registry under the relevant domain tag.
Adversarial probing: the gate randomly injects probe actions that would violate known desirable boundaries but are caught before execution. These probes generate the same hardening signal even when no mistake occurred. They cover the blind spot where the LLM always gets it right and no error is ever logged.
Syscall wrappers: every action that crosses from the Lisp image into the host OS passes through a gate wrapper that records the kernel's response. When the kernel denies an action (permissions, seccomp, namespaces) that the gate had no rule for, the wrapper translates that kernel denial into a hardening signal — "the kernel prevented this. Consider codifying it as an ACL2 boundary." This covers the blind spot where the kernel catches the problem first and the gate never sees the danger.

These three channels feed a queue. The autodidactic loop (or a human reviewer) periodically processes the queue, drafts ACL2 conjectures, runs the Prover, and deploys new verified boundaries. The gate's procedure registry grows transaction by transaction, domain by domain, from three rules to hundreds to thousands over the lifetime of the system.

The two blind spots and their mitigations.

Blind spot 1 — the LLM always gets it right. If the LLM never attempts a dangerous action in a domain, no mistake is logged, and no ACL2 boundary is proposed. Mitigation: adversarial probing. The gate regularly tests the LLM with actions that would violate known safety properties, logged before execution. These probes generate hardening signals regardless of the LLM's accuracy.

Blind spot 2 — the kernel prevents the action before the gate sees it. If the LLM tries to write to /etc/shadow and the kernel's DAC permissions reject it, the LLM sees a permission error, the gate sees a failed action, but neither knows a safety boundary was enforced. Mitigation: syscall wrappers. The gate wraps every kernel transition and records the reason for denial. A kernel EACCES on /etc/shadow becomes a hardening signal: "the kernel has a rule about /etc/shadow that the gate doesn't. Codify it."

Without these mitigations, the gate's coverage converges to a plateau determined only by what has already broken, leaving large regions permanently dependent on the LLM's probabilistic reliability.

Gate decision flow (Neurosymbolic Agent stage): An action arrives carrying a domain tag. First, the gate checks the deductive layer — does this domain have registered ACL2-verified boundary procedures? If any denies, reject instantly. The LLM cannot overrule. If no verified procedure denies, the gate checks with Screamer — a constraint network built from rules extracted by the LLM and corrected by humans. Screamer resolves domain-specific constraints, rights, and prohibitions. If Screamer finds a resolution, apply it. If not, the gate asks the LLM. The LLM proposes permit or deny, and the gate re-checks against the deductive boundaries (defense in depth). Every decision is logged to the decision log.

How domains emerge: Domain tags are not assigned upfront. The user writes notes in Org. The symbolic index extracts entities and relationships. Screamer's constraint network connects them. Over time, clusters form — entities that mention each other frequently and mention outside entities rarely. The gate notices clusters where LLM utilization is high. It asks the LLM to label them: "This cluster deals with financial records. Shall I create a domain called accounting?" If the user confirms, the procedure registry gets a new tag. New domains start empty — no verified boundaries — and fill as mistakes accumulate.

The autodidactic loop runs in two parallel tracks.

Track 1 — deductive hardening: formal proof generation and gate rule improvement, fast loop, runs autonomously at LLM speed:

Read the decision log since the last run.
Identify high-frequency patterns where the LLM was invoked.
Propose Screamer constraints for the top patterns.
Check the hardening queue for new ACL2 conjectures ready to prove.
Check the adversarial probe results — did any probe reveal an unprotected boundary?
Check the syscall wrapper logs — did the kernel deny anything the gate missed?
Propose new domain clusters if LLM utilization in a cluster exceeds a threshold.
Run the Prover on pending conjectures.
If proofs pass, compile and deploy new boundary functions.
Log the cycle results.

Track 2 — empirical validation: provenance store improvement and parameter refinement, slow loop, requires experimental feedback:

Review computations since the last run where predictions were compared to experimental results.
For each comparison, compute the prediction error. If error exceeds the model's stated confidence interval, flag the parameter for review.
Parameter review: is the error systematic (model needs recalibration) or random (noise within expected range)?
For systematic errors: propose updated parameters (LLM), validate against held-out benchmarks (symbolic engine), update provenance store.
Envelope expansion: if a model was used in conditions outside its original validity envelope and the predictions matched experimental data, expand the envelope to include those conditions.
Bias profile update: incorporate the new comparison into the model's running bias profile.
Community sharing: publish validated parameter updates and envelope expansions through the social protocol.

Track 1 runs every cycle (minutes to hours). Track 2 runs when experimental data arrives (hours to months). Both are essential — the fast loop makes the system more secure; the slow loop makes it more useful for real-world science and engineering. See Knowledge Layers for the epistemic framework that motivates this split.

The social protocol: provable communication.

The social protocol extends the verified semantics beyond a single machine. It provides:

Self-sovereign DID identity (every instance has a cryptographic identity it controls)
DIDComm encrypted messaging (end-to-end encrypted, signed, DAG-tracked)
Personal data stores (user-owned, gate-controlled)
Relay network (asynchronous message delivery across trust boundaries)
Compute marketplace (provision verified compute you rent)
Liquid democracy (delegable voting over protocol governance)

Every message is signed by the sender's DID, tracked in a content-addressed DAG, and optionally notarized. Communication is provable when you choose it to be — you can prove what you sent, to whom, when, without revealing content.

The social protocol is not a blockchain. DAG-based ordering handles causality; delegable trust replaces proof of work.

The staged progression.

The full architecture — gate-verified Lisp machine on custom silicon — is the destination. The staged roadmap (see the stages directory for full detail) describes how each successive replacement eliminates a class of threat:

Development (baseline: Linux + Python agent + SQLite), Neurosymbolic Agent (the gate — root eliminated, provenance store operational), Social Protocol (provable communication), Lisp Machine (bare-metal — no MMU), AI Inference (in-process LLM), AI Weights (plist-native neural data), AI Training (verified fine-tuning), What Remains (physical, political, oracular limits).

Each stage is independently useful. Development is running today. The migration is progressive component swap, not a cut-over.

Self-developing hardware (Lisp Machine onwards): The hardware side of the Lisp Machine self-improves by synthesizing its own microcode. A Tenstorrent P150 (~72 RISC-V Tensix cores) runs Lisp microcode with one core dedicated to ACL2, one to Screamer, and the rest to gate verification and fact store operations. The system profiles its own gate verification latency, proposes a new microcoded instruction for the hot path, compiles RISC-V assembly from ACL2-verified specifications, loads it via PCIe DMA from within SBCL, benchmarks it — and rolls back if slower. The self-driving threshold: every subdomain involved (RISC-V ISA, SBCL internals, ACL2 metafunctions, compiler optimization) is software — the most codifiable domain — and can flip to symbolic sufficiency within days of ingestion.

Downstream effects.

When every action is gate-checked, every message is provable, and every computation runs on verified semantics, the security model shifts from empirical to deductive. The downstream effects cascade beyond personal computing:

Compliance becomes executable gate rules instead of annual audits. A SOC 2 report is a gate configuration, not a PDF.
AI safety becomes a verified gate between the LLM and the action stream instead of probabilistic guardrails or RLHF.
Software certification becomes the accumulated regression suite of every deployed instance — the Underwriters Laboratory for AI.
Operating systems become obsolete. The gate replaces the kernel, the address space replaces process isolation, and the verified evaluator replaces the privilege model.

18 KiB Raw Permalink Blame History

Architecture

18 KiB

Raw Permalink Blame History