Law Does Not Return a Boolean

TL;DR

Legal drafting is not ordinary prose that has failed to become code. It is a way of allocating precision, choice, authority, and review. A payment clause may fix an amount and deadline. A trust clause may intentionally let a trustee choose within a fiduciary standard. An incapacity clause may specify who can make a status operative and on what record. An exception may defeat a general rule. An ambiguous phrase may support more than one meaning. Those are different legal moves, even when a conventional rules engine flattens all of them into input Booleans.

I propose a language called Fidryn. Its deterministic fragment computes dates, amounts, allocations, and other closed rules. Its legal kernel represents sources, roles, powers, duties, evidence, acts, and bitemporal state. Its typed judgment effects mark the exact places where a computation needs an observation, authorized determination, discretionary choice, interpretation, conflict resolution, or selection of applicable law.

A case-file handler may discharge an effect with a valid record. A scenario handler may supply a labeled hypothetical. A bounded explorer may branch over every declared lawful completion. If the unresolved branches still yield the same answer, Fidryn returns that answer with a trace. If they diverge, it returns the alternatives and the legal pivot. If the necessary authority, record, or interpretation is absent, it says so instead of guessing.

The governing rule is a no-false-determinacy principle:

A legal computation may return one determinate result only when that result is invariant across every still-admissible resolution of the unresolved issues, or when a competent authority has already made a determination that is operative in the relevant context.

This essay now goes far enough to be an implementation prompt. It gives the proposed surface language, core IR, static rules, evaluator, handlers, diagnostics, repository shape, and v0.1 acceptance tests. It also works through four deliberately different uses: a revocable trust, a California premarital agreement, a dated slice of federal FOIA, and formation of a Massachusetts LLC.

There are two useful reading paths. A research reader can follow the drafting problem, the three trustee outcomes, the verification boundary, and the falsifiable research wager. An implementer should also read the outcome and effect types, the four stress tests, the v0.1 contract, and every acceptance test. The implementation section is deliberately more like an RFC than an essay.

Fidryn would not make law mechanically decidable. It would make the boundary between calculation and legal judgment explicit, typed, traceable, and testable.

Part I: legal drafting is a distribution of precision

Consider four clauses. They are fictional, but their differences are ordinary:

The Trustee shall distribute net income on the last business day
of each calendar quarter.

The Settlor shall be treated as incapacitated when two licensed
physicians concur in writing after examination.

The Trustee may distribute principal for a beneficiary's health,
education, maintenance, and support, in the Trustee's good-faith judgment.

The Trustee shall furnish an accounting within a reasonable time.

The first clause tries to determine a result. Once the trust's income, calendar, and acting trustee are known, the remaining work resembles a total program: calculate a date and create a duty.

The second clause defines a procedure by which a proposition becomes operative for a particular purpose. It is about evidence, qualifications, concurrence, and legal effect. The third gives an officeholder a bounded power. The drafter is not necessarily being imprecise. The drafter may be deliberately refusing to choose today what only a trustee, facing facts years later, should choose. Turning that clause into best_interest = true deletes who may exercise the discretion, what must be considered, which choices are available, and how a court may review the decision. The fourth invokes an open-textured standard. It expects later evaluation against facts the document does not exhaustively enumerate.

Legal instruments move among these modes constantly:

Not all openness is intentional. Discretion, open texture, ambiguity, missing language, conflicting sources, and unknown facts are different phenomena. A useful formal language should not celebrate all uncertainty as wise drafting. It should preserve the deliberate forms, expose the accidental forms, and never convert one into another by convenience.

Programming languages already have mechanisms for making category errors, unresolved dependencies, and provenance explicit. Fidryn's wager is that those mechanisms can carry legal authority and review rather than merely application data. A proposition is not its proof. A physical act is not its legal effect. Permission is not power. A judge is not a callback that supplies whichever Boolean lets execution continue.

That is the problem Fidryn is designed to address.

A certificate is not incapacity

Suppose a revocable trust says that the settlor will be treated as incapacitated for purposes of trust administration when two licensed physicians concur in writing. The first version of the program is tempting:

on Incapacity(Bryan) {
    suspend Bryan as Trustee
    appoint first_eligible(successor_trustees)
}

It is also doing nearly all of the important legal work offstage.

What is Incapacity(Bryan)? It could name an underlying medical condition, a physician's opinion, an instrument-defined status, a court's conclusion, or the legal effect that activates a succession clause. Those are not interchangeable. One certificate does not itself establish the instrument-defined operative status. Two certificates may satisfy the trust's private procedure without binding a court in a later proceeding. A successor named in the document may still need to be eligible, receive notice, and accept the office. A later order may reverse the incapacity determination without unwinding every transaction completed in reliance on it.

The legally material path is closer to this:

possible underlying condition
    -> evidentiary items
    -> instrument-defined qualification
    -> authorized determination
    -> operative status for a stated purpose
    -> suspension or vacancy
    -> acceptance of office
    -> new legal powers and duties

Every arrow can fail in a different way. Every successful arrow needs a reason.

An event/state model remains useful, but a bare transition system with a single truth-valued state store leaves much of this structure implicit. Its simplest shape takes a current state and an event and returns a new state:

That remains useful, but it is too compressed to be the whole semantics. A legal system also asks whether an occurrence was proved, which rule qualified it, whether the rule was in force, which institution had competence, whether the actor possessed the relevant power, whether required formalities were satisfied, whether the act was permitted, and whether a later tribunal may revise the result.

The hard problem is not only representing what changes. It is representing why a change is legally operative, for whom, for what purpose, and subject to which paths of challenge.

This essay is a language-design proposal, not an encoding of an actual trust and not legal advice. The examples deliberately compress doctrine so that the programming language problem stays visible.

The language: Fidryn

I will call the language Fidryn, pronounced “FID-rin.” The name is coined rather than borrowed from Latin. It is meant to suggest fidelity: to source text, source version, institutional authority, the evidentiary record, and the reasons supporting an outcome. It is a provisional research name, not a claim of legal authority. Any public release would still need ordinary trademark, domain, and package-registry clearance.

Fidryn has two layers:

Fidryn surface modules
    lawyer-readable declarations and instrument syntax
                    |
                    v
Fidryn Core
    a small typed, proof-relevant, authority-indexed IR
                    |
                    +--> reference evaluator
                    +--> bounded completion explorer
                    +--> verification backends
                    +--> trace and source-map renderer
                    +--> constrained prose renderer

The surface language can eventually support specialized profiles for private instruments, legislation, administrative workflows, and litigation records. All of them must elaborate to one canonical Core. A trust clause and a federal statute may look different to their drafters, but Power, Duty, Determination, SourceRef, Interval, and TraceNode must not acquire incompatible meanings in different tools.

The file extension in this proposal is .fidryn; the command-line program is fidryn. The syntax shown in the worked modules is the v0.1 surface-design target rather than disposable if/then pseudocode. The earlier conceptual snippets use a few explanatory shorthands. The implementation contract later identifies the normative Core, the lowering boundary, and the parser work that must be frozen before those modules become parser goldens. Later surface conveniences may not weaken the static checks.

The language is built around a short set of commitments:

propositions are not Booleans
records are not truth
determinations are scoped institutional acts
offices are temporal relations, not person subtypes
power, permission, validity, effect, and violation are independent
legal state changes require a constitutive basis
priority requires a sourced doctrine
ambiguity branches instead of disappearing
open worlds require closure evidence for universal claims
every conclusion carries valid time, record time, and provenance
determinate means invariant over the declared admissible completion space

Those commitments lead first to a type distinction.

A legal status is not a truth value

One early sketch I considered used a status type like this:

type LegalTruth =
    True
  | False
  | Unknown
  | Disputed
  | PresumedTrue
  | PresumedFalse
  | AdjudicatedTrue
  | AdjudicatedFalse

That looks cautious because it contains more than true and false. It is actually a type error disguised as nuance.

Disputed is not a truth value. It describes a relation between claims in a proceeding. PresumedTrue describes the procedural consequence of a rule that may shift a burden. AdjudicatedTrue describes the product of an institutional process. An adjudicated proposition can be wrong about the world and still control a case. A presumption can operate while the proposition remains unknown. A proposition can be disputed after one court has decided it if the decision is under review or lacks force in a different proceeding.

At least these dimensions must remain separate:

A better core uses different objects. In v0.1, Prop is a first-class sort. It is not a generic placeholder and it has no implicit conversion to Bool:

sort Prop

type Claim {
    content: Prop
    asserted_by: Party
    proceeding: Proceeding
    asserted_at: Time
}

type Evidence {
    item: EvidenceItem
    relation: Supports(Prop) | Attacks(Prop)
    provenance: EvidenceProvenance
    admissibility: AdmissibilityStatus
}

type Determination {
    issue: Prop
    result: Established | NotEstablished
    decider: Authority
    record: EvidentiaryRecord
    standard: DecisionStandard
    scope: LegalContext
    valid_time: Interval
    finality: FinalityStatus
    review: ReviewStatus
}

The central relation is not

It is closer to

Here ValidDetermination includes the source-defined constitutive effect, competent authority, operative interval, and absence of an effective stay or reversal. A valid NotEstablished result does not establish $P$, and failure to establish $P$ does not by itself establish its negation.

The hidden world and the operative legal record may diverge. That divergence is not a pathology the model should erase. It is necessary to test erroneous but effective decisions, protected reliance, later reversal, and the difference between what happened and what an institution is legally required to treat as having happened.

What an honest evaluator may return

A conventional function is expected to return a value or an ordinary execution error. A legal query needs a richer result because many reasons for noncompletion are not errors.

type Outcome<T> =
    Determinate {
        value: T
        trace: TraceId
        convergence_certificate: Option<CompletionProofId>
        ignored_open_issues: FiniteSet<OpenRequest>
    }

  | Contingent {
        alternatives: Map<BranchId, T>
        pivots: FiniteSet<OpenIssue>
        trace: TraceId
    }

  | Suspended {
        requests: NonEmptySet<OpenRequest>
        trace: TraceId
    }

  | NormConflict {
        graph: ArgumentGraph
        trace: TraceId
    }

  | OutsideCompetence {
        request: OpenRequest
        reason: CompetenceFailure
        trace: TraceId
    }

  | Inconsistent {
        core: UnsatCore
        trace: TraceId
    }

type OpenRequest =
    NeedEvidence {
        issue: PropPattern
        schema: RecordSchemaId
    }
  | NeedJudgment {
        issue: Prop
        protocol: JudgmentProtocolId
    }
  | NeedChoice {
        protocol: DecisionProtocolId
        options: FiniteSet<LegalAction>
    }
  | NeedInterpretation {
        source: SourceSpan
        family: InterpretationFamilyId
    }
  | NeedApplicableLaw {
        issue: LegalIssue
        candidates: FiniteSet<SourceVersion>
    }

type PropPattern =
    Ground(Prop)
  | Match {
        predicate: PropId
        arguments: Vec<TermPattern>
    }

type TermPattern = Exact(Term) | Bind(Binder) | Wildcard

type LegalStatusPattern =
    PropositionStatus {
        proposition: PropPattern
        context: ContextPattern
    }
  | InstitutionalStatus {
        constructor: StatusConstructorId
        arguments: Vec<TermPattern>
    }

type LegalEffectPattern =
    Establish(LegalStatusPattern)
  | Terminate(LegalStatusPattern)
  | Suspend(LegalStatusPattern)
  | CreatePosition(PositionPattern)
  | Affect(LegalSubjectPattern)

type PositionPattern = MatchPosition {
    kind: PositionKind
    arguments: Vec<TermPattern>
}

type LegalSubjectPattern =
    Exact(LegalSubjectRef)
  | Bind(Binder)
  | Wildcard

type ContextPattern = CurrentContext | Exact(ContextId) | AnyContext

_ is legal only inside one of these checked patterns. It never creates an implicit existential in an ordinary expression. In a status position, a bare proposition pattern is injected as PropositionStatus { proposition, context: CurrentContext }. In an effect position, establish P, terminate P, and suspend P inject that status into the matching effect constructor. The narrower as_to X shorthand injects Affect(Exact(X)); it matches only staged effects whose typed subject is X, not every effect whose printed text happens to mention X. A NeedEvidence pattern asks for a record that can bind the missing terms; the successful observation supplies those bindings and records them in the trace.

Suspended { NeedJudgment(...) } is not the same as a crash. It can be the correct output of a sound legal computation. Contingent is not a vague “maybe.” It contains the reachable answers and the precise pivots that separate them. OutsideCompetence is not merely missing data: it says that this evaluator, office, or tribunal lacks authority to produce the requested effect.

The design should also avoid a different form of excessive caution. An unresolved issue does not necessarily make every downstream answer unresolved. Two interpretations of a clause may disagree about the reasoning but still place Alice in office. If all admissible branches converge on Alice, the trustee query can be determinate even while the interpretive issue remains open.

That gives the core soundness target.

Let $\Sigma$ be the available legal state, and let $\mathcal{C}_q(\Sigma)$ be the set of total admissible completions relevant to query $q$. Each member resolves every still-open fact, authorized determination, interpretation, discretionary choice, conflict, and source selection that can affect $q$, within the declared finite model. A branch with an unbounded or undeclared resolution domain is not a completion and may not be discarded; evaluation must suspend unless a checked convergence certificate proves that every admissible extension of that branch returns the same answer. Let $\mathcal{O}_q(\Sigma)$ be those remaining open branch prefixes. Then:

I call this the no-false-determinacy principle.

It is deliberately stronger than “the program did not encounter an unknown.” The evaluator has to establish that every legally admissible unresolved completion agrees, or that an authoritative determination has closed the issue within the scope of the query.

There is a formal trap here. If Determinate is defined to mean “invariant over every admissible completion,” the displayed implication is true largely by definition. The substantive work is to define admissibility without hiding the legal problem, construct a conservative procedure that can establish convergence, and prove that each handler preserves the authority, scope, time, and closure conditions used by the semantics.

A small counterexample makes the quantifiers concrete. Two complete branches that both return Bob justify Determinate(Bob) only if those branches exhaust the declared possibilities. Add one unresolved branch that might return Alice and the result must suspend. Delete every admissible branch and the universal equality is vacuously true, but there is no valid answer: the nonempty-completion condition rules that case out. A convergence certificate must cover every extension of an open branch and identify a satisfiable witness; a few agreeing samples are not such a certificate.

Judgment effects: carrying an authorized dependency

The programming-language mechanism I would test is an algebraic effect system.

Algebraic effects separate an abstract operation from the handler that gives the operation meaning in a particular run. The same computation can ask to read state, choose nondeterministically, or perform I/O without hard-coding one global implementation. A handler can interpret the request interactively, symbolically, from a stored record, or by exploring alternatives. Plotkin and Pretnar's foundational treatment formalizes this separation between effect operations and handlers.

The built-in legal operations look like this. Judgment payloads contain Prop values; observation requests accept PropPattern so records can bind missing terms. Their effect rows track which operation kinds a function may request:

effect Observe {
    request(
        issue: PropPattern,
        schema: RecordSchemaId
    ) -> EvidentialStatus
}

