LNkernel
a formally verified agentic system for capability-bounded autonomous reasoning
File Explorer
- ci.yml
- LionConcurrency.lean
- LionIsolation.lean
- CapabilityModel.tla
- IsolationModel.tla
- LionCore.tla
- PolicyModel.tla
- APPENDIX_A_NOTATION_REFERENCE.md
- APPENDIX_B_BIBLIOGRAPHY.md
- ch1_content.tex
- ch2_content.tex
- ch3_content.tex
- ch4_content.tex
- ch5_content.tex
- lion-ecosystem.bib
- main.tex
- main_bibtex.tex
- ch1-0-abstract.md
- ch1-1-introduction.md
- ch1-2-mathematical-preliminaries.md
- ch1-3-architecture-category.md
- ch1-4-categorical-security.md
- ch1-5-functors-transformations.md
- ch1-6-implementation.md
- ch1-7-summary.md
- ch1-bibliography.md
- README.md
- ch2-1-introduction.md
- ch2-10-security-analysis.md
- ch2-11-implementation-correspondence.md
- ch2-2-system-model.md
- ch2-3-theorem-2.1.md
- ch2-4-theorem-2.2.md
- ch2-5-theorem-2.3.md
- ch2-6-theorem-2.4.md
- ch2-7-implementation.md
- ch2-8-mechanized-verification.md
- ch2-9-implications.md
- ch2-bibliography.md
- README.md
- ch3-0-abstract.md
- ch3-1-memory-isolation.md
- ch3-2-theorem-3.1.md
- ch3-3-actor-model.md
- ch3-4-theorem-3.2.md
- ch3-5-integration.md
- ch3-6-verification-recap.md
- ch3-7-summary.md
- ch3-bibliography.md
- README.md
- ch4-0-abstract.md
- ch4-1-mathematical-foundations.md
- ch4-2-policy-evaluation.md
- ch4-3-theorem-4.1.md
- ch4-4-workflow-model.md
- ch4-5-theorem-4.2.md
- ch4-6-composition-algebra.md
- ch4-7-summary.md
- ch4-bibliography.md
- README.md
- ch5-0-abstract.md
- ch5-1-policy-correctness.md
- ch5-2-workflow-termination.md
- ch5-3-end-to-end-correctness.md
- ch5-4-implementation-roadmap.md
- ch5-5-future-research.md
- ch5-6-summary.md
- ch5-bibliography.md
- README.md
- liongate_v1.pdf
- README.md
- actor.rs
- kernel.rs
- memory.rs
- mod.rs
- plugin.rs
- state.rs
- thread.rs
- workflow.rs
- authorization.rs
- host_call.rs
- kernel_op.rs
- mod.rs
- plugin_internal.rs
- capability.rs
- identifiers.rs
- mod.rs
- policy.rs
- rights.rs
- runtime.rs
- security.rs
- crypto.rs
- error.rs
- extract_anchor.rs
- kernel.rs
- lib.rs
- Cargo.toml
- Cargo.lock
- Cargo.toml
- Basic.lean
- UseLimits.lean
- AttackCoverage.lean
- Bridge.lean
- Compatible.lean
- ComponentSafe.lean
- CompositionTheorem.lean
- EndToEnd.lean
- PolicyWorkflowBridge.lean
- SecurityComposition.lean
- StructuralDefs.lean
- StructuralInvariants.lean
- SystemInvariant.lean
- AllContracts.lean
- AuthContract.lean
- CapContract.lean
- Interface.lean
- MemContract.lean
- PolicyContract.lean
- RuntimeCorrespondence.lean
- StepAffects.lean
- CountPGeneral.lean
- CountPLemmas.lean
- Crypto.lean
- HashMapLemmas.lean
- Identifiers.lean
- Policy.lean
- Rights.lean
- RuntimeIsolation.lean
- SecurityLevel.lean
- SeparationLogic.lean
- Actor.lean
- Kernel.lean
- Memory.lean
- Plugin.lean
- State.lean
- Workflow.lean
- Authorization.lean
- Footprint.lean
- HostCall.lean
- HostCallFootprint.lean
- KernelOp.lean
- PluginInternal.lean
- Step.lean
- Footprint.lean
- FrameCases.lean
- StepCases.lean
- Attenuation.lean
- CapabilityUniqueness.lean
- Confinement.lean
- ConstraintImmutability.lean
- DeadlockFreedom.lean
- IntegrityNoninterference.lean
- Mediation.lean
- MediationRules.lean
- MessageDelivery.lean
- Noninterference.lean
- NoninterferenceBase.lean
- NoninterferenceRules.lean
- PolicySoundness.lean
- PolicySoundnessRules.lean
- Revocation.lean
- RuntimeTrustBundle.lean
- SpatialSafety.lean
- StutteringBisimulation.lean
- TemporalSafety.lean
- TemporalSafetyRules.lean
- Termination.lean
- Unforgeability.lean
- WorkflowAlgebra.lean
- WorkflowAuthorization.lean
- lake-manifest.json
- lakefile.lean
- lean-toolchain
- LICENSE
- Lion.lean
- add_license_headers.sh
- ci.sh
- lean_ci.sh
- .gitignore
- .pre-commit-config.yaml
- COPYRIGHT
- deno.json
- LICENSE
- Makefile
- MANIFESTO.md
- README.md
- TCB.md
# Use via CDN
jsDelivrjsDelivr serves any public GitHub repository as a CDN with zero setup. Pick a version and a file to get a ready-to-paste link and snippet.
Link
Example
// repository documentation
Was this content helpful?
(0 ratings)