🥮 mooncakes.io

    moonpermit

    Proof-carrying effect plans and least-authority runtime for AI agents

    ai-agent
    authorization
    capability
    security
    tooling
    Download zip
    Author
    Version
    0.1.0
    License
    Apache-2.0
    Repository
    Last updated
    8 hours ago
    Downloads
    2

    #MoonPermit

    CI License

    MoonPermit is a pure MoonBit library and CLI for compiling an AI agent's structured plan into a least-authority permit, checking every proposed tool effect against that permit, and emitting an explainable receipt with structured decision evidence.

    The core invariant is:

    realized effect <= approved effect
child permit    <= parent permit

    MoonPermit authorizes effects, not natural-language claims. It is designed to sit between an agent runtime and its tool executor. It is not an agent framework, an operating-system sandbox, a prompt-injection detector, or a production cryptographic credential system.

    #Status

    MoonPermit is under active development for the 2026 MoonBit September Hackathon. The repository starts from an empty public project, and development history is intentionally kept visible.

    Current milestone: the core vertical slice is runnable. Scope containment, budgeted runtime checks, non-amplifying delegation, approval diffs, JSON receipts, structured authorization proofs, and deterministic offline replay are implemented and tested.

    #Planned workflow

    structured plan -> compile minimum permit -> approve once
                -> check each tool call -> allow / deny / request expansion
                -> emit receipt + proof -> audit realized effects

    #Repository map

    • docs/proposal.md: one-page hackathon proposal.
    • docs/product-spec.md: user stories, scope, and acceptance criteria.
    • docs/architecture.md: effect algebra and trust boundaries.
    • docs/threat-model.md: security claims and explicit non-claims.
    • docs/acceptance-checklist.md: continuously maintained release gate.
    • docs/development-log.md: dated, public development record.
    • docs/quality.md: reproducible strict gate, coverage, and benchmarks.
    • docs/reviewer-guide.zh.md: Chinese reviewer guide and three-minute demo.
    • docs/cli.md: command reference and effect-expression grammar.
    • examples/basic: dependency-free end-to-end embedding example.
    • cmd/main: runnable CLI package.

    #Quick start

    Install the current stable MoonBit toolchain, clone this repository, and run:

    moon run cmd/main

    The default demo shows a structured proof, allow, budget exhaustion, expiry, rejected delegation, an authority expansion diff, and a successful offline receipt replay. No API key, network service, or paid dependency is needed.

    Compile a permit from the compact CLI effect grammar:

    moon run cmd/main -- compile docs-reader --calls 2 \
  read-tree:docs exec:moon,test,--deny-warn

    Check twice against a one-call grant; stdout is JSONL, one receipt per check:

    moon run cmd/main -- check --calls 1 --repeat 2 \
  read-tree:docs read:docs/guide.md

    Explain one atomic decision as machine-readable receipt-plus-proof JSON:

    moon run cmd/main -- explain --calls 2 --bytes 10 --expires 20 \
  --cost 4 --now 5 read-tree:docs read:docs/guide.md

    Other commands are delegate, diff, and audit. See docs/cli.md for the complete grammar and examples.

    #Library sketch

    ///|
    test {
      let permit = @moonpermit.compile_plan("docs", [
        @moonpermit.effect_request(
          @moonpermit.FileRead(@moonpermit.path_tree("docs")),
          @moonpermit.budget(max_calls=1),
        ),
      ])
      let runtime = @moonpermit.runtime(permit)
      let receipt = runtime.check(
        "read-1",
        @moonpermit.FileRead(@moonpermit.path_exact("docs/guide.md")),
        0L,
      )
      assert_true(receipt.allowed())

      let explained = @moonpermit.runtime(permit).check_with_proof(
        "read-with-proof",
        @moonpermit.FileRead(@moonpermit.path_exact("docs/guide.md")),
        0L,
      )
      assert_true(explained.receipt.allowed())
      assert_eq(explained.proof.reason, @moonpermit.ReasonCode::Granted)
    }

    All runtime time values are explicit logical Int64 timestamps. Expiry is exclusive. A finite budget is decremented only after scope, expiry, call, and byte checks all pass. check_with_proof returns its receipt and proof from that same state transition, so evidence generation never consumes budget twice.

    #Development

    Install the current stable MoonBit toolchain, then run:

    moon check --deny-warn