effect Determine {
    request(
        issue: Prop,
        protocol: JudgmentProtocolId
    ) -> Determination
}

effect Choose {
    request(
        options: FiniteSet<LegalAction>,
        protocol: DecisionProtocolId
    ) -> Decision
}

effect Interpret {
    request(
        source: SourceSpan,
        family: InterpretationFamilyId
    ) -> SelectedInterpretation
}

effect ResolveNormConflict {
    request(
        conflict: ArgumentGraph,
        doctrines: FiniteSet<ConflictDoctrine>
    ) -> ConflictResolution
}

effect SelectApplicableLaw {
    request(
        issue: LegalIssue,
        candidates: FiniteSet<SourceVersion>
    ) -> ApplicableLawSet
}

A trustee-succession core can then expose its unresolved legal dependencies in its type:

fn acting_trustee_core(trust: Trust)
    -> LegalPerson
    ! {
        Determine,
        Observe,
        Interpret
    }
{
    require operative Incapacitated(
        trust.settlor,
        Administer(trust)
    )

    return nominated_successors(trust)
        |> filter(candidate_is_eligible)
        |> filter(candidate_has_accepted)
        |> first_by_nomination_rank
}

The effect row after ! is part of the public contract. This function is not automatic in the sense that a date calculation is automatic. It may require an incapacity determination, evidence of acceptance, and an interpretation of eligibility.

Algebraic effects do not intrinsically provide this row-polymorphic tracking; that is an additional language-design choice. Nor does invoking a handler make its answer legally authoritative. The case-file handler must validate the imported determination's competence, provenance, scope, time, and review status before resuming the computation.

Crucially, the core does not dictate how those requests are resolved.

handler CaseFileExcerpt handles {Determine}
{
    on Determine.request(issue, protocol) {
        match record.controlling_determination(issue) {
            Some(d) if validate(protocol, d) =>
                resume d with determination_trace(d)
            None =>
                suspend NeedJudgment {issue, protocol}
        }
    }
}

That excerpt shows the semantic hinge without front-loading the runtime. Part III gives the complete four-operation handler, including invalid records, invalid authority, and trace propagation.

Effects and outcomes are different layers. Effects describe what the core computation may request. Outcome<T> describes what a particular handler reports when it cannot—or should not—discharge those requests.

fn acting_trustee_in_case(trust: Trust)
    -> Outcome<LegalPerson>
{
    handle CaseFile in acting_trustee_core(trust)
}

CaseFile wraps an ordinary core return as Determinate and maps a request it cannot legitimately discharge to Suspended, OutsideCompetence, or Contingent.

A hypothetical handler can inject declared assumptions. A model-checking handler can branch over every lawful result. A skeptical handler can collapse those branches only when they converge.

This is not a claim that every legal dependency is automatically an algebraic effect in the formal sense, or that arbitrary user-defined legal handlers will be sound. Those are questions for the calculus. The proposal is that the operation/handler boundary is the right place to make legal nonmechanicality explicit without making the formal core useless.

One trust, three legitimate answers

Return to the trustee query. The record contains one physician certificate. Alice is nominated first and Bob second, but neither has taken office. Under the illustrative instrument, one certificate does not produce an operative incapacity determination, so Bryan's existing occupancy continues. The case record is closed as to certificates received by the query's record_time, and this fixture makes a later completed physician protocol operative only prospectively. The explorer can therefore prove that any future response to the outstanding evidence request leaves the officeholder at the queried valid_time unchanged.

The current-status query is determinate:

Determinate {
    value: Bryan
    trace: Trace#T10 {
        uses: {InitialOccupancy#O1}
    }
    convergence_certificate: CompletionProof#P11
    ignored_open_issues: {
        NeedEvidence {
            issue: Incapacitated(Bryan, Administer(BRT))
            schema: SecondConcurringCertificate
        }
    }
}

The pending succession transition matters, but it does not make the current officeholder unknown. No false determinacy does not mean maximal refusal.

ignored_open_issues is legal only with a completion proof in the trace showing that every declared response preserves the queried value. A case-file handler cannot attach that field merely because it believes an issue is unimportant; it must call the bounded explorer or reuse a checked convergence certificate.

Now change the record. A second conforming certificate arrives, the instrument's protocol produces an operative determination, and Bryan's occupancy is suspended. Alice and Bob have both validly accepted. Under interpretation I1, Alice is eligible and takes priority. Under I2, Alice is ineligible and Bob is the highest-ranked eligible nominee.

The same query now has two genuinely different answers:

Contingent {
    alternatives: {
        I1: Alice
        I2: Bob
    }

    pivots: {
        EligibilityClause(BRT, Alice) {
            under I1: Eligible(Alice) => Alice
            under I2: NotEligible(Alice) => Bob
        }
    }

    trace: Trace#T21 {
        common: {
            Determination#D17,
            SuspensionRule#R31,
            Acceptance#A18,
            Acceptance#A19
        }
    }
}

The evaluator has computed the boundary of what the present record supports. Suppose a competent court later selects I2 for this administration. The query can then return:

Determinate {
    value: Bob
    convergence_certificate: none
    ignored_open_issues: {}
    trace: Trace#T30 {
        valid_time: [acceptance_effective_time, +inf)
        uses: {
            Determination#D17,
            SuspensionRule#R31,
            Nomination#N2,
            CourtInterpretation#I2,
            Acceptance#A19
        }
    }
}

Current certainty, genuine contingency, and later operative certainty are different results for different reasons. Each is auditable. Fidryn refuses only when the legal paths relevant to the query actually diverge.

What the kernel must keep separate

Effects explain how a computation can stop or branch. They do not, by themselves, explain what the computation ranges over. For that, a single map of Boolean facts is still too weak.

I would begin with legal state partitioned into related stores:

where:

• $W$ is the occurrence and world-hypothesis ledger: persons, assets, physical acts, and modeled events. Its hidden-truth substore is available only to tests and simulations; ordinary legal rules must work through records and determinations;
• $R$ is the evidentiary and procedural record;
• $L$ is institutional legal state: title, validity, and other operative legal statuses;
• $N$ contains Hohfeldian legal positions: duty and claim, liberty and no-right, power and liability, immunity and disability;
• $A$ is authority, jurisdiction, institutional competence, office occupancy, and delegated authorization;
• $D$ is the set of determinations, orders, discretionary decisions, valuations, and reviews;
• $I$ is the active interpretation or set of admissible interpretations; and
• $V$ is the source, amendment, effective-time, and version environment.

The partitions are conceptual, not a demand for eight physical databases. Their purpose is to prevent category errors. An evidentiary record is not institutional title. A private power is not a court's subject-matter competence. Office occupancy is not an intrinsic subtype of a person. A source version is not the interpretation selected for a particular issue.

Every material item should carry at least two clocks:

valid_time   // when the fact, rule, or effect legally applies
record_time  // when it became known or entered this system

Suppose a court enters an order in 2036 holding that a trust amendment executed in 2032 was ineffective from the start. A query asking what the record showed in 2033 is different from a query, asked in 2036, about the legal state valid in 2033. Ordinary event time cannot express both. This is a bitemporal problem.

A transition should therefore produce both new state and a proof-relevant trace:

Here $\Gamma$ is the source and rule environment, $\iota$ is the interpretation context, $x$ is an occurrence, submission, attempted act, or judgment, and $\tau$ records the evidence, authority, source, conflict doctrine, interpretation, and assumptions used.

That trace is not optional debugging metadata. It is part of the answer.

Five static refusals

The proposal becomes clearer as a set of prohibitions.

1. No proposition may silently coerce to a Boolean

This should fail:

if Incapacitated(Bryan) {
    activate Succession(BRT)
}

The drafter must say which status of the proposition matters:

when operative(
    Incapacitated(Bryan, Administer(BRT)),
    in = Administration(BRT)
) {
    activate Succession(BRT)
}

Other explicit uses might include assumed inside a scenario, determined with a particular determination, or necessarily across an interpretation space. There is no default coercion because there is no harmless default meaning.

2. Institutional facts may not be assigned like object fields

This should also fail:

BRT.revocable = false

Irrevocability is a legal effect. The trace needs a constitutive rule, a competent institutional act, or a valid exercise of power:

rule IrrevocabilityAtDeath : constitutive
    from BRT.instrument.clause("7.1")
{
    when operative Dead(Bryan)
        in Administration(BRT)

    then constitute Irrevocable(BRT)
}

3. External decisions may not enter as opaque Boolean oracles

reasonable_efforts = external_input<bool> hides exactly what the language exists to show. An external result must identify the issue, decider, authorization, record, standard, scope, time, and review posture—or be marked explicitly as a hypothetical assumption.

4. Rule priority may not be an unexplained integer

priority = 100 is useful to a rule engine and meaningless as legal justification. The preference must be produced by a named doctrine whose own source and applicability can be challenged: mandatory law over a private term, a valid later amendment over an earlier clause, a specific provision over a general one under stated conditions, or a controlling decision within its jurisdictional scope.

5. Ambiguity may not disappear because of declaration or solver order

If two admissible interpretations produce different beneficiaries, the output is contingent. The implementation may not select the first model returned by a solver and present it as “the” result.

These refusals sound restrictive. They are the point. A language that makes a hard legal problem pleasant to encode by erasing its hard parts is optimizing for the wrong thing.

Facts becoming operative: incapacity is a protocol

The earlier trust fragment can now be written more honestly in the v0.1 surface syntax.

proposition Incapacitated(
    person: NaturalPerson,
    purpose: CapacityPurpose
)

evidence_type PhysicianCertificate {
    issuer: LicensedPhysician
    subject: NaturalPerson
    purpose: CapacityPurpose
    conclusion: Supports | Opposes
    examination_time: Time
    signed_at: Time
}

judgment TrustIncapacity(
    person: NaturalPerson,
    trust: Trust
)
decides Incapacitated(person, Administer(trust))
{
    source:
        trust.instrument.clause("4.2")

    primary_authority:
        concurrence(
            count = 2,
            distinct = true,
            role = LicensedPhysician
        )

    record requires:
        c1: PhysicianCertificate
        c2: PhysicianCertificate

        where:
            c1.subject == person
            and c2.subject == person
            and c1.purpose == Administer(trust)
            and c2.purpose == Administer(trust)
            and c1.issuer != c2.issuer
            and fresh(c1, within = 90 days)
            and fresh(c2, within = 90 days)

    decision_rule:
        established
        when c1.conclusion supports issue
         and c2.conclusion supports issue

        not_established
        when c1.conclusion opposes issue
         and c2.conclusion opposes issue

        otherwise unresolved

    constitutive_effect:
        established =>
            operative issue
            in Administration(trust)

    duration:
        until superseded by
            CapacityRestoration(person, trust)

    review:
        forum = CourtWithTrustJurisdiction(trust)
        standard = DeNovo
        results = {Affirm, Reverse, Vacate, Remand}
}

This protocol still makes legal-design choices that a real instrument and governing law would have to supply. What counts as a licensed physician? Are the certificates current? What happens when the opinions split? Can the settlor refuse examination? May a third party rely on the determination? Does restoration operate prospectively? The language does not answer these questions for the drafter. It makes their absence visible.

The succession rule consumes the operative status produced by the protocol:

rule SuccessorAssumesOffice : constitutive
    from BRT.instrument.clause("4.4")
{
    require unique nomination_rank
        among nominations_for(TrusteeOf(BRT))

    select unique candidate
        from nominations_for(TrusteeOf(BRT))
        where operative Eligible(candidate, TrusteeOf(BRT))
          and effective AcceptOffice(candidate, TrusteeOf(BRT))
        order_by nomination_rank ascending

    when vacancy_or_suspension(TrusteeOf(BRT))

    then constitute Occupies(candidate, TrusteeOf(BRT))

    otherwise activate CourtAppointmentProcedure(BRT)
}

first_eligible has become a procedure with visible prerequisites. Static duplicate ranks are E410 AmbiguousSelection. Unknown eligibility raises an effect; it does not count as ineligibility. The otherwise branch runs only after the finite nomination set is closed and every candidate is established ineligible or has declined. Acceptance is a legal act, not a Boolean field. If nobody qualifies, the model activates a separate appointment path instead of producing an undefined trustee.

Power is not permission, validity, or effect

The incapacity clause shows how a proposition becomes operative. Other clauses allocate power rather than establish facts. The first trust sketch said:

permit Bryan {
    amend(BRT)
}

That conflates at least four questions:

1. Does Bryan possess a legal power to alter the trust's legal relations?
2. Is exercising that power permitted, or does another duty constrain it?
3. Did the attempted amendment satisfy the required formalities?
4. What effect, if any, did the legal system recognize?

The distinction matters because law regularly recognizes acts that are effective but wrongful. It also permits attempts that fail to produce the intended legal effect.

power SettlorAmendmentPower(
    holder: Bryan,
    subject: BRT
)
to constitute Adopted(amendment: TrustAmendment)
{
    source:
        BRT.instrument.clause("2.1")

    active_while:
        operative Alive(Bryan)

    exercise_by:
        AmendTrust(Bryan, BRT, amendment)
}

legal_act AmendTrust(
    actor: NaturalPerson,
    trust: Trust,
    amendment: TrustAmendment
)
{
    exercises:
        SettlorAmendmentPower(actor, trust)

    validity requires:
        operative HasCapacity(actor, Execute(amendment))
            using Determine
        and SignedWriting(amendment, actor)
        and Delivered(amendment, ActingTrustee(trust))

    constitutive_effect:
        Adopted(amendment)

    defects:
        no_power => Ineffective
        missing_signature => Ineffective
}

The governing implications are separate:

while

Neither implication collapses into the other. Prohibition does not necessarily erase power. Effectiveness does not prove permission. This distinction is already explicit in normative systems such as eFLINT; the additional wager here is that the language can connect power exercise to formalities, evidence, determinations, defect classes, challenge rights, and remedies without losing that separation.

The resulting act type should be able to distinguish at least:

type ActOutcome<E: LegalEffect> =
    Ineffective { defects: FiniteSet<ValidityDefect> }
  | Effective { effect: E, compliance: Compliant }
  | EffectiveButWrongful {
        effect: E,
        violations: FiniteSet<NormViolation>
    }
  | Voidable {
        provisional_effect: E,
        challenge_holder: LegalPerson,
        deadline: Time
    }

These categories would need domain-specific refinement. Their purpose here is to block the familiar but invalid inference that an illegal act cannot happen, or that an act which happened must have been legally effective. An unresolved capacity issue does not fabricate a half-formed ActOutcome; evaluation returns Outcome<ActOutcome<E>>::Suspended with a NeedJudgment request.

Discretion is authorized choice

Power says who can produce a legal effect. Discretion says how much choice that power leaves. Open-textured standards create another temptation:

predicate BestInterest(person, action)
    -> Discretionary<Bool>

The type admits discretion and still models it as a hidden truth-value provider. The legally significant object is usually the structured decision process.

