Repository navigation
feat: legitimacy seam (ex-FDK) + Freedom Formal under decision-os meet - #8
Merged
Merged
Conversation
… meet Keep AuthGate TCB unchanged. Legitimacy is DENY-only via PolicyDecision; Freedom Formal is the default evaluator. FDK module remains a compat shim. Add research/freedom-fullscope engine, tests, and branch docs for with vs without legitimacy. Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Adds formal.yml and seccomp.yml CI jobs, rights-derived seccomp allowlists, monotonic SessionClock helper, adversarial execve test, and updates README and gap tables to match verified evidence on Linux CI. Co-authored-by: Cursor <cursoragent@cursor.com>
… T-SC1 - Fix seccomp adversarial test script indentation (unblocks CI + Seccomp workflow) - README engineering gaps: all closed/scoped; INFRA.md ties infra-ready to zero open gaps - Lean: prove T-SC1 for non-trailing paths; add FreedomKernel.lean + lake CI job - Honest DEPLOYMENT_READINESS D7 Lean counts Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
EOF Co-authored-by: Cursor <cursoragent@cursor.com>
- Main README: What's new (Aug 2026), CI workflow table, honest formal status - Add INDUSTRY_READINESS, KEY_MANAGEMENT, DISASTER_RECOVERY, MIGRATION - Sync formal/, attack_harness/, tcb/, STATUS, BRANCHES, DEPLOYMENT_READINESS - Deployment checklist 83% (code-addressable ops items closed) Co-authored-by: Cursor <cursoragent@cursor.com>
Add banner clarifying local vs ecosystem-level positioning authority. Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
AuthGate is the authority TCB. The book and philosopher edition live in Aliipou/freedom-theory. Co-authored-by: Cursor <cursoragent@cursor.com>
Aliipou
added a commit
that referenced
this pull request
Sep 16, 2026
… merge Kani (19 proved, CI-verified), Lean4 (partial - TCB/Temporal/MultiAgent proved, 2 sorry in Scope.lean, 2 crypto axioms), and TLC (CI-verified, formal/tlc_run.log) were stale/pessimistic on this page relative to what just landed from PR #8. Still honest -- Lean4 stays flagged as partial, not "fully proved".
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What problem does this solve?
FDK was a confusing second product name; legitimacy must compose with AuthGate under decision-os meet without changing the TCB.
Why this approach?
Rename the seam to legitimacy, keep the PolicyDecision JSON contract, use Freedom Formal as the DENY-only evaluator, leave CallGate/Rust TCB untouched. Ruled out: merging norms into TCB, all-Rust FDK port, keeping FDK as a parallel brand.
TCB Gate
Skipped — this PR does not touch
engine.rs,capability.rs,wire.rs, orcrypto.rs.General checklist
Design
Quality
unwrap()/expect()in TCB files (clippy enforces this)If AI-assisted
Test plan
Branches
with-legitimacy— this PRresearch/freedom-fullscope— same tip (lab)