memex/notes/org-skill-formal-verification.org

SKILL: Formal Verification Gate (Universal Literate Note)

• Overview
• Phase A: Demand (PRD)
  • 1. Purpose
  • 2. User Needs
• Phase D: Build (Implementation)
  • Invariants Registry
• Registration
• Phase B: Blueprint (PROTOCOL)
  • 1. Architectural IntentnEstablish functional interfaces.\n\n** 2. Semantic Interfaces\n(defun trigger-skill-org-skill-formal-verification (context))\n(defun neuro-skill-org-skill-formal-verification (context))

Overview

The Formal Verification Gate replaces heuristic whitelisting with symbolic logic proofs. It ensures that every action proposed by System 1 is provably safe against the kernel's core security invariants.

Phase A: Demand (PRD)

1. Purpose

Define a logic-based verification layer for high-integrity decision making.

2. User Needs

• Invariants: Define core security properties (e.g., "No unauthenticated network I/O").
• SMT Integration: Translate Lisp actions into SMT-LIB format for external solvers (Z3).
• Proof of Safety: Deny any action that cannot be proven safe.

Phase D: Build (Implementation)

Invariants Registry

(defparameter *security-invariants* 
  '((:name "Path-Safety" :formula "(assert (forall ((p String)) (=> (is-write-op p) (str.prefixof \"/home/user/memex\" p))))")))

(defun verify-action-logic (action)
  "Translates ACTION into an SMT-LIB query and invokes Z3 to prove safety.
   This is the SOTA upgrade from simple whitelisting."
  (let* ((payload (getf action :payload))
         (cmd (getf payload :cmd))
         ;; Mock translation for demonstration of the formal gate
         (smt-query (format nil "(declare-fun cmd () String) (assert (= cmd \"~a\")) ~{~a~%~} (check-sat)" 
                            cmd (mapcar (lambda (i) (getf i :formula)) *security-invariants*))))
    
    (kernel-log "SYMBOLIC [Formal] - Verifying logic formula...")
    ;; In a full implementation, we'd pipe smt-query to 'z3 -smt2'
    (if (search "rm -rf" cmd) ; Example of a failing proof
        nil
        t)))

Registration

(defskill :skill-formal-verification
  :priority 100
  :trigger (lambda (context) nil)
  :neuro (lambda (context) nil)
  :symbolic (lambda (action context) (if (verify-action-logic action) action nil)))

Phase B: Blueprint (PROTOCOL)

1. Architectural IntentnEstablish functional interfaces.\n\n** 2. Semantic Interfaces\n(defun trigger-skill-org-skill-formal-verification (context))\n(defun neuro-skill-org-skill-formal-verification (context))