decision_protocol TrusteeDistributionDecision(
    trustee: LegalPerson,
    trust: Trust,
    beneficiary: Beneficiary,
    proposed: Distribution
)
{
    competent_when:
        occupies(trustee, TrusteeOf(trust))

    choice_space:
        proposed.amount >= 0
        and proposed.amount <= distributable_principal(trust)
        and proposed.recipient == beneficiary

    must_consider:
        beneficiary.health
        beneficiary.education
        beneficiary.maintenance
        beneficiary.other_resources
        trust.remaining_needs

    must_not_consider:
        trustee.personal_financial_interest
        irrelevant_animus

    record requires:
        written_reasons
        identified_information_sources
        material_factors_considered

    standard:
        GoodFaithAndBestInterests

    output:
        Approve(proposed)
      | Reject(proposed)
      | Modify(proposed)

    review:
        forum = CourtWithTrustJurisdiction(trust)
        standard = AbuseOfDiscretion
}

A compiler can check structured assertions that the decision-maker occupied the office, the proposed amount was inside a defined range, and required record fields were supplied. It cannot, without an additional trusted analysis, establish from unstructured reasons that a factor was actually considered or absent. It usually cannot prove that the decision was substantively in the beneficiary's best interests.

Formal verification is still useful. The model checker can quantify over every choice the protocol permits:

verify TrustRemainsSolventUnderDiscretion {
    for_all decision in lawful_choices(
        TrusteeDistributionDecision
    )

    assert always:
        trust_liquidity(BRT) >= required_reserve(BRT)
}

This verifies a robust property of the discretionary range. It does not counterfeit a mechanical answer to the discretionary standard.

Ambiguity is not discretion

Discretion is authorized choice within a source-defined space. Ambiguity is unresolved meaning. Neither is a Boolean, but they branch for different reasons. Formalization often hides interpretation by selecting one reading before execution. That may be necessary for a particular legal opinion, but it should not be an invisible property of the encoding.

LegalRuleML already provides a mechanism to record alternative formalizations and connect rules to source and context metadata, but it does not prescribe an operational semantics for choosing among those alternatives. The language proposed here would add an executable semantics over them.

interpretation_family DistributionRepresentation
    for BRT.instrument.clause("9.3")
{
    alternative StrictPerStirpes {
        defines allocate as
            divide_at_root_generation
            then represent_deceased_members_by_branch
    }

    alternative PerCapitaAtEachGeneration {
        defines allocate as
            pool_at_first_generation_with_living_member
            then redistribute_equally_by_generation
    }

    alternative InstrumentDefinedMeaning {
        defines allocate as
            BRT.instrument.definition("per_stirpes")
    }

    admissibility:
        InstrumentDefinedMeaning when explicit_definition_exists
        StrictPerStirpes when supported_by(governing_law)
        PerCapitaAtEachGeneration when supported_by(governing_law)

    selector:
        explicit instrument definition defeats external default
        otherwise request Interpret {
            source: BRT.instrument.clause("9.3")
            family: DistributionRepresentation
        }
}

The query language can quantify over the family:

query necessarily final_shares(BRT) == allocation
query possibly Alice receives more_than(1 / 2)
query contingent final_shares(BRT)
query final_shares(BRT) under StrictPerStirpes

If two admissible readings yield different shares, the result should name the clause, the interpretations, the divergent allocations, and the authority capable of selecting an operative reading. If all readings produce the same allocation, that conclusion may be determinate even before the interpretive dispute is resolved.

Source conflicts need the same honesty. “Mandatory rule wins” is not a total ordering over legal sources. Applicability can depend on jurisdiction, subject matter, time, institutional competence, mandatory or default status, choice of law, preemption, waiver, specificity, and procedural posture. A conflict may be resolved by defeat, but it may also be harmonized, narrowed, severed, or left for an authorized institution.

The output should distinguish resolution by a named doctrine from harmonization, severance, and a still-unresolved argument graph that names the authority capable of deciding it. An integer can schedule a rule engine. It cannot stand in for this explanation.

Part II: four Fidryn stress tests

The language has to survive more than one friendly trust clause. The following examples exercise four different shapes of law:

These are normative design fixtures, not finished parser inputs, legal forms, or advice. A production encoding would require lawyers in the relevant jurisdiction, authenticated source artifacts, and a stated question. Every example therefore begins with a jurisdiction, a source snapshot, effective and record times, and an outside_scope declaration.

Example 1: build a revocable trust

The trust example is the most complete because it drives v0.1. It combines an instrument with an imported governing-law module, but it keeps their authority separate.

module Examples.BryanRevocableTrust version "0.1.0" {
    jurisdiction Massachusetts
    source_snapshot "2026-08-23-ma-trust-fixture"
    source_manifest "sources/ma-trust-fixture.manifest.json"
    effective_at 2026-08-23
    recorded_at 2026-08-23T12:00:00-04:00

    outside_scope {
        tax
        creditor_priority
        real_property_recording
        complete_Massachusetts_trust_law
    }

    source Instrument {
        kind private_instrument
        authority Bryan as SettlorOf(BRT)
        artifact "sources/bryan-revocable-trust.txt"
        effective [execution_time, +inf)
    }

    import MA.TrustLaw.Fixture version "2026-08-23"

    entity Bryan : NaturalPerson
    entity Alice : NaturalPerson
    entity Bob : NaturalPerson
    entity BRT : Trust

    office TrusteeOf(trust: Trust) occupied_by LegalPerson {
        cardinality 0..1
        acquired_by Effective(AcceptOffice)
        suspended_by OperativeIncapacity
        lost_by {Death, EffectiveResignation, EffectiveRemoval}
        competence {AdministerTrust, DecideTrustDistributions}
    }

    proposition Alive(person: NaturalPerson)
    proposition Dead(person: NaturalPerson)
    proposition TrustInstrumentExecuted(trust: Trust)
    proposition Incapacitated(
        person: NaturalPerson,
        purpose: CapacityPurpose
    )
    proposition Eligible(person: LegalPerson, office: Office)

    interpretation_family SuccessorEligibility
        for Instrument.clause("4.4")
    {
        alternative I1 {
            defines Eligible(Alice, TrusteeOf(BRT)) as established
            defines Eligible(Bob, TrusteeOf(BRT)) as established
        }

        alternative I2 {
            defines Eligible(Alice, TrusteeOf(BRT)) as not_established
            defines Eligible(Bob, TrusteeOf(BRT)) as established
        }

        selector explicit_instrument_definition
          or controlling_interpretation
          or request Interpret
    }

    rule InitialTrustee : constitutive
        from Instrument.clause("1.2")
    {
        when operative TrustInstrumentExecuted(BRT) in TrustCreation(BRT)
        then establish Occupies(Bryan, TrusteeOf(BRT))
    }

    nomination Alice for TrusteeOf(BRT) rank 1
        from Instrument.clause("4.4.a")

    nomination Bob for TrusteeOf(BRT) rank 2
        from Instrument.clause("4.4.b")

    evidence_type PhysicianCertificate {
        issuer: LicensedPhysician
        subject: NaturalPerson
        purpose: CapacityPurpose
        conclusion: Supports | Opposes
        examined_at: Time
        signed_at: Time
    }

    judgment TrustIncapacity(person: NaturalPerson, trust: Trust)
        decides Incapacitated(person, Administer(trust))
        from Instrument.clause("4.2")
    {
        authority concurrence(2 distinct LicensedPhysician)

        record requires c1: PhysicianCertificate
        record requires c2: PhysicianCertificate
        where same_subject_and_purpose(c1, c2)
          and c1.issuer != c2.issuer
          and fresh(c1, 90 days)
          and fresh(c2, 90 days)

        establish when c1.conclusion == Supports
                     and c2.conclusion == Supports

        reject when c1.conclusion == Opposes
                  and c2.conclusion == Opposes

        otherwise suspend NeedJudgment {
            issue: Incapacitated(person, Administer(trust))
            protocol: CourtCapacityDetermination
        }

        on established
            make issue operative in Administration(trust)

        review by CourtWithTrustJurisdiction(trust) under DeNovo
    }

    legal_act AcceptOffice(candidate: LegalPerson, office: Office) {
        performer candidate
        validity requires SignedWriting(candidate, office)
        effect establish Accepted(candidate, office)
        source Instrument.clause("4.4")
    }

    rule SuspendIncapacitatedTrustee : constitutive
        from Instrument.clause("4.3")
    {
        when operative Incapacitated(Bryan, Administer(BRT))
            in Administration(BRT)

        then suspend Occupies(Bryan, TrusteeOf(BRT))
    }

    rule HighestRankedSuccessor : constitutive
        from Instrument.clause("4.4")
    {
        require closed nominations_for(TrusteeOf(BRT))
        require unique nomination_rank

        select unique candidate
            from nominations_for(TrusteeOf(BRT))
            where operative Eligible(candidate, TrusteeOf(BRT))
              and effective AcceptOffice(candidate, TrusteeOf(BRT))
            order_by nomination_rank ascending

        when vacancy_or_suspension(TrusteeOf(BRT))
        then establish Occupies(candidate, TrusteeOf(BRT))
        otherwise activate CourtAppointmentProcedure(BRT)
    }

    power SettlorAmendmentPower {
        holder Bryan
        subject BRT
        effect Adopted(amendment: TrustAmendment)
        active_while operative Alive(Bryan)
        source Instrument.clause("2.1")
    }

    legal_act AmendTrust(amendment: TrustAmendment) {
        performer Bryan
        exercises SettlorAmendmentPower
        validity requires operative HasCapacity(Bryan, Execute(amendment))
            using Determine
        validity requires SignedWriting(amendment, Bryan)
        validity requires Delivered(amendment, ActingTrustee(BRT))
        effect establish Adopted(amendment)
    }

    rule IrrevocableAtDeath : constitutive
        from Instrument.clause("7.1")
    {
        when operative Dead(Bryan) in Administration(BRT)
        then establish Irrevocable(BRT)
        then terminate SettlorAmendmentPower
    }

    duty PostDeathAdministration {
        bearer ActingTrustee(BRT)
        claimant BeneficiariesOf(BRT)
        attaches when operative Dead(Bryan) in Administration(BRT)
        content {
            IdentifyTrustAssets(BRT)
            ResolveAllowedClaims(BRT)
            ResolveApplicableTaxes(BRT)
            MaintainReserve(BRT)
            DistributeResidue(BRT)
        }
        discharge_by AdministrationTerminal(BRT)
        violation_when due_and_unperformed
    }

    decision TrusteeDistributionDecision(
        trustee: LegalPerson,
        proposed: Distribution
    ) {
        authority occupant TrusteeOf(BRT)
        options lawful_distributions(proposed)
        must_consider {health, education, maintenance, support}
        must_not_consider {trustee_personal_interest}
        record requires WrittenReasons
        standard GoodFaithAndBestInterests
        review by CourtWithTrustJurisdiction(BRT)
            under AbuseOfDiscretion
    }

    query acting_trustee()
        -> LegalPerson
        ! {Observe, Determine, Interpret}
    {
        goal UniqueOccupant {
            office TrusteeOf(BRT)
        }
    }

    verify TrusteeContinuity {
        interpretations all_admissible
        judgments all_lawful
        choices all_lawful
        bounds {persons: 8, events: 40, time_points: 80}

        assuming fair_response(CourtAppointmentProcedure)

        assert always
            occupied(TrusteeOf(BRT))
            or active CourtAppointmentProcedure(BRT)
    }
}

This module can generate an instrument outline, but its more important products are the questions it refuses to hide: no capacity determination exists; a nominee has not accepted; two ranks collide; the family set is not closed; tax law is outside the loaded source bundle; or the trustee's choice needs a record and review protocol.

Example 2: build a California premarital agreement

A premarital agreement tests a different distinction: execution is not the same as effectiveness, and neither guarantees enforceability against a particular party or provision years later.

California provides a useful dated example. Its current code says that a premarital agreement must be in writing and signed, becomes effective upon marriage, restricts agreements affecting child support, and supplies issue-specific rules for voluntariness, disclosure, unconscionability, counsel, and spousal-support provisions. The source for this illustrative module is California Family Code sections 1610–1617.

module Examples.AvaNoahPrenup version "0.1.0" {
    jurisdiction California
    source_snapshot "2026-08-23-ca-family-1610-1617"
    source_manifest "sources/ca-family-1610-1617.manifest.json"
    effective_at 2026-08-23
    recorded_at 2026-08-23T12:00:00-07:00

    outside_scope {
        complete_choice_of_law_analysis
        tax
        bankruptcy
        probate
        agreements_executed_before_2020
        all_case_law_not_expressly_imported
    }

    source CaliforniaUPAA {
        kind statute
        authority CaliforniaLegislature
        citation "Cal. Fam. Code §§ 1610-1617"
        artifact "sources/ca-family-1610-1617.txt"
        retrieved_at 2026-08-23T12:00:00-07:00
        provision_intervals from "sources/ca-family-1610-1617.manifest.json"
    }

    source Agreement {
        kind private_instrument
        authority {Ava, Noah}
        artifact "sources/ava-noah-prenup.txt"
    }

    entity Ava : NaturalPerson
    entity Noah : NaturalPerson
    entity ANP : PremaritalAgreement

    record_type FinancialDisclosureSchedule {
        owner: NaturalPerson
        assets: FiniteSet<DisclosedAsset>
        obligations: FiniteSet<DisclosedObligation>
        delivered_to: NaturalPerson
        delivered_at: Time
    }

    proposition Married(a: NaturalPerson, b: NaturalPerson)
    proposition ProspectiveSpouses(
        a: NaturalPerson,
        b: NaturalPerson,
        at: Time
    )
    proposition ExecutedVoluntarily(
        agreement: PremaritalAgreement,
        party: NaturalPerson
    )
    proposition EnforceableAgainst(
        agreement: PremaritalAgreement,
        party: NaturalPerson,
        provision: Provision,
        proceeding: Proceeding
    )

    legal_act ExecutePrenup(agreement: PremaritalAgreement) {
        performers {Ava, Noah}
        validity requires operative ProspectiveSpouses(
            Ava,
            Noah,
            execution_time
        ) in PrenupExecution
        validity requires Written(agreement)
        validity requires SignedBy(agreement, Ava)
        validity requires SignedBy(agreement, Noah)
        effect establish Executed(agreement)
        source CaliforniaUPAA.section("1611")
    }

    rule EffectiveUponMarriage : constitutive
        from CaliforniaUPAA.section("1613")
    {
        when effective ExecutePrenup(ANP)
          and operative Married(Ava, Noah)
        then establish Effective(ANP)
    }

    clause SeparateProperty(property: Asset, owner: NaturalPerson)
        from Agreement.clause("3")
    {
        when operative Effective(ANP) in MaritalPropertyRegime
        then purport_to establish ClassifiedAsSeparate(property, owner)
        enforcement requires PrenupEnforceability(
            against = party_opposing_classification,
            provision = this,
            case = current_proceeding
        )
        subject_to loaded_mandatory_law
    }

    clause SpousalSupportWaiver
        from Agreement.clause("8")
    {
        purports_to establish Waived(SpousalSupportClaim)
        subject_to CaliforniaUPAA.section("1612(c)")
        enforcement requires Determine
    }

    clause ChildSupportWaiver
        from Agreement.clause("9")
    {
        purports_to establish Waived(ChildSupportClaim)
        subject_to CaliforniaUPAA.section("1612(b)")
    }