moon test --deny-warn
moon fmt --check
moon info

    See docs/quality.md for the current 62-test result, coverage denominators, reproducible benchmark workloads, and limitations.

    The complete local gate also passes from an isolated clean clone. Until a tagged release and remote CI are complete, the repository should still be treated as a transparent pre-release.

    #Security boundary

    MoonPermit is an application-level reference monitor. The embedding host must mediate every protected operation and provide truthful typed effects and time. Proofs and receipts are deterministic decision evidence, not cryptographic signatures or reusable authorization credentials. Proof explanations never copy secret values beyond the typed request identifier already being checked. See docs/threat-model.md and report vulnerabilities as described in SECURITY.md.

    #Open source and AI assistance

    The project is an original implementation licensed under Apache-2.0. Design influences, external specifications, and AI-assisted work are recorded in docs/prior-art.md and docs/ai-use.md. No third-party implementation is copied into this repository.

    #License

    Apache-2.0. See LICENSE.

    PermitError

    source
    pub(all) suberror PermitError {
      EmptyPermitId
      EmptyPlan
      InvalidCallLimit(Int)
      InvalidByteLimit(Int64)
      InvalidExpiry(Int64)
      EmptyInvocationId
      InvalidLogicalTime(Int64)
      InvalidByteCost(Int64)
      ChildAuthorityExceeded(String)
    } derive(Eq, ToJson, 
    Debug    )

    Invalid permit, budget, or plan input.

    ScopeError

    source
    pub(all) suberror ScopeError {
      EmptyPath
      AbsolutePath(String)
      ParentTraversal(String)
      AmbiguousSeparator(String)
      EmptyProgram
      InvalidHost(String)
      EmptyMethodSet
      InvalidMethod(String)
      EmptySecret
    } derive(Eq, ToJson, 
    Debug    )

    Why construction of a scope failed.

    AuditFinding

    source
    pub(all) struct AuditFinding {
      receipt_index : Int
      code : AuditIssueCode
      message : String
    } derive(Eq, ToJson, 
    Debug    )

    One evidence-integrity problem found during replay.

    AuditIssueCode

    source
    pub(all) enum AuditIssueCode {
      SequenceMismatch
      PermitMismatch
      ReplayMismatch
      InvalidReceipt
    } derive(Eq, ToJson, 
    Debug    )

    Stable category for one offline verification failure.

    AuditReport

    source
    pub struct AuditReport {
      checked : Int
      findings : Array[AuditFinding]
    } derive(Eq, ToJson, 
    Debug    )

    Result of deterministically replaying a receipt stream.

    AuditReport::checked

    source
    fn AuditReport::checked(self : AuditReport) -> Int

    AuditReport::findings

    source
    fn AuditReport::findings(self : AuditReport) -> Array[AuditFinding]

    AuditReport::passed

    source
    fn AuditReport::passed(self : AuditReport) -> Bool

    AuthorizationProof

    source
    pub(all) struct AuthorizationProof {
      sequence : Int
      invocation_id : String
      permit_id : String
      requested : EffectScope
      effect : String
      verdict : Verdict
      decision_grant_id : String?
      reason : ReasonCode
      checks : Array[ProofCheck]
    } derive(Eq, ToJson, 
    Debug    )

    Structured evidence for the exact runtime state transition that emitted a receipt. This is decision evidence, not a cryptographic proof.

    Budget

    source
    pub struct Budget {
      max_calls : Int?
      max_bytes : Int64?
      expires_at : Int64?
    } derive(Eq, ToJson, 
    Debug    )

    Optional limits attached to one effect grant. None means unbounded.

    Budget::expires_at

    source
    fn Budget::expires_at(self : Budget) -> Int64?

    Budget::max_bytes

    source
    fn Budget::max_bytes(self : Budget) -> Int64?

    Budget::max_calls

    source
    fn Budget::max_calls(self : Budget) -> Int?

    CheckedAuthorization

    source
    pub(all) struct CheckedAuthorization {
      receipt : Receipt
      proof : AuthorizationProof
    } derive(Eq, ToJson, 
    Debug    )

    Receipt and proof returned by one atomic authorization decision.

    CommandScope

    source
    pub struct CommandScope {
      program : String
      arguments : Array[String]
      allow_extra_arguments : Bool
    } derive(Eq, ToJson, 
    Debug    )

    A shell-free executable and argument scope.

    CommandScope::allows_extra_arguments

    source
    fn CommandScope::allows_extra_arguments(self : CommandScope) -> Bool

    CommandScope::arguments

    source
    fn CommandScope::arguments(self : CommandScope) -> Array[String]

    CommandScope::program

    source
    fn CommandScope::program(self : CommandScope) -> String

    Containment

    source
    pub(all) enum Containment {
      Contained
      NotContained(reason~ : String)
    } derive(Eq, ToJson, 
    Debug    )

    Structured result of an authority containment check.

    DataClass

    source
    pub(all) enum DataClass {
      Public
      Internal
      Confidential
      Secret
    } derive(Eq, ToJson, 
    Debug    )

    Sensitivity carried by data sent through a network effect.

    DiffEntry

    source
    pub(all) struct DiffEntry {
      effect : String
      budget : String
      verdict : Verdict
      covered_by : String?
      explanation : String
    } derive(Eq, ToJson, 
    Debug    )

    One requested grant classified against an already approved permit.

    EffectRequest

    source
    pub struct EffectRequest {
      effect : EffectScope
      budget : Budget
    } derive(Eq, ToJson, 
    Debug    )

    One requested effect and its intended resource budget.

    EffectRequest::budget

    source
    fn EffectRequest::budget(self : EffectRequest) -> Budget

    EffectRequest::effect

    source

    EffectScope

    source
    pub(all) enum EffectScope {
      FileRead(PathScope)
      FileWrite(PathScope)
      FileDelete(PathScope)
      ProcessExec(CommandScope)
      NetworkSend(NetworkScope)
      SecretRead(String)
    } derive(Eq, ToJson, 
    Debug    )

    Authority over an externally visible effect.

    EffectScope::canonical

    source
    fn EffectScope::canonical(self : EffectScope) -> String

    Grant

    source
    pub struct Grant {
      id : String
      effect : EffectScope
      budget : Budget
    } derive(Eq, ToJson, 
    Debug    )

    One normalized permit entry.

    Grant::budget

    source
    fn Grant::budget(self : Grant) -> Budget

    Grant::effect

    source
    fn Grant::effect(self : Grant) -> EffectScope

    Grant::id

    source
    fn Grant::id(self : Grant) -> String

    GrantState

    source
    type GrantState

    Mutable counters paired with one immutable compiled grant.

    HostScope

    source
    pub struct HostScope {
      canonical : String
      subdomains : Bool
    } derive(Eq, ToJson, 
    Debug    )

    A normalized DNS host scope.

    HostScope::canonical

    source
    fn HostScope::canonical(self : HostScope) -> String

    HostScope::includes_subdomains

    source
    fn HostScope::includes_subdomains(self : HostScope) -> Bool

    NetworkScope

    source
    pub struct NetworkScope {
      host : HostScope
      methods : Array[String]
      max_data_class : DataClass
    } derive(Eq, ToJson, 
    Debug    )

    Network authority combines a host scope, normalized HTTP methods, and the most sensitive data class that may leave the host.

    PathScope

    source
    pub struct PathScope {
      canonical : String
      tree : Bool
    } derive(Eq, ToJson, 
    Debug    )

    A normalized repository-relative path scope.

    Values can only be created through path_exact and path_tree, so an accepted value never contains an absolute path or a parent traversal.

    PathScope::canonical

    source
    fn PathScope::canonical(self : PathScope) -> String

    PathScope::is_tree

    source
    fn PathScope::is_tree(self : PathScope) -> Bool

    Permit

    source
    pub struct Permit {
      id : String
      grants : Array[Grant]
    } derive(Eq, ToJson, 
    Debug    )

    A deterministic set of grants approved for one plan.

    Permit::canonical

    source
    fn Permit::canonical(self : Permit) -> String

    Permit::grant_count

    source
    fn Permit::grant_count(self : Permit) -> Int

    Permit::grants

    source
    fn Permit::grants(self : Permit) -> Array[Grant]

    Permit::id

    source
    fn Permit::id(self : Permit) -> String

    PermitDiff

    source
    pub struct PermitDiff {
      approved_id : String
      requested_id : String
      entries : Array[DiffEntry]
    } derive(Eq, ToJson, 
    Debug    )

    Deterministic, requested-authority-centric permit comparison.

    PermitDiff::entries

    source
    fn PermitDiff::entries(self : PermitDiff) -> Array[DiffEntry]

    PermitDiff::render

    source
    fn PermitDiff::render(self : PermitDiff) -> String

    PermitDiff::requires_approval

    source
    fn PermitDiff::requires_approval(self : PermitDiff) -> Bool

    ProofCheck

    source
    pub(all) struct ProofCheck {
      kind : ProofCheckKind
      status : ProofCheckStatus
      grant_id : String?
      explanation : String
    } derive(Eq, ToJson, 
    Debug    )

    One deterministic, machine-readable authorization check.

    Explanations never include secret values or untyped request payloads.

    ProofCheckKind

    source
    pub(all) enum ProofCheckKind {
      InvocationUnique
      ScopeContained
      NotExpired
      CallBudgetAvailable
      ByteBudgetAvailable
    } derive(Eq, ToJson, 
    Debug    )

    Stable category for one check recorded in an authorization proof.

    ProofCheckStatus

    source
    pub(all) enum ProofCheckStatus {
      Pass
      Fail
      Skipped
    } derive(Eq, ToJson, 
    Debug    )

    Outcome of one check. Skipped checks are explicit rather than inferred.

    ReasonCode

    source
    pub(all) enum ReasonCode {
      Granted
      NoMatchingGrant
      PermitExpired
      CallBudgetExhausted
      ByteBudgetExhausted
      DuplicateInvocation
    } derive(Eq, ToJson, 
    Debug    )

    Stable machine-readable reason for a runtime decision.

    Receipt

    source
    pub(all) struct Receipt {
      sequence : Int
      invocation_id : String
      permit_id : String
      verdict : Verdict
      grant_id : String?
      requested : EffectScope
      effect : String
      logical_time : Int64
      byte_cost : Int64
      reason : ReasonCode
      message : String
      remaining_calls : Int?
      remaining_bytes : Int64?
    } derive(Eq, ToJson, 
    Debug    )

    Explainable evidence emitted for every checked invocation.

    Receipt::allowed

    source
    fn Receipt::allowed(self : Receipt) -> Bool

    Runtime

    source
    pub struct Runtime {
      permit_id : String
      states : Array[GrantState]
      seen_invocations : 
    Set    [String]
      receipts : Array[Receipt]
      sequence : Int
    }

    Stateful, single-owner evaluator for one permit.

    Runtime::check

    source
    fn Runtime::check(self : Runtime, invocation_id : String, requested : EffectScope, now : Int64, byte_cost? : Int64) -> Receipt raise PermitError

    Runtime::check_with_proof

    source
    fn Runtime::check_with_proof(self : Runtime, invocation_id : String, requested : EffectScope, now : Int64, byte_cost? : Int64) -> CheckedAuthorization raise PermitError

    Runtime::delegate

    source
    fn Runtime::delegate(self : Runtime, child_id : String, requests : Array[EffectRequest], now : Int64) -> Permit raise PermitError

    Runtime::permit_id

    source
    fn Runtime::permit_id(self : Runtime) -> String

    Runtime::receipt_count

    source
    fn Runtime::receipt_count(self : Runtime) -> Int

    Runtime::receipts

    source
    fn Runtime::receipts(self : Runtime) -> Array[Receipt]

    Runtime::remaining_budget

    source
    fn Runtime::remaining_budget(self : Runtime, grant_id : String) -> Budget?

    Verdict

    source
    pub(all) enum Verdict {
      Allow
      Deny
      NeedsApproval
    } derive(Eq, ToJson, 
    Debug    )

    Runtime authorization result.

    audit_receipts

    source
    fn audit_receipts(permit : Permit, receipts : Array[Receipt]) -> AuditReport

    budget

    source
    fn budget(max_calls? : Int, max_bytes? : Int64, expires_at? : Int64) -> Budget raise PermitError

    budget_contains

    source
    fn budget_contains(grant : Budget, requested : Budget) -> Bool

    budget_intersection

    source
    fn budget_intersection(left : Budget, right : Budget) -> Budget

    command_contains

    source
    fn command_contains(grant : CommandScope, requested : CommandScope) -> Bool

    command_exact

    source
    fn command_exact(program : String, arguments : Array[String]) -> CommandScope raise ScopeError

    command_prefix

    source
    fn command_prefix(program : String, arguments : Array[String]) -> CommandScope raise ScopeError

    compile_plan

    source
    fn compile_plan(permit_id : String, requests : Array[EffectRequest]) -> Permit raise PermitError

    diff_permits

    source
    fn diff_permits(approved : Permit, requested : Permit) -> PermitDiff

    effect_contains

    source
    fn effect_contains(grant : EffectScope, requested : EffectScope) -> Containment

    effect_intersection

    source
    fn effect_intersection(left : EffectScope, right : EffectScope) -> EffectScope?

    effect_request

    source
    fn effect_request(effect : EffectScope, budget : Budget) -> EffectRequest

    grant_contains

    source
    fn grant_contains(grant : Grant, requested : Grant) -> Bool

    host_and_subdomains

    source
    fn host_and_subdomains(input : String) -> HostScope raise ScopeError

    host_contains

    source
    fn host_contains(grant : HostScope, requested : HostScope) -> Bool

    host_exact

    source
    fn host_exact(input : String) -> HostScope raise ScopeError

    network_contains

    source
    fn network_contains(grant : NetworkScope, requested : NetworkScope) -> Bool

    network_scope

    source
    fn network_scope(host : HostScope, methods : Array[String], max_data_class : DataClass) -> NetworkScope raise ScopeError

    path_contains

    source
    fn path_contains(grant : PathScope, requested : PathScope) -> Bool

    path_exact

    source
    fn path_exact(input : String) -> PathScope raise ScopeError

    path_tree

    source
    fn path_tree(input : String) -> PathScope raise ScopeError

    permit_contains

    source
    fn permit_contains(grant : Permit, requested : Permit) -> Bool

    runtime

    source
    fn runtime(permit : Permit) -> Runtime

    unlimited_budget

    source
    fn unlimited_budget() -> Budget

    Source Files

    Powered by MoonBit

    Site sourceReport issuePackagesBuild queueSkillsStatistics

    © 2026 mooncakes.io