amr/passepartout
1
0
Fork 0
Code Issues 15 Pull Requests 1 Actions Packages Projects Releases Wiki Activity

docs: global terminology update from kernel/core to harness

Browse Source
This commit is contained in:
Amr Gharbeia
2026-04-12 18:28:11 -04:00
parent 475f79e79d
commit 3f8c37712c
71 changed files with 255 additions and 499 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
skills/org-skill-formal-verification.org
View File

@@ -8,7 +8,7 @@
#+FILETAGS: :security:logic:formal-methods:psf:
* 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 using a Lisp-native symbolic prover.
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 harness's core security invariants using a Lisp-native symbolic 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).
@@ -130,7 +130,7 @@ The core prover that applies all relevant invariants to an action.
(eq inv-type action-target)
(eq inv-type action-type))
(unless (funcall inv-logic action context)
(kernel-log "FORMAL FAILURE: Action ~s violated invariant ~a" action inv-name)
(harness-log "FORMAL FAILURE: Action ~s violated invariant ~a" action inv-name)
(setf all-passed nil)))))
*formal-invariants*)
all-passed))