    conflict_doctrine ChildSupportCannotBeAdverselyAffected
        from CaliforniaUPAA.section("1612(b)")
    {
        when ChildSupportWaiver adversely_affects ChildSupportRight
        then defeat ChildSupportWaiver as_to ChildSupportRight
        reason MandatoryStatutoryLimit
    }

    judgment PrenupVoluntariness(
        against: NaturalPerson,
        case: Proceeding
    )
    decides ExecutedVoluntarily(ANP, against)
        from CaliforniaUPAA.section("1615")
    {
        authority CourtWithJurisdiction(case)

        burden_of_persuasion {
            bearer against
            issue NotVoluntary(ANP, against)
            source CaliforniaUPAA.section("1615(a)(1)")
        }

        court_finding form written_or_on_record
        court_finding requires
            IndependentCounselAtSigning(against)
            or {
                AdvisedToSeekIndependentCounselAtLeast(
                    7 calendar_days_before_signing,
                    against
                )
                and SeparateWrittenCounselWaiverAfterAdvisement(against)
            }

        court_finding requires
            FinalAgreementPresentedAtLeast(7 calendar_days_before_signing)

        when operative Unrepresented(against) in case:
            court_finding requires WrittenExplanationOfRights(
                against,
                delivered_before_signing = true
            )
            court_finding requires LanguageProficiency(against)
            court_finding requires SignedReceiptOfExplanation(
                against,
                identifies_explainer = true
            )

        court_finding requires no established {
            Duress
            Fraud
            UndueInfluence
            LackOfCapacity
        }

        court may_consider OtherRelevantFactors
        otherwise not_established
    }

    judgment PrenupEnforceability(
        against: NaturalPerson,
        provision: Provision,
        case: Proceeding
    )
    decides EnforceableAgainst(ANP, against, provision, case)
        from CaliforniaUPAA.sections("1612(c)", "1615")
    {
        authority CourtWithJurisdiction(case)
        record requires ExecutionRecord(ANP)
        record may_include DisclosureRecord(ANP, against)
        record may_include CounselAndWaiverRecord(ANP, against)

        burden_of_persuasion {
            bearer against
            issue UnconscionableWithDisclosureFailures(ANP, against)
            source CaliforniaUPAA.section("1615(a)(2)")
        }

        reject when determination PrenupVoluntariness(against, case)
            is NotEstablished

        reject when established UnconscionableAtExecution(ANP)
          and established NoFairReasonableFullDisclosure(ANP, against)
          and established NoValidDisclosureWaiver(ANP, against)
          and established NoAdequateKnowledge(ANP, against)

        for SpousalSupportWaiver:
            reject when established NoIndependentCounselAtSigning(against)
            reject when established UnconscionableAtEnforcement(
                provision,
                case
            )

        otherwise decide under this fixed source_snapshot
        review under ApplicableAppellateStandard
    }

    legal_act AmendOrRevokePrenup(change: WrittenAgreement) {
        performers {Ava, Noah}
        active_while operative Married(Ava, Noah)
        validity requires SignedBy(change, Ava)
        validity requires SignedBy(change, Noah)
        effect establish AgreementChangedBy(ANP, change)
        source CaliforniaUPAA.section("1614")
    }

    query property_result(asset: Asset, case: Proceeding)
        -> PropertyClassification
        ! {Observe, Determine, Interpret}
    {
        goal EvaluateClause {
            clause SeparateProperty(
                asset,
                case_input<NaturalPerson>("asserted_owner")
            )
            context case
            result property_classification(asset, case)
        }
    }

    query provision_result(
        provision: ClauseRef,
        against: NaturalPerson,
        case: Proceeding
    )
        -> EnforcementResult
        ! {Observe, Determine, Interpret}
    {
        goal EvaluateClause {
            clause provision
            context case
            result enforcement_result(
                agreement = ANP,
                against = against,
                clause = provision,
                proceeding = case
            )
        }
    }

    verify AgreementSafety {
        assert always
            not EffectiveAdverseEffect(ANP, ChildSupportRight)

        assert every ScheduledAsset
            has disclosure_source_span

        assert SpousalSupportWaiver
            is never treated automatic
    }
}

The ProspectiveSpouses guard is legally material. Without it, the program could take a new agreement signed after marriage and incorrectly route it through the rule that makes a premarital agreement effective upon marriage. A post-marriage amendment or revocation follows the separately modeled section 1614 act instead.

The fixture is useful only if it produces visibly different results for different legal dependencies. With the agreement and marriage established, the sourced mandatory-law doctrine can prevent the child-support waiver's adverse effect without asking a court to make the agreement enforceable. The spousal-support waiver cannot be treated the same way:

$ fidryn run ava-noah.fidryn \
    --query provision_result \
    --arg 'provision=Examples.AvaNoahPrenup@0.1.0::ChildSupportWaiver()' \
    --arg against=Ava \
    --case divorce-record.json \
    --valid-at 2034-03-01T09:00:00-08:00 \
    --known-at 2034-03-01T09:00:00-08:00

Determinate {
    value: PreventedAsTo(
        ChildSupportRight,
        ChildSupportCannotBeAdverselyAffected
    )
    convergence_certificate: none
    ignored_open_issues: {}
    trace: trace:CA-44
}

$ fidryn run ava-noah.fidryn \
    --query provision_result \
    --arg 'provision=Examples.AvaNoahPrenup@0.1.0::SpousalSupportWaiver()' \
    --arg against=Ava \
    --case divorce-record-without-enforceability-order.json \
    --valid-at 2034-03-01T09:00:00-08:00 \
    --known-at 2034-03-01T09:00:00-08:00

Suspended {
    requests: {
        NeedJudgment {
            issue: EnforceableAgainst(
                ANP,
                Ava,
                SpousalSupportWaiver,
                DivorceCase
            )
            protocol: PrenupEnforceability
        }
    }
    trace: trace:CA-61
}

The CLI spelling module@version::Clause(arguments) is the canonical serialized ClauseRef. The runner resolves it to the ModuleId, ClauseId, typed arguments, and content digest in the already authenticated compiled bundle. An unknown module, different version, stale digest, wrong arity, or ill-typed argument is E431 InvalidClauseReference; the CLI never turns the characters ChildSupportWaiver into a clause by an ambient name lookup.

The crucial result type is not ValidPrenup. A court may enforce one provision and not another. A challenge may be against one party in one proceeding. Unconscionability can be evaluated at different times for different statutory purposes. Choice of law and the enforcing forum may change the source bundle. Fidryn therefore asks a scoped question: EnforceableAgainst(agreement, party, provision, proceeding).

Example 3: reconstruct a bounded slice of federal FOIA

“Encode federal law” is too broad to be a meaningful task. The United States Code is a codification of federal statutes, not the complete body of federal law. A useful program states the question and loads a dated source bundle.

This example reconstructs only the request-processing spine of the Freedom of Information Act: a proper request, the response deadline, asserted exemptions, foreseeable harm, segregability, an adverse determination, and review. Its statutory anchor is the Office of the Law Revision Counsel's preliminary text of 5 U.S.C. § 552, and the Department of Justice maintains a sectioned, explanatory FOIA Guide. Agency regulations and controlling decisions must be separate imports; the guide is not a substitute for them.

module US.Federal.FOIA.RequestProcessing version "0.1.0" {
    jurisdiction UnitedStates.Federal
    source_snapshot "2026-08-23-foia-bounded"
    source_manifest "sources/foia-bounded.manifest.json"
    effective_at 2026-08-23
    recorded_at 2026-08-23T12:00:00-04:00

    outside_scope {
        proactive_disclosure
        fee_waiver_merits
        every_exemption_element
        ten_day_component_rerouting_rule
        time_limit_tolling
        unusual_circumstances_extensions
        PrivacyAct_interaction
        complete_appeal_and_litigation_procedure
        non_withholding_adverse_determination_categories
        sources_not_listed_in_this_bundle
    }

    source FOIAStatute {
        kind statute
        authority UnitedStatesCongress
        citation "5 U.S.C. § 552"
        artifact "sources/usc-5-552.txt"
        digest required_in source_manifest
        effective according_to source_manifest
    }

    import Agency.FOIARegulations version "fixture-2026-08-23" {
        digest required_in source_manifest
    }
    import US.Federal.Cases.FOIA version "fixture-2026-08-23" {
        digest required_in source_manifest
    }
    import US.Federal.Calendars version "2026"

    entity Requester : LegalPerson
    entity Agency : FederalAgency
    office FOIAOfficeOf(agency: FederalAgency)
        occupied_by AgencyComponent
    {
        competence {
            DetermineRequestSufficiency
            DecideRecordDisposition
        }
    }

    record_type FOIARequest {
        requester: LegalPerson
        target_agency: FederalAgency
        description: String
        requested_format: MediaType
        submitted_at: Time
    }

    proposition ProperRequest(request: FOIARequest)
    proposition Responsive(part: RecordPart, request: FOIARequest)
    proposition ExemptionApplies(part: RecordPart, exemption: FOIAExemption)
    proposition ForeseeableHarm(
        part: RecordPart,
        protected_interest: LegalInterest
    )
    proposition DeterminationIssued(
        request: FOIARequest,
        disposition: FOIADisposition
    )
    proposition AdverseDetermination(
        request: FOIARequest,
        disposition: FOIADisposition
    )

    legal_act SubmitFOIARequest(request: FOIARequest) {
        performer request.requester
        recipient FOIAOfficeOf(request.target_agency)
        effect establish Received(request, received_time)
        source FOIAStatute.section("552(a)(3)(A)")
    }

    judgment RequestSufficiency(request: FOIARequest)
        decides ProperRequest(request)
        from FOIAStatute.section("552(a)(3)(A)")
    {
        authority occupant FOIAOfficeOf(request.target_agency)
        record requires RequestRecord(request)
        establish when reasonably_describes_records(request)
          and conforms_to_published_agency_rules(request)

        on unresolved
            follow Agency.FOIARegulations.RequestClarification
    }

    duty InitialDetermination(request: FOIARequest) {
        bearer FOIAOfficeOf(request.target_agency)
        claimant request.requester
        attaches when operative ProperRequest(request)
        due 20 counted_days after received_by_appropriate_component(request)
        exclude_from_count {
            Saturday
            Sunday
            FederalLegalPublicHoliday
        }
        content DetermineComplianceAndNotify(request)
        source FOIAStatute.section("552(a)(6)(A)(i)")
    }

    type WithholdingBasis =
        HarmBased {
            exemption: FOIAExemption
            protected_interest: LegalInterest
        }
      | ValidExemption3 {
            exemption: Exemption3
            qualifying_statute: SourceRef
        }
      | OtherwiseProhibitedByLaw {
            prohibiting_source: SourceRef
        }

    record_type Withholding {
        part: RecordPart
        basis: WithholdingBasis
    }

    record_type FOIADisposition {
        released: FiniteSet<RecordPart>
        withheld: FiniteSet<Withholding>
    }

    decision ProcessResponsiveRecord(
        request: FOIARequest,
        record: AgencyRecord,
        proposed: FOIADisposition
    ) -> FOIADisposition {
        authority occupant FOIAOfficeOf(request.target_agency)
        options lawful_partitions(record.parts)

        for each withholding in proposed.withheld:
            require operative Responsive(withholding.part, request)
            record requires CitedWithholdingBasis(withholding)

            when withholding.basis is HarmBased(exemption, interest):
                require operative ExemptionApplies(
                    withholding.part,
                    exemption
                )
                require operative ForeseeableHarm(
                    withholding.part,
                    interest
                )
                record requires HarmAnalysis(withholding)

            when withholding.basis is ValidExemption3(exemption, statute):
                require operative ExemptionApplies(
                    withholding.part,
                    exemption
                )
                require operative QualifyingExemption3Statute(statute)
                record requires ProhibitingLawTrace(withholding, statute)

            when withholding.basis is OtherwiseProhibitedByLaw(source):
                require operative DisclosureProhibitedByLaw(
                    withholding.part,
                    source
                )
                record requires ProhibitingLawTrace(withholding, source)

        require every reasonably_segregable_nonexempt_part(record)
            is in proposed.released

        record requires SegregabilityAnalysis(record)
            when proposed.withheld is nonempty

        returns proposed when every requirement above is satisfied

        source {
            FOIAStatute.section("552(a)(8)(A)")
            FOIAStatute.section("552(b)")
        }
    }

    legal_act IssueFOIADetermination(
        request: FOIARequest,
        disposition: FOIADisposition
    ) {
        performer occupant FOIAOfficeOf(request.target_agency)
        validity requires operative ProperRequest(request)
            in FOIARequestProcessing
        effect establish DeterminationIssued(request, disposition)
        source FOIAStatute.section("552(a)(6)(A)(i)")
    }

    rule EveryDeterminationTriggersReasonsAndAssistance(
        request: FOIARequest,
        disposition: FOIADisposition
    ) : prescriptive
        from FOIAStatute.section("552(a)(6)(A)(i)")
    {
        when effective IssueFOIADetermination(request, disposition)
        then create Duty(
            bearer = Agency,
            claimant = request.requester,
            content = GiveNotice(
                reasons_for(disposition),
                right_to_seek_assistance_from(FOIAPublicLiaison)
            )
        )
    }

    rule WithholdingDispositionIsAdverse(
        request: FOIARequest,
        disposition: FOIADisposition
    ) : derive
        from FOIAStatute.section("552(a)(6)(A)(i)(III)")
    {
        when disposition.withheld is nonempty
        then derive AdverseDetermination(request, disposition)
    }

    rule AdverseDeterminationTriggersReviewNotice(
        request: FOIARequest,
        disposition: FOIADisposition
    ) : prescriptive
        from FOIAStatute.section("552(a)(6)(A)(i)(III)")
    {
        when effective IssueFOIADetermination(request, disposition)
          and derived AdverseDetermination(request, disposition)
        then create Duty(
            bearer = Agency,
            claimant = request.requester,
            content = GiveNotice(
                appeal_procedure,
                appeal_deadline_at_least(90 days),
                dispute_resolution_available_from {
                    FOIAPublicLiaison,
                    OGIS
                }
            )
        )
    }

    query disposition(request: FOIARequest)
        -> FOIADisposition
        ! {Observe, Determine, Interpret}
    {
        goal RunDecision {
            decision ProcessResponsiveRecord
            arguments {
                request
                case_input<AgencyRecord>("responsive_record")
                case_input<FOIADisposition>("proposed_disposition")
            }
            result declared_result
        }
    }

    verify ProcessingIntegrity {
        assert no withholding
            without CitedWithholdingBasis(withholding)

        assert every responsive part is exactly_one_of {
            released
            withheld_with_valid_basis_and_required_showing
        }

        assert every reasonably_segregable_nonexempt_part is released
        assert every disposition with withheld parts
            has SegregabilityAnalysis
        assert every determination creates reasons_and_liaison_notice
        assert every adverse_determination creates
            appeal_and_dispute_resolution_notice
    }
}

