amr/memex
1
0
Fork 0
Code Issues 12 Pull Requests Actions Packages Projects 1 Releases Wiki Activity

chore: unify bold syntax to single asterisk in .org files and update legacy memex-amero references

Browse Source
This commit is contained in:
Amr Gharbeia
2026-04-01 12:37:45 -04:00
parent 78ba3112cb
commit d364f90ff6
102 changed files with 955 additions and 955 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
notes/org-skill-formal-verification.org
View File

@@ -4,7 +4,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.
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)
:PROPERTIES:
@@ -15,9 +15,9 @@ The **Formal Verification Gate** replaces heuristic whitelisting with symbolic l
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.
- *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)