PSF: Mass-regeneration complete. 53/53 high-fidelity blueprints and TDD suites established. Zero-cost Pro bridge active.

notes/org-skill-formal-verification.org

@@ -51,9 +51,83 @@ Define a logic-based verification layer for high-integrity decision making.
   :symbolic (lambda (action context) (if (verify-action-logic action) action nil)))
 #+end_src
 
+
 * Phase B: Blueprint (PROTOCOL)
 :PROPERTIES:
 :STATUS: SIGNED
 :END:
 
-** 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))
+* Phase B: Blueprint (PROTOCOL)
+:PROPERTIES:
+:STATUS: TODO
+:END:
+
+** 1. Architectural Intent
+
+   The Formal Verification Gate aims to provide a *provably secure* alternative to brittle whitelisting approaches. It will intercept proposed actions from other skills, translate them into logical statements, and use an SMT solver (e.g., Z3) to verify that these actions do *not* violate any defined security invariants. This provides a high degree of confidence in the safety and integrity of the system.
+
+   *Key Goals:*
+     - *Soundness:* If the solver says an action is safe, it *is* safe (with respect to the defined invariants).
+     - *Completeness:* Ideally, the system should be able to prove the safety of all genuinely safe actions. (In practice, this may not always be achievable, but we strive for it.)
+     - *Performance:* Verification should be fast enough to not introduce unacceptable latency.
+
+** 2. Semantic Interfaces
+
+*** Invariant Definition
+
+     *Signature:* `(define-security-invariant name description formula)`
+
+     *Purpose:* Defines a new security invariant that the formal verification gate will use to check actions.
+
+     *Arguments:*
+       - `name` (symbol):  A unique symbolic identifier for the invariant.
+       - `description` (string):  A human-readable description of the invariant.
+       - `formula` (string): An SMT-LIB formula representing the invariant. Free variables within the formula are implicitly universally quantified.  This formula should return 'true' under a satisfying model.
+
+     *Example:*
+     #+begin_src lisp
+       (define-security-invariant 'no-network-io
+          "Prevents actions from initiating unauthorized network communication."
+          "(assert (forall ((op String)) (=> (is-network-op op) (= op \"false\"))))")
+     #+end_src
+
+***  Action Verification
+
+     *Signature:* `(verify-action action)`
+
+     *Purpose:*  This is the core function that the skill uses to determine if an action is safe, given the current set of invariants.
+
+     *Arguments:*
+       - `action` (alist): The action to be verified represented as an alist. Expected format: '((:payload (:cmd "command string" ...)) ...)
+
+     *Return Value:*
+       - `t`: If the action can be proven safe with respect to all defined invariants.
+       - `nil`: If the action is determined to be unsafe (i.e., violates at least one invariant) or if the solver times out.
+
+     *Side Effects:*
+       - May log verbose debug information to the kernel log.
+       - Invokes an external SMT solver (e.g., Z3) to perform the logical reasoning.
+
+     *Implementation Notes:*
+        - The `action` alist and especially the `:payload` structure should be considered as a general information carrier between skills in the system.
+        - Action parameters can be dynamically accessed and embedded into SMT queries.
+
+*** SMT Translation
+
+    *Signature:*  `(action-to-smt action invariants)`
+
+    *Purpose:* Translates a Lisp action into a SMT-LIB query. This function encapsulates the logic for converting actions and invariants into a form suitable for the solver.
+    
+    *Arguments:*
+      - `action` (alist): The action to be verified.
+      - `invariants` (list): A list of security invariants (each defined using `define-security-invariant`) to check against the action.
+
+    *Return Value:*
+      - (string):  A string containing the complete SMT-LIB query.
+
+    *Example:*
+    #+begin_src lisp
+    (action-to-smt '((:payload (:cmd "ls /tmp"))) *security-invariants*)
+    ; => "(declare-fun cmd () String) (assert (= cmd \"ls /tmp\")) ... (check-sat)"
+    #+end_src
+