Two small details prevent the fixture from becoming a misleading checklist. The statutory clock counts twenty days while excluding Saturdays, Sundays, and legal public holidays; a generic business-day calendar could exclude more. And every determination notice carries reasons plus the right to seek Public Liaison assistance, while the appeal and OGIS dispute-resolution material is added for an adverse determination. This bounded record-disposition fixture derives adversity from a nonempty withholding; a production module must import the other adverse categories rather than pretending that no-record, format, fee, fee-waiver, expedited-processing, and request-description decisions do not exist.

Suppose the agency proposes to withhold part 17 under Exemption 5, cites the exemption, but the case record contains neither the required harm analysis nor a segregability analysis. The evaluator does not convert those omissions into false, and it does not approve the withholding because an exemption number is present:

$ fidryn run foia.fidryn \
    --query disposition \
    --case proposed-exemption-5-withholding.json \
    --valid-at 2026-08-23T12:00:00-04:00 \
    --known-at 2026-08-23T12:00:00-04:00

Suspended {
    requests: {
        NeedEvidence {
            issue: ForeseeableHarm(Part17, DeliberativeProcessInterest)
            schema: HarmAnalysis
        }
        NeedEvidence {
            issue: SegregabilityEstablished(Record9)
            schema: SegregabilityAnalysis
        }
    }
    trace: trace:FOIA-88
}

The program does not claim to contain “FOIA.” It contains a bounded, dated reconstruction for specified queries. A real source manifest would record each artifact's issuer, citation, effective interval, retrieval time, digest, amendment lineage, and whether it is binding, controlling, persuasive, or merely explanatory. Changing an agency regulation or controlling case produces a new source snapshot and a semantic diff; it does not silently mutate yesterday's result.

Example 4: form a Massachusetts LLC

An LLC formation workflow demonstrates why legal acts cannot be ordinary object construction. A signed operating agreement can allocate private rights without being the statutory filing that creates the entity. A name search is not a filing. Sending a certificate to a web endpoint is not, by itself, proof that filing occurred. An EIN and federal tax classification are downstream federal matters, not the constitutive state-law event.

For this example, Massachusetts law requires a certificate of organization with specified information and provides that the LLC is formed at filing, or a later stated effective date, if there has been substantial compliance. It also requires a Commonwealth office and resident agent and an annual report. The relevant current sources are M.G.L. c. 156C, § 5, § 12, and the Secretary of the Commonwealth's LLC filing instructions.

module Examples.FormHarborRoboticsLLC version "0.1.0" {
    jurisdiction Massachusetts
    source_snapshot "2026-08-23-ma-llc"
    source_manifest "sources/ma-llc.manifest.json"
    effective_at 2026-08-23
    recorded_at 2026-08-23T12:00:00-04:00

    outside_scope {
        professional_LLC_requirements
        securities_law
        tax_elections
        licensing
        employment
        foreign_qualification
    }

    source MassachusettsLLCAct {
        kind statute
        authority MassachusettsGeneralCourt
        citation "M.G.L. c. 156C"
        artifact "sources/ma-c156c.txt"
    }

    source SecretaryInstructions {
        kind administrative_material
        authority MassachusettsSecretaryOfCommonwealth
        artifact "sources/ma-llc-filing-instructions.html"
        retrieved_at 2026-08-23T12:00:00-04:00
    }

    entity Bryan : NaturalPerson
    entity ResidentAgentCo : DomesticCorporation
    entity HarborRobotics : ProposedLLC

    record_type CertificateOfOrganization {
        name: LLCName
        commonwealth_office: StreetAddress
        resident_agent: LegalPerson
        resident_agent_address: StreetAddress
        resident_agent_consent: SignedConsent
        dissolution_date: Option<Date>
        managers: FiniteSet<NamedPersonAddress>
        authorized_filers: FiniteSet<NamedPersonAddress>
        real_property_signers: FiniteSet<NamedPersonAddress>
        business_character: String
        requested_effective_time: Option<Time>
        federal_ein_if_available: Option<EIN>
        executed_by: NonEmptySet<LegalPerson>
    }

    record_type OfficialFilingRecord {
        filing_id: String
        recorded_by: Authority
        filed_at: Time
        effective_at: Time
        observed_at: Time
        source_document: CertificateOfOrganization
        source_digest: Digest
    }

    proposition NameConforms(name: LLCName)
    proposition Filed(
        certificate: CertificateOfOrganization,
        filed_at: Time,
        effective_at: Time
    )
    proposition SubstantiallyComplies(
        certificate: CertificateOfOrganization,
        source: SourceRef
    )

    observation OfficialFilingObservation(
        filing: OfficialFilingRecord
    )
    establishes Filed(
        filing.source_document,
        filing.filed_at,
        filing.effective_at
    )
        from {
            MassachusettsLLCAct.section("12(b)")
            SecretaryInstructions.section("Certificates of Organization")
        }
    {
        authenticate filing.recorded_by ==
            MassachusettsSecretaryOfCommonwealth.CorporationsDivision
        authenticate digest(filing.source_document) == filing.source_digest
        require filing.effective_at == later_effective_time_or(
            filing.source_document.requested_effective_time,
            filing.filed_at
        )
    }

    judgment FormationCompliance(
        certificate: CertificateOfOrganization
    )
    decides SubstantiallyComplies(certificate, MassachusettsLLCAct)
        from MassachusettsLLCAct.section("12(b)")
    {
        authority CompetentFormationAuthority
        record requires CertificateFieldRecord(certificate)
        record requires OfficialFilingRecordFor(certificate)
        standard SubstantialCompliance
        review by CourtWithEntityJurisdiction under ApplicableStandard
    }

    query filing_readiness(certificate: CertificateOfOrganization)
        -> FilingPacket
        ! {Observe, Determine}
    {
        require certificate.name has_llc_designator
        require operative NameConforms(certificate.name)
            using Observe
        require in_commonwealth(certificate.commonwealth_office)
        require eligible_resident_agent(certificate.resident_agent)
        require valid_service_address(certificate.resident_agent_address)
        require valid(certificate.resident_agent_consent)
        require every certificate.executed_by
            is authorized_to_execute(certificate)
        require certificate.managers is nonempty
            or certificate.authorized_filers is nonempty
        require every named_person_address is complete
        require not_blank(certificate.business_character)

        return FilingPacket {
            certificate
            fee: current_fee(
                CertificateOfOrganization,
                SecretaryInstructions
            )
            destination:
                MassachusettsSecretaryOfCommonwealth.CorporationsDivision
        }
    }

    legal_act SubmitCertificate(
        organizer: NaturalPerson,
        packet: FilingPacket
    ) {
        performer organizer
        recipient MassachusettsSecretaryOfCommonwealth.CorporationsDivision
        physical_effect TransmissionAttempted(packet)
        does_not_establish Filed(packet.certificate, _, _)
        source SecretaryInstructions.section("Certificates of Organization")
    }

    rule FormationByFiledCertificate(
        certificate: CertificateOfOrganization,
        filed_at: Time,
        effective_at: Time
    ) : constitutive
        from MassachusettsLLCAct.section("12")
    {
        when operative Filed(certificate, filed_at, effective_at)
            in EntityFormation(HarborRobotics)
          and effective_at == later_effective_time_or(
                certificate.requested_effective_time,
                filed_at
              )
          and operative SubstantiallyComplies(
                certificate,
                MassachusettsLLCAct
              )
            in EntityFormation(HarborRobotics)

        then establish FormedLLC(HarborRobotics)
            valid_time [effective_at, +inf)
            record_time [max_record_time(guard_trace), +inf)
    }

    legal_act ExecuteOperatingAgreement(agreement: OperatingAgreement) {
        performers MembersNamedBy(agreement)
        effect establish PrivateGovernanceTerms(
            HarborRobotics,
            agreement
        )
        does_not_establish FormedLLC(HarborRobotics)
        source agreement
    }

    duty MaintainCommonwealthOfficeAndAgent {
        bearer HarborRobotics
        attaches when operative FormedLLC(HarborRobotics)
        content Maintain(OfficeInCommonwealth)
            and Maintain(ResidentAgentForService)
        source MassachusettsLLCAct.section("5")
    }

    duty FileAnnualReport {
        bearer HarborRobotics
        attaches when operative FormedLLC(HarborRobotics)
        due on_or_before every anniversary_of(original_filing_date)
        content File(AnnualReportWithRequiredInformation)
        source {
            MassachusettsLLCAct.section("12(c)")
            SecretaryInstructions.section("Annual Reports")
        }
    }

    query entity_status()
        -> EntityStatus
        ! {Observe, Determine}
    {
        goal StatusOf {
            status FormedLLC(HarborRobotics)
            when_present FormedLLC(HarborRobotics)
            when_closed_absent NotFormedLLC(HarborRobotics)
        }
    }

    verify FormationIntegrity {
        for every operative Filed(certificate, filed_at, effective_at):
            assert not operative FormedLLC(HarborRobotics)
                before effective_at

        assert no FilingPacket
            without ResidentAgentConsent

        assert Effective(ExecuteOperatingAgreement)
            does_not_imply FormedLLC(HarborRobotics)

        assert operative FormedLLC(HarborRobotics)
            implies scheduled FileAnnualReport
    }
}

The constitutive rule depends on the statutory facts Filed and SubstantiallyComplies, not on possession of a receipt or prior agency “acceptance.” An official record is evidence by which the CaseFile handler may establish Filed; it is not an extra formation element. Likewise, the compliance protocol lets a particular query establish the open-textured statutory condition without claiming the determination created that condition. If the packet has merely been transmitted, the correct case-file result is suspension rather than either Formed or NotFormed. Once authenticated filing evidence and a scoped substantial-compliance determination are present, they support the constitutive result with the statute's effective time:

$ fidryn run harbor-robotics.fidryn \
    --query entity_status \
    --case transmitted-without-official-record.json \
    --valid-at 2026-09-01T10:00:00-04:00 \
    --known-at 2026-08-28T10:00:00-04:00

Suspended {
    requests: {
        NeedEvidence {
            issue: Filed(HarborRoboticsCertificate, _, _)
            schema: OfficialFilingRecord
        }
    }
    trace: trace:MA-31
}

$ fidryn run harbor-robotics.fidryn \
    --query entity_status \
    --case official-filing-record.json \
    --valid-at 2026-09-01T10:00:00-04:00 \
    --known-at 2026-09-01T10:00:00-04:00

Determinate {
    value: FormedLLC(HarborRobotics)
    valid_time: [2026-09-01T09:00:00-04:00, +inf)
    record_time: [2026-08-28T14:12:00-04:00, +inf)
    convergence_certificate: none
    ignored_open_issues: {}
    trace: trace:MA-52
}

The reference implementation should generate the packet and checklist, then wait for authenticated evidence of filing. It should not automate a real filing in v0.1. External submission involves credentials, fees, terms of service, retries, idempotency, and the risk of creating an entity accidentally; that belongs behind an audited capability adapter later.

The source snapshot also prevents stale checklist logic. For example, older U.S. LLC workflows may still list a domestic beneficial-ownership report as a universal federal step. FinCEN's current BOI page states that U.S. companies are exempt under the final rule effective August 14, 2026. Fidryn should represent that as a dated federal module, not a timeless comment embedded in a Massachusetts formation wizard.

What formal verification can honestly promise

The existence of judgment effects does not make verification pointless. It changes the quantifiers and the properties.

Strong candidates

With fixed source modules and explicit closure assumptions, a compiler or verifier can plausibly detect:

• ill-typed people, offices, assets, currencies, dates, and legal effects;
• exercises of power by someone who does not hold it;
• institutional effects with no constitutive source;
• role vacancies with no appointment path;
• unreachable clauses and shadowed rules;
• contradictory duties that attach simultaneously;
• duties with impossible deadlines or no discharge behavior;
• beneficiary branches with no terminal disposition;
• unaccounted title or fractional interests;
• inconsistent source-applicability declarations;
• semantic regressions across amendments; and
• bounded temporal safety and liveness failures.

Conditional candidates

Other properties become formal only after importing a determination or declaring an interpretation:

• whether a creditor's claim is enforceable;
• whether a nominee is eligible;
• whether an amendment satisfied a disputed formality;
• whether funds are sufficient after claims, reserves, and taxes;
• which persons are descendants for a particular distribution; and
• which version of an external statute governs.

The result should name the dependency. “Proved under Determination D17 and Source Snapshot V4” is useful. “Proved” without the qualifiers is not.

Structured but generally not settled by the language

The language can expose the authorized process around reasonableness, good faith, credibility, materiality, best interests, settlor intent, abuse of discretion, and the weight of evidence. It should not claim that a type checker has decided those standards.

It may nevertheless prove that:

• the correct actor made the decision while holding the relevant office;
• mandatory considerations were part of the record;
• forbidden considerations were not used in the stated reasons;
• the outcome stayed within a legally defined choice space;
• notice, reasons, and record requirements were satisfied;
• review was available in the correct forum; and
• a safety property holds under every legally admissible discretionary result.

Verification declarations make each quantifier visible instead of hiding several axes inside one mode enum:

interpretations:
    concrete
  | selected(InterpretationId)
  | all_admissible

judgments:
    case_record
  | selected(DeterminationId)
  | all_lawful

choices:
    case_record
  | selected(DecisionId)
  | all_lawful

scope:
    concrete
  | bounded(Bounds)

assumptions:
    FiniteSet<ExplicitAssumption>

For example:

verify TrusteeContinuity {
    interpretations all_admissible
    judgments all_lawful
    choices all_lawful
    scope bounded {persons: 8, events: 40, time_points: 80}

    assuming fair_response(CourtAppointmentProcedure)

    assert always
        occupied(TrusteeOf(BRT))
        or active CourtAppointmentProcedure(BRT)
}

The displayed assertion is a safety invariant: every vacancy has an active appointment process. It permits that process to remain pending forever. Its proof should therefore be checked without using fairness to exclude an inconvenient finite prefix. A separate liveness target is

Here $\mathbf G$ means always and $\mathbf F$ means eventually. This target needs assumptions that a qualified appointee remains available and that enabled appointment steps eventually occur. Fairness alone cannot create an eligible trustee or set a maximum response time. On a bounded trace, an unfinished appointment at the horizon is inconclusive unless the specification adds a response deadline or the checker explores all reachable cycles under a stated infinite-trace semantics. These are separate proof obligations; see Lamport's formal account of safety, liveness, and fairness.

Closed-world assumptions need similar treatment. A finite database of descendants is not proof that no other descendant exists. Universal claims should require a closure certificate or be labeled bounded to the enumerated model.

The formal source is not automatically the law

The compiler metaphor also needs discipline. There are three possible relationships between a formal specification and conventional legal prose.

1. The formal source controls. Generated prose is a view of the operative formal instrument. This resembles a conventional compiler, but it requires legal recognition of the language and a rule for resolving implementation or rendering defects.
2. Both control. Formal and prose representations are jointly operative. This creates a new conflict problem whenever they diverge.
3. The prose controls. The formal model is a drafting artifact, executable interpretation, test suite, and possible evidence of intent, but not the ultimate source of legal meaning.

The third regime is the plausible starting point. It is also the least like a compiler in the strong semantic-preservation sense. A court may assign generated prose a meaning that differs from the formal model. The OECD's 2026 consultation takes that boundary explicitly: authoritative legal text remains legally binding; Law as Code does not change interpretation or institutional responsibilities and does not decide individual cases; interpretive, discretionary, and evaluative elements remain visible rather than being silently converted into deterministic rules.

