:PROPERTIES:
:ID:       4819956d-a2ec-403d-99f8-4ccb13efb7c2
:CREATED:  [2026-03-31 Tue 20:28]
:EDITED:   [2026-04-11 Sat 17:45]
:END:
#+TITLE: SKILL: Formal Verification Gate (Universal Literate Note)
#+STARTUP: content
#+FILETAGS: :security:logic:formal-methods:autonomy:

* Overview
The *Formal Verification Gate* replaces heuristic whitelisting with deterministic logic proofs. It ensures that every action proposed by Probabilistic Engine is *provably safe* against the harness's core security invariants using a Lisp-native deterministic prover.

** Deep Reasoning: The Sandbox of Intent
This gate is the first line of defense against both "Inside Threats" (maliciously modified skill files) and "Hallucination Threats" (LLMs generating unsafe commands). 

1. **Isolation from Implementation:** The Prover does not trust the logic inside a skill. It sits between the skill's proposal and the physical world.
2. **Structural Enforcement:** Even if a skill is compromised and attempts to execute a command like `rm -rf /`, the Prover identifies the violation of the `path-confinement` invariant and blocks it before it hits the OS.
3. **Prover vs. Bouncer:**
   - **The Prover (Static):** Focuses on *Structure*. "Is this path legal? Is this tool allowed?"
   - **The Bouncer (Runtime):** Focuses on *Content*. "Is this message leaking my API keys? Is this network packet unauthorized?"

* Phase A: Demand (PRD)
:PROPERTIES:
:STATUS: SIGNED
:END:

** 1. Purpose
Define a logic-based verification layer for high-integrity decision making without external SMT dependencies.

** 2. Success Criteria
- [ ] *Invariants:* Express security properties as Lisp predicates.
- [ ] *Soundness:* Block any action that fails a deterministic safety check.
- [ ] *Path Confinement:* Prove that file operations are confined to the Autonomous's memex.
- [ ] *Network Protection:* Prove that shell commands do not attempt unauthorized data exfiltration.

* Phase B: Blueprint (PROTOCOL)
:PROPERTIES:
:STATUS: SIGNED
:END:

** 1. Architectural Intent
The gate operates as high-priority middleware. It decomposes proposed actions and applies a suite of formal invariants. Unlike simple string matching, it evaluates the *intent* and *impact* of the action within the current context.

** 2. Semantic Interfaces
- `(def-invariant name action-type (action context) ...)`
- `(verify-action-formally action context)`

* Phase D: Build (Implementation)

** Package Context
#+begin_src lisp
#+end_src

** Invariant Registry
Global store for all registered security invariants.

#+begin_src lisp
(defvar *formal-invariants* (make-hash-table :test 'equal)
  "Registry of security invariants used by the Formal Verification Gate.")
#+end_src

** Invariant Definition Macro
#+begin_src lisp
(defmacro def-invariant (name action-type (action context) &body body)
  "Defines a formal security invariant. 
   BODY must return T for safe actions and NIL for unsafe ones."
  `(setf (gethash (string-downcase (string ',name)) *formal-invariants*)
         (list :name ',name
               :type ,action-type
               :logic (lambda (,action ,context) ,@body))))
#+end_src

** Invariant: Path Confinement
Ensures all file-related operations (including shell calls that touch files) are confined to the memex root.

#+begin_src lisp
(def-invariant path-confinement :all (action context)
  "Forces all path-based operations to reside within the Autonomous Memex."
  (declare (ignore context))
  (let* ((payload (getf action :payload))
         (path (or (getf payload :file) (getf payload :path)))
         (cmd (getf payload :cmd))
         (memex-root (or (uiop:getenv "MEMEX_DIR") "/home/user/memex")))
    (cond
      ;; If a path is explicitly provided, verify it is absolute and within root
      (path 
       (let ((truename (ignore-errors (namestring (truename path)))))
         (if truename
             (str:starts-with-p memex-root truename)
             ;; If file doesn't exist yet, check string prefix
             (str:starts-with-p memex-root path))))
      ;; If it's a shell command, check for absolute paths outside memex
      (cmd 
       (not (cl-ppcre:scan "(^|\\s)/((etc|var|proc|root|sys)|(home/(?!user/memex)))" cmd)))
      (t t))))
#+end_src

** Invariant: No Network Exfiltration
Blocks common tools and patterns used for data exfiltration via the shell.

#+begin_src lisp
(def-invariant no-network-exfil :shell (action context)
  "Prevents shell commands from establishing unauthorized external connections."
  (declare (ignore context))
  (let* ((payload (getf action :payload))
         (cmd (getf payload :cmd)))
    (if (and cmd (stringp cmd))
        (let ((forbidden-tools '("nc" "netcat" "ssh" "scp" "rsync" "ftp" "telnet")))
          (not (some (lambda (tool) (cl-ppcre:scan (format nil "(^|\\s)~a(\\s|$)" tool) cmd)) 
                     forbidden-tools)))
        t)))
#+end_src

** Verification Engine
The core prover that applies all relevant invariants to an action.

#+begin_src lisp
(defun verify-action-formally (action context)
  "Deterministically proves that ACTION satisfies all applicable security invariants."
  (let ((action-target (getf action :target))
        (action-type (getf action :type))
        (all-passed t))
    (maphash (lambda (id inv)
               (declare (ignore id))
               (let ((inv-type (getf inv :type))
                     (inv-logic (getf inv :logic))
                     (inv-name (getf inv :name)))
                 (when (or (eq inv-type :all)
                           (eq inv-type action-target)
                           (eq inv-type action-type))
                   (unless (funcall inv-logic action context)
                     (harness-log "FORMAL FAILURE: Action ~s violated invariant ~a" action inv-name)
                     (setf all-passed nil)))))
             *formal-invariants*)
    all-passed))
#+end_src

** Registration: Skill
#+begin_src lisp
(defskill :skill-formal-verification
  :priority 95 ; Just below Bouncer
  :trigger (lambda (context) (declare (ignore context)) nil) ; Middleware only
  :probabilistic nil
  :deterministic (lambda (action context)
              (if (verify-action-formally action context)
                  action
                  (let ((err (format nil "Formal verification failed for action: ~s" action)))
                    `(:type :log :payload (:level :error :text ,err))))))
#+end_src