Skip to content

Releases: ohdearquant/LNkernel

lion-core v0.3.0 — initial public release

18 May 15:28
@ohdearquant ohdearquant
v0.3.0
dd23834
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Choose a tag to compare

View all tags
lion-core v0.3.0 — initial public release Latest
Latest

First public release of the Lion microkernel — a capability-bounded, formally verified microkernel for autonomous reasoning systems.

What's in the box

Rust crate (crates.io/crates/lion-core) — cargo add lion-core

  • Production microkernel types, state machine, and kernel API
  • 25 source files, ~13.9k LOC, #![deny(unsafe_code)]
  • 245 unit tests + 1 doctest, all green
  • serde feature flag for optional Serialize/Deserialize
  • Licensed under AGPL-3.0-or-later

Lean theory (under proofs/)

  • 73 .lean files formalizing the kernel's security properties
  • Mathlib v4.23.0 dependency
  • Licensed under Apache-2.0 (research-friendly)

What's verified (machine-checked)

Property Theorem
End-to-End Correctness any_reachable_from_init_is_secure — capstone theorem; any state reachable from the initial state satisfies full security
Complete Mediation Type-level enforcement via Authorized witness — no effect without authorization
Confinement Rights form a semilattice; delegation cannot amplify rights
Unforgeability UF-CMA game reduction over HMAC-SHA256; capability forgery probability ≤ 2^(-λ/2)
Deadlock Recovery Timeout-based liveness; no permanent deadlock
Workflow Termination Lexicographic measure decrease; every workflow terminates
Noninterference (TINI) Termination-insensitive via stuttering bisimulation
Attack Coverage All identified attack classes mitigated

Full audit, including the Trusted Computing Base (what we assume — WASM sandbox correctness, cryptographic hardness, scheduler fairness, hardware) is in TCB.md.

License

Dual-licensed by directory:

  • crates/ (Rust): AGPL-3.0-or-later — network-copyleft enforcement-grade license. Any service that integrates the kernel and is offered to third parties must release source.
  • proofs/ (Lean): Apache-2.0 — quotable, citable, portable for research and pedagogy.

See COPYRIGHT for the rationale.

Why a microkernel for AI?

Firewalls do not stop an agent from reasoning its way around restrictions. Access control lists do not bind a system that can request, persuade, or manipulate its way to elevated privileges. Sandboxes do not contain an entity that can reason about their boundaries.

See MANIFESTO.md for the long-form argument.

Getting started

[dependencies]
lion-core = "0.3"
use lion_core::{Kernel, SecurityLevel};

let mut kernel = Kernel::new();
kernel.register_plugin(1, SecurityLevel::Public, 4096)?;

API docs: https://docs.rs/lion-core/0.3.0

CI / quality

  • Rust workspace gates on fmt + clippy + test + no-default + doc + release-build for both ubuntu and macos
  • Pre-commit config covers hygiene, formatting, and secret scanning
  • All public source files carry SPDX license headers
  • Lean proof CI is wired but currently disabled in workflows (mathlib cold-build cost); will be re-enabled in a follow-up

Acknowledgements

This is research-grade infrastructure released in good faith. Cite, build on, and extend the proofs freely under Apache-2.0. The Rust implementation is AGPL-3 to keep commercial competition from packaging it as a hosted service without releasing their integrations — academic and self-hosted use is unaffected.

— HaiyangLi

Assets 2
Loading