The initial toolchain should therefore produce traceable pairs, not claim semantic identity:

structured legal intent
        -> canonical legal IR
        -> static analysis and open-issue report
        -> constrained prose templates
        -> conventional legal instrument

with:

formal clause <-> generated prose source map
formal clause <-> governing authority map
version <-> semantic diff
open judgment <-> responsible protocol

Every generated sentence should map back to semantic constructs. Free-form prose should be allowed as an explicitly opaque provision whose automation status is noncomputable and whose interpretation protocol is named. Opaque prose is not a failure. Hiding it inside a Boolean predicate is.

An unconstrained text generator can propose wording, tests, or candidate mappings. Its output remains an untrusted draft. Fluency is not a semantic-preservation proof.

Why this is not simply another rules language

“Law as executable rules” is not a novelty claim worth making. The nearby systems are too substantial for that.

These systems do not solve the same problem, and their semantics cannot simply be unioned. Nearly every noun in “a typed, temporal, defeasible language for legal rules, rights, obligations, powers, provenance, and verification” already belongs to an existing research program.

One scope note matters for L4. Its research line has explored defeasible-rule translations, but the current default-reasoning documentation describes UNLESS classically and states that L4 does not infer priorities or retract conclusions. Current implementation claims should not be blended with the separate 2022 SMT/ASP study.

Fidryn's possible contribution is at the seam: treating each unresolved legal dependency as a typed, scoped operation while giving any proposed answer authority, record, purpose, time, finality, review, and constitutive consequences. That is a hypothesis about integration, not yet a proven novelty claim. The benchmark must still show that these properties cannot be obtained cleanly as a library or disciplined encoding in an existing system.

The research argument is complete at this point. The remainder is a normative v0.1 design contract for someone implementing the reference interpreter, followed by the benchmark and failure conditions. General readers can skip to the conclusion; builders should treat unresolved syntax choices as milestone-one work, not as permission to change the semantics.

Part III: Fidryn v0.1 implementation contract

The one-screen contract is:

When prose, an example, and Core disagree, Core plus the acceptance tests control the reference implementation. When surface syntax remains underspecified, milestone one must resolve it in grammar.ebnf and update every fixture before semantic work proceeds.

The first implementation is a reference interpreter, not a full legal operating system. V0.1 must be small enough that every evaluator step can be inspected and every completion can be enumerated in tests.

Scope and explicit deferrals

V0.1 supports:

• finite, named entities and finite collections;
• one fixed jurisdiction and authenticated source snapshot per run;
• sources, imports, offices, propositions, record types, evidence, and closure records;
• constitutive and prescriptive rules;
• Hohfeldian positions;
• legal acts whose validity, effect, and compliance are evaluated separately;
• Observe, Determine, Choose, and Interpret effects;
• case-file, scenario, exploration, and skeptical handlers;
• bitemporal queries over discrete time points;
• one finite interpretation family;
• named, nonrecursive conflict doctrines;
• deterministic trace and source-map output; and
• bounded safety and liveness verification.

V0.1 explicitly defers general court procedure, unrestricted first-order quantification, arbitrary user-defined effects, live government filing, tax engines, a complete source hierarchy, open-ended case-law argumentation, unconstrained natural-language generation, and general recursion. ResolveNormConflict and SelectApplicableLaw exist in the language design, but the first interpreter accepts a fixed source selection and returns an unresolved NormConflict rather than running a general conflict oracle.

That boundary is a feature. A prototype that claims to handle the whole legal system is not testable enough to teach us whether the kernel works.

Surface syntax and grammar boundary

Fidryn source is UTF-8. Identifiers in v0.1 are ASCII letters, digits, and underscores, with an initial letter or underscore. Strings use JSON escapes. // begins a line comment and /// begins documentation attached to the next declaration. Block comments are deferred.

The formatter uses braces and newline terminators. The lexer inserts a statement terminator at a newline when delimiter depth is zero, the previous token can end a statement, and the next token is not a continuation such as and, or, where, then, else, ., or ,. An explicit ; is always accepted. This makes the examples above the required parser fixtures without making the grammar indentation-sensitive; their validity is established only when milestone one's closed body productions accept all four modules.

File            ::= Module EOF

Module          ::= "module" QName "version" String "{" ModuleItem* "}"

ModuleItem      ::= HeaderDecl
                  | SourceDecl
                  | ImportDecl
                  | EntityDecl
                  | TypeDecl
                  | RecordTypeDecl
                  | OfficeDecl
                  | PropositionDecl
                  | ObservationDecl
                  | NominationDecl
                  | FunctionDecl
                  | RuleDecl
                  | PowerDecl
                  | DutyDecl
                  | JudgmentDecl
                  | DecisionDecl
                  | LegalActDecl
                  | ClauseDecl
                  | InterpretationDecl
                  | ConflictDoctrineDecl
                  | QueryDecl
                  | ScenarioDecl
                  | VerifyDecl

HeaderDecl      ::= "jurisdiction" QName End
                  | "source_snapshot" String End
                  | "source_manifest" String End
                  | "effective_at" Date End
                  | "recorded_at" Time End
                  | "outside_scope" "{" QName* "}"

SourceDecl      ::= "source" Ident "{" SourceField* "}"
ImportDecl      ::= "import" QName "version" Value
                    ("{" ImportField* "}")? End
EntityDecl      ::= "entity" Ident ":" Type End
TypeDecl        ::= "type" Ident TypeParameters? "=" TypeBody
RecordTypeDecl  ::= ("record_type" | "evidence_type") Ident
                    "{" FieldDecl* "}"
OfficeDecl      ::= "office" Signature "occupied_by" Type
                    "{" OfficeField* "}"
PropositionDecl ::= "proposition" Signature End
ObservationDecl ::= "observation" Signature
                    "establishes" Expr SourceRef? Block
NominationDecl  ::= "nomination" Expr "for" Expr "rank" Int
                    SourceRef? End
FunctionDecl    ::= ("fn" | "calc") Signature "->" Type
                    EffectRow? Block
PowerDecl       ::= "power" Ident Signature? SourceRef? Block
DutyDecl        ::= "duty" Ident Signature? SourceRef? Block
ClauseDecl      ::= "clause" Ident Signature? SourceRef? Block
InterpretationDecl
                ::= "interpretation_family" Ident "for" Expr Block
ConflictDoctrineDecl
                ::= "conflict_doctrine" Ident SourceRef? Block

RuleDecl        ::= "rule" Ident ("(" ParameterList? ")")?
                    ":" RuleKind SourceRef?
                    "{" RuleStatement* "}"
RuleKind        ::= "derive" | "constitutive" | "prescriptive"

JudgmentDecl    ::= "judgment" Signature "decides" Expr SourceRef?
                    "{" JudgmentStatement* "}"
DecisionDecl    ::= "decision" Signature ("->" Type)?
                    "{" DecisionStatement* "}"
LegalActDecl    ::= "legal_act" Signature "{" ActStatement* "}"

QueryDecl       ::= "query" "automatic"? Signature
                    "->" Type EffectRow? Block
EffectRow       ::= "!" "{" EffectName ("," EffectName)* "}"

ScenarioDecl    ::= "scenario" Ident "{" ScenarioStatement* "}"
VerifyDecl      ::= "verify" Ident "{" VerifyStatement* "}"

Signature       ::= Ident "(" ParameterList? ")"
ParameterList   ::= Parameter ("," Parameter)*
Parameter       ::= Ident ":" Type
SourceRef       ::= "from" Expr

Expr            ::= literal
                  | QName
                  | Call
                  | UnaryExpr
                  | BinaryExpr
                  | SetExpr
                  | RecordExpr

End             ::= inserted-newline | ";"

The expression parser uses fixed precedence, from strongest to weakest: member access and calls; unary not; multiplication and division; addition and subtraction; comparisons; and; or; implication. Chained comparisons are rejected. Time literals use ISO 8601. Duration literals carry a calendar kind: 20 working_days is not the same type as 20 days. Money is written as USD(500.00), never as an untyped decimal.

This is a top-level grammar sketch, not yet a complete parser grammar: declaration-body nonterminals such as SourceField, RuleStatement, and JudgmentStatement still need closed productions. The first milestone must publish the complete grammar.ebnf, make all four modules parser goldens, and reject any syntax accepted only by ad hoc parsing. That work may clarify notation, but it may not change the Core operations or acceptance outcomes below.

The implementer does not have discretion to invent arbitrary body keys. The closed v0.1 body inventory is:

grammar.ebnf must give each row declaration-specific productions; there is no catch-all Ident Expr field statement. Unknown fields are parse or schema errors, not extension points. Parser work is the acceptance gate for semantic work: do not begin Core lowering until every code block labeled as a module parses losslessly and its formatted round trip is byte-stable apart from documented whitespace normalization.

The parser must retain every token, comment, and byte span in a lossless syntax tree. The typed AST may discard trivia, but source mapping and a future prose renderer depend on the lossless tree.

The type and effect system

The core judgment is:

meaning that expression $e$ has type $\tau$ and may perform the effects in row $\epsilon$. V0.1 effect rows are finite sets rather than row-polymorphic variables. Polymorphism can come later.

Primitive value types are:

Bool
Int
Decimal
String
Date
Time
Duration<Calendar>
Money<Currency>
Interval<Time>
Option<T>
FiniteSet<T>
NonEmptySet<T>
Map<K, V>

Nominal legal sorts include:

Prop
NaturalPerson
LegalPerson
LegalEntity
Trust
PremaritalAgreement
ProposedLLC
Asset
Office
Authority
Jurisdiction
SourceVersion
LegalContext
LegalAction
LegalEffect
Proceeding
RecordItem
Determination
Interpretation
ClauseRef

NaturalPerson <: LegalPerson and LegalEntity <: LegalPerson are ordinary nominal subtyping relations. TrusteeOf(BRT) is not a subtype of person; it is an Office, and Occupies(Bryan, TrusteeOf(BRT)) is a temporal legal relation. Power, institutional Competence, and delegated Authorization are distinct parameterized types. ClauseRef is an authenticated, module-qualified reference to one clause application; it carries the clause ID and checked arguments, not a free-form provision name or string.

Hohfeldian positions are canonical Core values:

type Position =
    Duty {
        bearer: LegalPersonRef
        claimant: LegalPersonRef
        content: NormContent
    }
  | Claim {
        claimant: LegalPersonRef
        bearer: LegalPersonRef
        content: NormContent
    }
  | Liberty {
        holder: LegalPersonRef
        against: LegalPersonRef
        content: NormContent
    }
  | NoRight {
        against: LegalPersonRef
        holder: LegalPersonRef
        content: NormContent
    }
  | Power {
        holder: LegalPersonRef
        subject: LegalSubjectRef
        effect: LegalEffect
    }
  | Liability {
        subject: LegalSubjectRef
        holder: LegalPersonRef
        effect: LegalEffect
    }
  | Immunity {
        holder: LegalPersonRef
        against: LegalPersonRef
        effect: LegalEffect
    }
  | Disability {
        against: LegalPersonRef
        holder: LegalPersonRef
        effect: LegalEffect
    }

Surface declarations may generate correlatives, but the elaborated IR records both. An unqualified Right is rejected because it does not say which jural relation is intended.

The key typing rules are operationally simple:

• a declared proposition application has type Prop, never Bool;
• only explicit operators such as operative(p, context), assumed(p, scenario), or determined(p, determination) may turn a proposition's status into a rule guard;
• calc functions must be total, effect-free, and terminating;
• a function's inferred effect set must be a subset of its declared effect row;
• a query declared automatic must have an empty open-legal-effect row;
• a query declares its domain result T and its open effects; the selected runner and handler lift evaluation into Outcome<T> exactly once;
• an observation maps one authenticated record schema to one proposition and may discharge Observe only after every validator succeeds;
• wildcard and binding terms are accepted only in checked proposition or status patterns, never in ordinary value expressions;
• only a constitutive rule, a competent institutional act, or a valid exercise of power may establish or terminate an institutional legal status;
• an office must be occupied before office-indexed power can be exercised;
• authority occupant Office resolves to the current officeholder only when the office declares competence for that operation in the loaded source snapshot;
• valid and record intervals must be well formed, and record time may not precede the system's receipt of the record;
• universal quantification over an external domain requires a closure record or is labeled bounded; and
• pure definitions and negative derivations must be stratified. General recursion is rejected in v0.1.

These rules are enforced before any solver runs. An SMT model is not allowed to repair an ill-typed legal program by finding a convenient interpretation.

The standard prelude defines all infrastructure types used by the evaluator, including TraceId, OpenIssue, ArgumentGraph, UnsatCore, SourceRef, LegalPersonRef, NormContent, PropTerm, PropPattern, LegalStatusPattern, LegalEffectPattern, and the Outcome family. Domain names such as FOIAExemption, CapacityPurpose, and PropertyClassification are not magical built-ins: each fixture must declare them or import them from a versioned profile module before it can become a parser and type-checking golden.

Core IR

The parser's AST is not the semantics. Resolution and elaboration produce a small, immutable CoreModule:

CoreModule {
    id: ModuleId
    version: Version
    snapshot: SourceSnapshotId
    manifest: SourceManifestId
    jurisdiction: JurisdictionId
    declarations: Arena<CoreDecl>
    queries: Arena<CoreQuery>
    verifications: Arena<CoreVerify>
    assertions: Arena<CoreAssertion>
    source_map: SourceMap
}

CoreDecl =
    Source(CoreSource)
  | Entity(CoreEntity)
  | RecordType(CoreRecordType)
  | Office(CoreOffice)
  | Proposition(CoreProposition)
  | Observation(CoreObservation)
  | Fact(CoreFact)
  | Function(CoreFunction)
  | Rule(CoreRule)
  | Position(CorePositionSchema)
  | Power(CorePower)
  | Duty(CoreDuty)
  | Judgment(CoreJudgment)
  | Decision(CoreDecision)
  | LegalAct(CoreLegalAct)
  | InterpretationFamily(CoreInterpretationFamily)
  | ConflictDoctrine(CoreConflictDoctrine)

CoreRule {
    id: NodeId
    kind: Derive | Constitutive | Prescriptive
    binders: Vec<Binder>
    selection: Option<CoreSelection>
    guard: Guard
    consequences: Vec<CoreEffect>
    fallback: Option<Vec<CoreEffect>>
    meta: NodeMeta
}

CoreObservation {
    id: NodeId
    record_binder: Binder
    validators: NonEmptyVec<Guard>
    establishes: PropTerm
    meta: NodeMeta
}

CoreDecision {
    id: NodeId
    binders: Vec<Binder>
    requirements: Vec<Guard>
    option_space: FiniteDomainExpr
    declared_result: Option<DecisionReturn>
    meta: NodeMeta
}

DecisionReturn {
    result_type: TypeId
    expression: CoreExpr
}

CoreFact {
    id: NodeId
    relation: RelationId
    arguments: Vec<Term>
    meta: NodeMeta
}

CoreEffect {
    id: EffectId
    consequence: Consequence
    meta: NodeMeta
}

