passepartout/docs/rca/rca-formal-verification.org

Root Cause Analysis: Lisp-Native Formal Verification Gate

• Executive Summary
• 1. Architectural Shift: Native vs. External
  • Issue
  • Resolution
• 2. Issue: Dependency Fragility
  • Symptoms
  • Root Cause
  • Resolution
• 3. Formal Invariants Implemented
• 4. org-agent Mandate Alignment
  • Soundness over Heuristics
  • Literate Granularity
• 5. Permanent Learnings

Executive Summary

Implemented a Lisp-Native Deterministic Prover to replace heuristic whitelisting with formal security invariants. This ensures that every high-impact action (shell, file I/O) is mathematically proven safe against the Autonomous's core mandates.

1. Architectural Shift: Native vs. External

Issue

The initial draft suggested using `Z3`, an external SMT solver. However, `Z3` was not available in the environment and would add significant complexity/bloat to the Docker image.

Resolution

Leveraged Common Lisp's inherent strength in symbol manipulation to build a Lisp-Native Prover. Invariants are defined as high-order predicates that operate on the structure of proposed actions. This provides a self-contained, high-performance verification layer.

2. Issue: Dependency Fragility

Symptoms

System failed to load with `Package STR does not exist`.

Root Cause

Incorrect assumption about the Quicklisp system name vs. the package name. The library is `cl-str` but the Quicklisp system is `str` and the package is `str`.

Resolution

1. Updated `org-agent.asd` to depend on `:str`.
2. Updated all source code and literate notes to use the `str:` prefix.
3. Verified via explicit `ql:quickload` in the test runner.

3. Formal Invariants Implemented

• Path Confinement: Deterministically proves that any file operation or absolute path in a shell command is strictly within the `/home/user/memex` root.
• No Network Exfiltration: Prevents the shell from invoking common exfiltration tools (`nc`, `ssh`, etc.) by inspecting the parsed command structure.

4. org-agent Mandate Alignment

Soundness over Heuristics

By moving to formal invariants, we have moved from "blacklisting bad things" to "proving safety." Any action that cannot be proven to satisfy all invariants is denied by default.

Literate Granularity

The `org-skill-formal-verification.org` file follows the "one definition per block" mandate, ensuring that the logic of each invariant is individually documented and verifiable.

5. Permanent Learnings

• Tooling Independence: Whenever possible, prefer native Lisp logic over external binaries for core security gates to reduce the attack surface and deployment complexity.
• Environment Consistency: Always use `(setf (uiop:getenv …) …)` for portable environment manipulation in tests.