#+TITLE: Root Cause Analysis: Lisp-Native Formal Verification Gate
#+DATE: 2026-04-11
#+FILETAGS: :rca:security:formal-verification:autonomy:

* 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 `opencortex.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. opencortex 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.