CoreQuery {
    id: NodeId
    binders: Vec<Binder>
    result_type: TypeId
    effects: FiniteSet<EffectName>
    plan: QueryPlan
    meta: NodeMeta
}

QueryPlan =
    Evaluate(CoreExpr)
  | UniqueOccupant {office: OfficeId}
  | EvaluateClause {
        clause: ClauseSelector
        context: ContextId
        result: CoreExpr
    }
  | RunDecision {
        decision: DecisionId
        arguments: Vec<Term>
        result: DeclaredDecisionResult
    }
  | StatusOf {
        status: LegalStatusPattern
        when_present: Term
        when_closed_absent: Term
    }

ClauseSelector =
    Instantiated {
        clause: ClauseId
        arguments: Vec<Term>
    }
  | Bound {
        binder: Binder
        authenticated_module: ModuleId
    }

DeclaredDecisionResult {
    expected_type: TypeId
}

CoreVerify {
    id: NodeId
    bounds: VerificationBounds
    quantification: QuantificationMode
    fairness: Vec<FairnessAssumption>
    formula: CoreFormula
    meta: NodeMeta
}

Guard =
    Satisfied
  | Operative(PropTerm, ContextId)
  | CompletedAct(ActId)
  | EffectiveAct(ActId)
  | Observed(RecordPattern, Binder, RecordTimeBinder)
  | Derived(RelationId, Vec<Term>)
  | Compare(CompareOp, Term, Term)
  | And(Vec<Guard>)
  | Or(Vec<Guard>)
  | Not(Box<Guard>)
  | Request(OpenOperation)

Consequence =
    Derive(RelationFact)
  | RecordOccurrence(WorldOccurrence)
  | Establish(LegalStatus)
  | Terminate(StatusRef)
  | Suspend(StatusRef)
  | CreatePosition(Position)
  | Discharge(PositionRef)
  | Activate(ProcessRef)

NodeMeta {
    span: Span
    source: Option<SourceRef>
    jurisdiction: JurisdictionId
    valid_time: IntervalExpr
    record_time: IntervalExpr
    origin: OriginId
}

OriginId = Direct(NodeId) | Clause(ClauseId) | Imported(NodeId)

CoreSelection {
    binder: Binder
    finite_domain: FiniteDomainExpr
    predicate: Guard
    ordering: NonEmptyVec<OrderKey>
    require_unique_keys: Bool
}

type SelectionResult<T> =
    Selected(T)
  | NoCandidate
  | OpenSelection(NonEmptySet<OpenRequest>)
  | Ambiguous(NonEmptySet<T>)

CoreAssertion =
    NonDerivation {
        antecedent: Guard
        forbidden: LegalEffectPattern
    }
  | Invariant(CoreFormula)

CoreConflictDoctrine {
    id: NodeId
    guard: Guard
    defeats: NonEmptySet<ConflictTarget>
    as_to: Option<LegalEffectPattern>
    reason: ConflictReason
    meta: NodeMeta
}

ConflictTarget =
    Clause(ClauseId)
  | Rule(RuleId)
  | Effect(EffectId)

The surface-to-Core lowering rules close several intentionally readable shorthands:

Imports are resolved into the authenticated source snapshot before Core is emitted. Type aliases are expanded but retained in the source map. A surface clause may elaborate to several Core nodes, but each node carries the same ClauseId so a conflict doctrine can target the clause, a named rule, or one named effect without relying on display text. No surface declaration may disappear without an explicit elaboration record in the source map.

Every query must contain a body or a goal block; a declaration with only a name and return type is E430 MissingQueryGoal. The runner binds CLI arguments, evaluates the QueryPlan under one RunContext, and lets its selected handler lift the domain result into Outcome<T> exactly once. StatusOf returns its absent value only when the relevant record or domain is closed; otherwise the prerequisite rule requests remain open. EvaluateClause executes the clause's elaborated rules and enforcement dependencies, then evaluates its explicit result expression; it does not return a type name or prose label. A static clause application lowers to ClauseSelector::Instantiated. A bound ClauseRef is resolved only within the authenticated module named by the selector. Its stored arity and argument types are rechecked, while the goal's explicit result expression must unify with the query return type. Failure is E431 InvalidClauseReference, never a runtime lookup by display text.

A decision may omit a return only when it is used solely as a constraint protocol. A decision used by RunDecision must declare -> T and returns e, where e: T is evaluated only after its authority, option-space, record, and substantive requirements succeed. The query's result declared_result lowers to DeclaredDecisionResult { expected_type: T }. Missing or mismatched projections are static errors, so the FOIA query returns the accepted FOIADisposition rather than an unspecified success token.

case_input<T>(key) is a typed Observe request against the case-record schema. A missing key suspends with NeedEvidence; a present value of the wrong schema is Inconsistent. It is not ambient I/O, and the key plus record digest appears in the trace.

A successful CoreObservation appends an evidential establishment of its proposition to the record ledger, scoped by context and both clocks. It does not manufacture the underlying occurrence or mutate institutional state. operative(P, C) may use that record status as a basis only through a named observation, judgment, presumption, or constitutive rule admissible in context C; the trace retains the basis, validators, and source.

Ambiguous is never resolved by source order. Known duplicate nomination keys produce E410 during checking; ambiguity introduced by case data produces an Inconsistent outcome with the conflicting records. An open selection propagates its requests and cannot trigger the otherwise path.

CoreAssertion::NonDerivation is a proof obligation, not a negative mutation. Its forbidden value is a LegalEffectPattern; the surface shorthand does_not_establish Filed(...) injects a proposition pattern into Establish(PropositionStatus(...)). Inside a legal_act, its antecedent is exactly CompletedAct(CurrentLegalActInstance): the performer and validity checks succeeded and the act's declared transition committed. It is not triggered by a mere physical attempt, and it does not require EffectiveAct, because a completed act such as transmitting a filing may intentionally have no constitutive legal effect. Outside a legal_act, this shorthand is rejected; an explicit assert non_derivation when G forbids E is required. Pattern matching is constructor-first, then left-to-right over arguments: exact terms compare by typed equality, binders must agree across repeated occurrences, and _ matches one typed argument without binding it. The checker and verifier reject any trace in which the named antecedent is the only constitutive basis for the forbidden effect. They do not suppress an independent rule that happens to establish the same status. This is how ExecuteOperatingAgreement can be proved insufficient to form the LLC without making formation impossible.

V0.1 conflict handling is deliberately small. After ordinary candidate rule applications are built, the evaluator assigns each staged effect a content-derived EffectId, then runs finite, stratified, nonrecursive conflict doctrines from the fixed source snapshot. One applicable doctrine may defeat a named clause, rule, or effect and must add the target ID, source, and reason to the trace. If no doctrine applies, the conflict remains NormConflict; incompatible multiple doctrines do the same. A Clause(ClauseId) target expands, in EffectId order, to every staged effect whose NodeMeta.origin names that clause, narrowed by as_to when present; an empty expansion is E511 UnknownConflictTarget, not a successful no-op. A rule target expands the same way over that rule application's effects. Defeated effects never reach the atomic commit set. An application-level EffectId is the hash of the rule or clause node, bound arguments, triggering occurrence, and consequence ordinal, so replay names the same effect without conflating different applications. The general ResolveNormConflict effect remains reserved for a later version.

Every semantic node has a NodeId stable within the content hash of its module. Every conclusion can therefore point to exact IR nodes and source spans. Static declarations, runtime state, and trace nodes live in different arenas; mutating an AST node must never change legal state.

NodeMeta.source may be absent only on nonconclusive wrappers such as a query or verification request. Elaboration may inherit a source from an explicitly exercised power, containing clause, or imported doctrine. After that step, every rule, observation, doctrine, position, and staged legal effect must carry a source; otherwise checking reports E540 MissingLegalSource before evaluation.

The eight-ledger state from earlier becomes an immutable runtime value:

LegalState {
    world: WorldLedger
    record: RecordLedger
    legal: LegalStatusLedger
    normative: PositionLedger
    authority: AuthorityLedger
    decisions: DecisionLedger
    interpretations: InterpretationLedger
    sources: SourceLedger
}

State transitions create a new value or append to persistent stores. This makes replay, branching, and bitemporal comparison much easier than in-place mutation.

Static analysis and diagnostics

The compiler performs these passes in order:

parse
    -> authenticate the fixed source manifest
    -> resolve names and imports against that manifest
    -> elaborate surface conveniences
    -> infer and check types/effects
    -> validate sources, authority, and time
    -> stratify derivations
    -> verify finite domains and closure requirements
    -> emit CoreModule

Compiler diagnostics are different from legal outcomes. A malformed program receives a stable diagnostic code, primary span, related spans, and a proposed repair. A valid program may evaluate to Suspended, Contingent, or NormConflict; those are not compiler failures.

The initial diagnostic set is:

E100 ParseError
E200 UnresolvedName
E210 TypeMismatch
E310 PropAsGuard
E320 DirectInstitutionalMutation
E330 MissingConstitutiveBasis
E340 InvalidAuthorityKind
E410 AmbiguousSelection
E420 UnhandledEffect
E430 MissingQueryGoal
E431 InvalidClauseReference
E510 UnjustifiedPriority
E511 UnknownConflictTarget
E520 InvalidBitemporalInterval
E530 NegativeRecursion
E540 MissingLegalSource
W610 OpenUniverse
W620 BoundedVerification

For example:

E310 PropAsGuard

`Incapacitated(Bryan, Administer(BRT))` has type `Prop`,
but this rule requires a guard.

Use one of:
    operative(issue, Administration(BRT))
    determined(issue, Determination#...)
    assumed(issue, Scenario#...)

No implicit proposition-to-Boolean conversion exists.

And a duplicate successor rank should not be settled by file order:

E410 AmbiguousSelection

Alice and Bob both have nomination rank 1 for TrusteeOf(BRT).

Primary:   Nomination#N1
Related:   Nomination#N2
Required:  unique ranks or an explicit tie-resolution rule

Reference operational semantics

The implementation pipeline is atomic at the semantic boundary:

parse -> authenticate manifest -> resolve -> elaborate
     -> type/effect check -> Core IR
     -> evaluate guards and handler requests
     -> stage named effects and evaluate conflict doctrines
     -> validate authority and constitutive basis
     -> check CoreAssertion obligations against the dependency trace
     -> commit consequences atomically
     -> append proof-relevant trace
     -> Outcome<T>

The reference evaluator is a deterministic worklist interpreter. Each guard evaluates to one of four states:

type GuardResult =
    Satisfied {trace: TraceFragment}
  | Refuted {trace: TraceFragment}
  | Open {requests: NonEmptySet<OpenRequest>}
  | Conflict {graph: ArgumentGraph}

Within one stratum, derivation rules run to a finite fixed point. A constitutive rule whose guard is satisfied stages its effects. All staged effects are validated and then committed together. If a guard is open or conflicting, the rule performs no partial mutation. This is essential: a handler request halfway through an amendment cannot leave half the amendment legally effective.

Legal acts use two independent judgments:

evaluate_effectiveness(act, state)
    -> Outcome<ActOutcome<LegalEffect>>

evaluate_compliance(act, state)
    -> Outcome<ComplianceResult>

The evaluator may therefore derive EffectiveButWrongful without contradiction. It may also record a physical occurrence while returning Ineffective for the intended legal effect.

Every evaluation context supplies both clocks. They are not ordinary query parameters, because every rule, effect handler, and trace node observes the same temporal lens:

RunContext {
    source_snapshot: "2036-06-02-ma-trust"
    valid_time: 2033-01-01T00:00:00Z
    record_time: 2036-06-02T00:00:00Z
}

A later order may have earlier valid time, but it cannot have record time before the system received it. Replaying with an earlier record_time must reproduce what the loaded record could support then.

Handler interface and no-false-determinacy

Handlers do not return bare values. They return a value plus a trace fragment, or a structured suspension:

type HandlerResult<T> =
    Resume {
        value: T
        trace_fragment: TraceFragment
    }
  | Suspend {
        requests: NonEmptySet<OpenRequest>
        reason: SuspensionReason
        trace_fragment: TraceFragment
    }
  | Halt {
        reason: HaltReason
        trace_fragment: TraceFragment
    }

type HaltReason =
    OutsideCompetence {
        request: OpenRequest
        reason: CompetenceFailure
    }
  | NormConflict {graph: ArgumentGraph}
  | Inconsistent {core: UnsatCore}

The runner composes every handler fragment with the core evaluation trace before constructing an Outcome; no Resume, Suspend, or Halt path can produce an outcome without the required deterministic trace.

The case-file handler is deliberately boring: it may authenticate and reuse what the record already contains, but it may not create a missing legal answer.

handler CaseFile handles {Observe, Determine, Choose, Interpret}
{
    on Observe.request(issue, schema) {
        match record.evidence_status(issue, schema) {
            Some(status) if validate(schema, status) =>
                resume status with record.trace(issue)

            Some(status) =>
                halt Inconsistent {
                    core: invalid_evidence(status)
                } with rejection_trace(status)

            None =>
                suspend NeedEvidence {issue, schema}
                    with open_request_trace(issue)
        }
    }

    on Determine.request(issue, protocol) {
        match record.controlling_determination(issue) {
            Some(d) if validate(protocol, d) =>
                resume d with determination_trace(d)

            Some(d) =>
                halt OutsideCompetence {
                    request: NeedJudgment {issue, protocol}
                    reason: invalid_scope_or_authority(d)
                } with rejection_trace(d)

            None =>
                suspend NeedJudgment {issue, protocol}
                    with open_request_trace(issue)
        }
    }

    on Choose.request(options, protocol) {
        match record.current_decision(protocol) {
            Some(d) if validate(protocol, d)
                       and options contains d.choice =>
                resume d with decision_trace(d)

            Some(d) =>
                halt OutsideCompetence {
                    request: NeedChoice {protocol, options}
                    reason: invalid_decider_scope_or_choice(d)
                } with rejection_trace(d)

            None =>
                suspend NeedChoice {protocol, options}
                    with open_request_trace(protocol)
        }
    }

    on Interpret.request(source, family) {
        match record.controlling_interpretation(source) {
            Some(i) if family.admits(i) and valid_scope(i) =>
                resume i with interpretation_trace(i)

            Some(i) =>
                halt OutsideCompetence {
                    request: NeedInterpretation {source, family}
                    reason: inadmissible_or_out_of_scope(i)
                } with rejection_trace(i)

            None =>
                suspend NeedInterpretation {source, family}
                    with open_request_trace(source)
        }
    }
}

V0.1 implements four handlers:

CaseFile
    validates evidence, determinations, and interpretations already
    present in the record; never invents a result

Scenario
    resumes from explicit assumptions and marks every resulting trace
    node as Hypothetical

Explore
    branches only over declared finite admissible sets and preserves
    each branch label in the trace; a request without an exhaustive
    declared domain remains an OpenBranch and is never dropped

Skeptical
    runs Explore; returns Determinate only when the nonempty exhaustive
    completion set agrees on one answer and every OpenBranch has a
    checked convergence certificate proving all of its admissible
    extensions return that answer; returns Contingent when completed
    answers diverge, Suspended when an uncertified OpenBranch remains,
    NormConflict when an unresolved conflict remains, or Inconsistent
    when the explored assumptions have an unsatisfiable core

Aggregation uses a fixed conservative precedence. If every branch is unsatisfiable, return Inconsistent. Otherwise an uncertified OutsideCompetence halt prevents a determinate answer; next, any uncertified open request yields Suspended, then any unresolved conflict yields NormConflict. Only after those blockers are absent may divergent total answers yield Contingent or convergent answers yield Determinate. The trace retains every discarded unsatisfiable branch and every known alternative, so the precedence does not erase why the stronger outcome was unavailable.

The bounded no-false-determinacy test is then executable rather than aspirational. For every finite case fixture and query, enumerate the declared admissible completions. If Skeptical returns Determinate(v), assert that every total completion returns $v$ and that every open branch carries a valid certificate covering all admissible extensions. The first implementation does not prove this over arbitrary law; it exhaustively checks the property over the bounded reference semantics and preserves the conditions needed for a later proof.

Trace, output, and explanation contract

Every evaluation emits deterministic JSON and a trace DAG. Stable output matters for tests, external tools, and signed audit artifacts.

{
  "schema": "fidryn.outcome/v0.1",
  "module": "Examples.BryanRevocableTrust@0.1.0",
  "sourceSnapshot": "2026-08-23-ma-trust-fixture",
  "query": "acting_trustee",
  "asOf": {
    "validTime": "2033-01-01T00:00:00Z",
    "recordTime": "2036-06-02T00:00:00Z"
  },
  "outcome": {
    "kind": "determinate",
    "value": "Bob",
    "trace": "trace:T30",
    "convergenceCertificate": null,
    "ignoredOpenIssues": []
  }
}

Trace nodes have a closed initial vocabulary:

SourceText
StrictRuleApplication
DefeasibleRuleApplication
EvidenceSubmission
ClosureRecord
Presumption
Determination
DiscretionaryDecision
InterpretationSelection
ConflictDoctrine
Assumption
ConstitutiveEffect
SolverLemma

Canonical serialization sorts maps and sets, normalizes timestamps, and refers to nodes by content-derived IDs. Running the same query against the same source snapshot and record must produce byte-identical JSON.

Compiler repository and command line

Rust is a practical implementation language for the reference toolchain because the core is a typed compiler and persistent evaluator, but the semantics must not depend on Rust-specific behavior. I would create this workspace:

fidryn/
├── Cargo.toml
├── crates/
│   ├── fidryn-syntax/       # lexer, lossless tree, parser, formatter
│   ├── fidryn-hir/          # names, imports, surface elaboration
│   ├── fidryn-core/         # canonical types and CoreModule
│   ├── fidryn-check/        # types, effects, authority, time, strata
│   ├── fidryn-eval/         # reference worklist evaluator
│   ├── fidryn-handlers/     # CaseFile, Scenario, Explore, Skeptical
│   ├── fidryn-verify/       # bounded temporal and completion explorer
│   ├── fidryn-trace/        # DAG, canonical JSON, source maps
│   └── fidryn-cli/
├── schemas/
│   ├── outcome-v0.1.json
│   ├── case-record-v0.1.json
│   └── source-manifest-v0.1.json
├── examples/
│   ├── trust/
│   ├── prenup/
│   ├── foia/
│   └── massachusetts-llc/
└── tests/
    ├── parse/
    ├── diagnostics/
    ├── traces/
    ├── bitemporal/
    └── completions/

The CLI contract is:

fidryn fmt PATH
fidryn check PATH
fidryn run PATH --query NAME --case RECORD.json \
    --valid-at TIME --known-at TIME
fidryn explore PATH --query NAME --case RECORD.json --bounds BOUNDS.json \
    --valid-at TIME --known-at TIME
fidryn explain TRACE_ID --format text|json|dot
fidryn verify PATH --property NAME
fidryn diff OLD_SNAPSHOT NEW_SNAPSHOT --query NAME
fidryn render PATH --template TEMPLATE

run never silently chooses a completion. explore requires explicit finite bounds. render is experimental and cannot mark prose semantics-preserving unless a separately trusted renderer proves that property for its constrained template fragment.

Milestones and acceptance tests

Build the language in this order:

1. Syntax. Implement lexer, lossless tree, parser, formatter, source spans, parse goldens, and recovery around a malformed declaration.
2. Core. Resolve names and imports, elaborate the four examples, serialize stable CoreModule snapshots, and reject duplicate or missing source IDs.
3. Static semantics. Implement nominal types, Prop, effect rows, authority kinds, office occupancy, interval checks, rank uniqueness, stratification, and diagnostic goldens.
4. Reference evaluator. Support initial occupancy, observations, determinations, constitutive transitions, duties, and atomic traces without any solver backend.
5. Handlers. Add CaseFile, Scenario, Explore, and Skeptical; exhaustively test no-false-determinacy on the finite trust fixture.
6. Acts and time. Add ActOutcome, independent compliance, valid/record time, retrospective determinations, and replay tests.
7. Verification. Add bounded invariants, finite liveness with explicit fairness, closure warnings, counterexample traces, and source-snapshot diffing.
8. Artifacts. Add canonical JSON, trace explanations, constrained templates, and the other three domain fixtures.

V0.1 is done only when all of these statements are true:

• one certificate yields Determinate(Bryan) plus an ignored NeedEvidence issue only with a checked convergence certificate;
• one completed Bob branch plus an uncertified open branch that can still yield Alice returns Suspended, never Determinate(Bob);
• two certificates and two admissible eligibility interpretations yield Contingent({I1: Alice, I2: Bob});
• a scoped court interpretation yields Determinate(Bob);
• duplicate successor ranks produce E410 AmbiguousSelection;
• a query without a body or explicit goal produces E430 MissingQueryGoal;
• a proposition used directly as a guard produces E310 PropAsGuard;
• an incapacity effect cannot commit if its handler suspends;
• a disputed amendment capacity suspends Outcome<ActOutcome<_>> rather than inventing an act result;
• a prenup provision cannot be applied to adversely affect a child's support right; the trace identifies the statutory limit and the affected provision and effect, while a spousal-support waiver remains judgment-dependent;
• the child-support doctrine's ClauseId target expands only to the matching staged waiver effects and reports E511 if that expansion is empty;
• a FOIA withholding cannot appear without an exemption basis, the applicable harm showing where required, and the segregability record; every determination produces reasons and Public Liaison assistance notice, while only an adverse determination adds the appeal and dispute-resolution notice;
• a Massachusetts LLC is never formed before the proved filing event or its permitted later effective time, and an operating agreement never substitutes for formation;
• the filing observation binds both wildcard times in Filed(HarborRoboticsCertificate, _, _) before the formation rule runs;
• bitemporal replay distinguishes what was legally valid from what the record showed;
• every outcome has a source-complete trace; and
• repeated evaluation is byte-for-byte deterministic.

Only after this reference interpreter is stable should the project add a visual editor, controlled English, live filing adapters, unconstrained text generation, or multiple solver backends. For any backend fragment $F$, translation $T_F$ must eventually be shown sound with respect to Fidryn Core under declared finiteness, source, closure, and handler assumptions.

Part IV: evaluation and failure conditions

Then I would encode the same difficult trust provisions in eFLINT, L4, Symboleo, and the proposed IR, using LegalRuleML where useful for interchange and provenance. The corpus should include incapacity and restoration, successor acceptance, vacancy and court appointment, amendment formalities, mandatory and discretionary distributions, creditor claims, survivorship, distribution by representation, and court modification.

For every encoding, the study should record:

• which concepts are native language constructs;
• which become ordinary predicates or comments;
• which judgments are represented as application-supplied facts, opaque predicates, callbacks, or explicit institutional records;
• which institutional acts become field assignments;
• which source, authority, or interpretation information is lost;
• which verification properties remain expressible; and
• which assumptions are machine-visible.

Two metrics matter more than line count.

The semantic escape-hatch rate measures how often legally material structure is replaced with an opaque Boolean, untyped callback, unrestricted predicate, or prose comment. Its denominator must come from an independently annotated, lawyer-reviewed corpus rather than from the concepts the candidate language happens to expose:

The false-determinacy rate measures how often the evaluator returns a single result even though that result varies across admissible completions:

This is a false-determinacy rate conditioned on non-invariant queries. Its numerator counts queries, once each. It does not detect an incorrect answer on a query whose completions all agree; report that separately as wrong determinate answers divided by all determinate answers. Empty or inconsistent completion spaces belong in their own outcome category. A zero denominator makes a rate undefined, not zero.

The second metric should approach zero by construction, but it cannot stand alone. An evaluator that returns Suspended { NeedJudgment(...) } for every query achieves zero false determinacy and has no practical value. The study also needs invariant-answer coverage:

All three metrics must be evaluated on frozen, bounded, and labeled scenario suites whose source snapshot, jurisdiction, closure assumptions, interpretation families, and completion spaces are declared in advance. The first rate should be lower than the comparison systems, the second should approach zero, and coverage should remain useful without making ordinary encodings impossibly verbose.

False-determinacy measurement therefore requires a benchmark oracle or an exhaustively enumerated bounded completion space. In the reference semantics, false determinacy is intended to be impossible; a nonzero observed rate would expose either an unsound analysis or an incomplete admissibility model.

That last condition matters. A language can achieve perfect explicitness by demanding a formal model of the entire legal system before compiling one trust. That is not a useful victory. The study must measure modeling burden, lawyer readability, explanation quality, solver behavior, and the number of provisions that remain in deliberately opaque form.

The research wager

The defensible research thesis is narrower than “a programming language for law”:

Legal instruments can be modeled as authority-indexed normative transition systems in which evidence, institutional judgment, discretion, interpretation, conflict resolution, and applicable-law selection are typed effects, and in which evaluation remains partial until those effects are handled or shown irrelevant to the result.

The proposed contributions would be:

1. a calculus for judgment effects and authority-indexed handlers;
2. a soundness theorem—or, initially, a bounded conservative-analysis result—relative to an explicit admissible-completion semantics;
3. proof-relevant legal-act outcomes separating validity, effectiveness, wrongfulness, voidability, and dispute;
4. robust verification over interpretation and discretionary choice spaces; and
5. a comparative, multi-domain corpus that measures semantic escape hatches rather than celebrating surface expressiveness.

The project should be abandoned or redirected if the comparative study shows that the same properties can be expressed cleanly as libraries or disciplined encodings in an existing system; if admissible completions cannot be defined without smuggling every hard question into an oracle; if useful queries become intractable even on the bounded trust corpus; or if lawyers cannot tell whether a judgment protocol matches the source instrument.

The surface syntax is not the research contribution. A new syntax is justified only after the kernel survives those tests.

What this proposal does not claim

This essay does not establish that the calculus is novel, sound, complete, decidable, or usable. It does not prove that trusts reduce to transition systems. It does not settle a jurisprudential theory of truth or interpretation. It does not show that formal source and generated prose can be made legally equivalent. It does not decide reasonableness, best interests, credibility, good faith, or intent. It does not make a formal artifact legally operative. The trust, premarital-agreement, FOIA, and LLC programs are research fixtures; they are not instruments, filings, legal opinions, or a complete statement of any jurisdiction's law.

Most importantly, no-false-determinacy is always relative to what the model admits. If the drafter omits a plausible interpretation, loads the wrong source version, assumes a closed family that is not closed, or gives an office authority it does not possess, the evaluator can be precisely wrong. The principle is a semantics and a proof obligation, not a substitute for legal expertise.

That limitation is not unique to this project. Every formal model draws a boundary around the world. The proposal merely insists that the boundary, assumptions, and institutional dependencies become part of the result.

Conclusion: a judge is not an untyped callback

The easiest legal programs are the ones that quietly move every difficult decision into their inputs. Someone supplies incapacitated = true, reasonable = false, and governing_law = Massachusetts, and the program performs impeccable logic from there. The logic may be correct while the legal model is nearly empty.

A serious language should force a different conversation. Fidryn is the concrete proposal for doing so.

Who established incapacity? Under which instrument-defined procedure? On what record? For which capacity and which legal purpose? When did the result become operative? Who could review it? Did suspension create a vacancy? Did the successor accept? Which powers attached to the office, and were later acts effective even if wrongful?

Those questions do not sit outside the computation. They determine what the computation is allowed to mean.

The point is not to automate the judge away. It is to stop pretending the judge is a Boolean callback. Evidence, judgment, interpretation, and discretion should enter the model as typed, authorized, reviewable operations with visible effects on legal state.

Sometimes every admissible path will converge, and the language should return an answer with a trace. Sometimes the paths will diverge, and it should identify the pivot. Sometimes the record will be insufficient, the source conflict unresolved, or the requested actor outside its competence.

In those cases, refusal is not the absence of computation. It is the most important computation the system performs.

Primary sources and further reading

• L. Thomas van Binsbergen, Christopher A. Esterhuyse, and Tim Müller, “Reflections on the design, applications and implementations of eFLINT, a domain-specific language for legal compliance reasoning”, Journal of Computer Languages, article 101411, 2026; open arXiv version.
• Denis Merigoux, Nicolas Chataing, and Jonathan Protzenko, “Catala: A Programming Language for the Law”, 2021.
• Alireza Parvizimosaed, Sepehr Sharifi, Daniel Amyot, Luigi Logrippo, Marco Roveri, Aidin Rasti, Ali Roudak, and John Mylopoulos, “Specification and Analysis of Legal Contracts with Symboleo”, Software and Systems Modeling 21(6), 2395–2427, 2022.
• Legalese, “Regulative Rules” and “Default Reasoning and Exceptions”, current L4 documentation.
• SMU CCLAW, “How L4 Approaches Law”, historical documentation, 2023.
• How Khang Lim, Avishkar Mahajan, Martin Strecker, and Meng Weng Wong, “Automating Defeasible Reasoning in Law”, arXiv:2205.07335, 2022.
• OASIS, LegalRuleML Core Specification Version 1.0, OASIS Standard, 30 August 2021.
• Thomas F. Gordon, Henry Prakken, and Douglas Walton, “The Carneades Model of Argument and Burden of Proof”, Artificial Intelligence 171(10–15), 875–896, 2007.
• Gordon D. Plotkin and Matija Pretnar, “Handling Algebraic Effects”, Logical Methods in Computer Science 9(4:23), 2013.
• California Legislative Information, California Family Code sections 1610–1617, current online code used for the premarital-agreement fixture.
• Office of the Law Revision Counsel, “About the United States Code”, including the Code's source, organization, and relationship to federal statutes, and the preliminary text of 5 U.S.C. § 552.
• U.S. Department of Justice, Office of Information Policy, the DOJ Guide to the Freedom of Information Act, used as explanatory material rather than statutory text.
• Massachusetts General Court, M.G.L. c. 156C, § 5 and § 12, together with the Secretary of the Commonwealth's LLC filing instructions.
• Financial Crimes Enforcement Network, “Beneficial Ownership Information Reporting”, current federal reporting-status guidance used only to illustrate versioned downstream obligations.
• OECD, “Consultation on the Digital Provision of Law: Towards a Shared Reference Framework for Law as Code”, public consultation, 2026.