--- title: "Law Does Not Return a Boolean" description: "Fidryn is a proposed programming language for legal instruments: precise where law is mechanical, explicit where judgment enters, and incapable of hiding authority, discretion, or ambiguity inside a Boolean." date: "2026-08-23" type: "work" slug: "law-does-not-return-a-boolean" url: "https://www.onlygass.dev/work/law-does-not-return-a-boolean" markdown: "https://www.onlygass.dev/work/law-does-not-return-a-boolean.md" thumbnail: "https://www.onlygass.dev/images/thumbnails/law-does-not-return-a-boolean.png" readingTime: 96 author: "Bryan Gass" tags: ["programming languages", "computational law", "formal methods", "legal reasoning", "algebraic effects", "language design"] --- # 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: ```text 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: | Drafting move | What it does legally | What a language must preserve | | -------------------------------- | ----------------------------------- | --------------------------------------------------- | | Defined amount, date, or formula | fixes a consequence | total or guarded computation | | Condition or formality | controls when an effect attaches | event, evidence, and validity structure | | Institutional procedure | says how a status becomes operative | record, authority, determination, and scope | | Discretionary power | allocates bounded choice | office, choice space, reasons, and review | | Open-textured standard | reserves evaluative judgment | typed judgment request rather than an input Boolean | | Exception or overriding rule | defeats or narrows another rule | defeasibility with a legally justified priority | | Ambiguous language | supports competing meanings | executable interpretations and provenance | | Omission or contradiction | creates a drafting defect | diagnostic, not invented meaning | 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: ```text 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: ```text 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: $$ (S,e) \longrightarrow S'. $$ 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: ```text 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: ```text 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: ```text 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: | Dimension | Example question | | ------------------- | ----------------------------------------------------------------------------- | | Proposition content | Is Bryan incapacitated for the capacity relevant to administering this trust? | | World hypothesis | Is the proposition actually true in the scenario being modeled? | | Assertion | Who alleged or denied it, and in which proceeding? | | Record | What evidence was offered, admitted, excluded, or credited? | | Procedural posture | Is a presumption active? Who bears production and persuasion? | | Competence | Who is authorized to determine this issue for this purpose? | | Determination | What result was issued, on what record, under what standard? | | Operative scope | Whom does the result bind, for what issue and interval? | | Review | Is it final, appealable, stayed, reversed, vacated, or remanded? | 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`: ```text 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 $$ \operatorname{Determined}(P) \Rightarrow P. $$ It is closer to $$ \operatorname{ValidDetermination}(d,P,C) \land\operatorname{Result}(d)=\operatorname{Established} \Rightarrow \operatorname{Operative}(P,C). $$ 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. ```text type Outcome = Determinate { value: T trace: TraceId convergence_certificate: Option ignored_open_issues: FiniteSet } | Contingent { alternatives: Map pivots: FiniteSet trace: TraceId } | Suspended { requests: NonEmptySet 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 } | NeedInterpretation { source: SourceSpan family: InterpretationFamilyId } | NeedApplicableLaw { issue: LegalIssue candidates: FiniteSet } type PropPattern = Ground(Prop) | Match { predicate: PropId arguments: Vec } type TermPattern = Exact(Term) | Bind(Binder) | Wildcard type LegalStatusPattern = PropositionStatus { proposition: PropPattern context: ContextPattern } | InstitutionalStatus { constructor: StatusConstructorId arguments: Vec } type LegalEffectPattern = Establish(LegalStatusPattern) | Terminate(LegalStatusPattern) | Suspend(LegalStatusPattern) | CreatePosition(PositionPattern) | Affect(LegalSubjectPattern) type PositionPattern = MatchPosition { kind: PositionKind arguments: Vec } 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: $$ \operatorname{Eval}(q,\Sigma)=\operatorname{Determinate}(v) \quad\Longrightarrow\quad \mathcal{C}_q(\Sigma)\neq\varnothing \;\land\; \left(\forall c\in\mathcal{C}_q(\Sigma),\; \operatorname{Answer}(\operatorname{Eval}(q,c))=v\right) \;\land\; \left(\forall o\in\mathcal{O}_q(\Sigma),\; \operatorname{CertifiedInvariant}(o,v)\right). $$ 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](https://homepages.inf.ed.ac.uk/gdp/publications/handling-algebraic-effects.pdf) 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: ```text effect Observe { request( issue: PropPattern, schema: RecordSchemaId ) -> EvidentialStatus } effect Determine { request( issue: Prop, protocol: JudgmentProtocolId ) -> Determination } effect Choose { request( options: FiniteSet, protocol: DecisionProtocolId ) -> Decision } effect Interpret { request( source: SourceSpan, family: InterpretationFamilyId ) -> SelectedInterpretation } effect ResolveNormConflict { request( conflict: ArgumentGraph, doctrines: FiniteSet ) -> ConflictResolution } effect SelectApplicableLaw { request( issue: LegalIssue, candidates: FiniteSet ) -> ApplicableLawSet } ``` A trustee-succession core can then expose its unresolved legal dependencies in its type: ```text 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. ```text 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` describes what a particular handler reports when it cannot—or should not—discharge those requests. ```text fn acting_trustee_in_case(trust: Trust) -> Outcome { 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: ```text 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: ```text 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: ```text 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: $$ \Sigma = \langle W,R,L,N,A,D,I,V\rangle, $$ 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: ```text 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: $$ \Gamma,\iota \vdash \langle\Sigma,x\rangle \Longrightarrow \langle\Sigma',\tau\rangle. $$ 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: ```text if Incapacitated(Bryan) { activate Succession(BRT) } ``` The drafter must say which status of the proposition matters: ```text 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: ```text BRT.revocable = false ``` Irrevocability is a legal effect. The trace needs a constitutive rule, a competent institutional act, or a valid exercise of power: ```text 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` 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. ```text 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: ```text 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: ```text 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. ```text 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: $$ \operatorname{Power}(a,\phi) \land \operatorname{ValidExercise}(x,a,\phi) \Rightarrow \operatorname{Effective}(\phi), $$ while $$ \operatorname{Duty}(a,\neg x) \land \operatorname{Performed}(a,x) \Rightarrow \operatorname{Violation}(a,x). $$ 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](https://arxiv.org/abs/2511.12276); 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: ```text type ActOutcome = Ineffective { defects: FiniteSet } | Effective { effect: E, compliance: Compliant } | EffectiveButWrongful { effect: E, violations: FiniteSet } | 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>::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: ```text predicate BestInterest(person, action) -> Discretionary ``` The type admits discretion and still models it as a hidden truth-value provider. The legally significant object is usually the structured decision process. ```text 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: ```text 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. ```text 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: ```text 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: | Program | Dominant difficulty | What Fidryn must demonstrate | | ------------------------------- | ------------------------------------------------------------- | -------------------------------------------------------------------- | | Revocable trust | succession, powers, duties, discretion | long-lived private legal state | | California premarital agreement | formation, disclosure, mandatory law, later enforceability | agreement validity is issue- and time-sensitive | | Federal FOIA slice | statutes, agency process, exemptions, deadlines, review | public law is a versioned source bundle, not one rule file | | Massachusetts LLC formation | filing, external authority, effective time, continuing duties | paperwork and private agreements do not themselves create the entity | 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. ```text 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](https://leginfo.legislature.ca.gov/faces/codes_displayText.xhtml?article=2&chapter=2.&division=4.&lawCode=FAM&part=5.&title=). ```text 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 obligations: FiniteSet 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("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: ```text $ 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](https://uscode.house.gov/about.xhtml) 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](https://uscode.house.gov/view.xhtml?edition=prelim&hl=false&num=0&req=granuleid%3AUSC-prelim-title5-section552&saved=%7CKHRpdGxlOjUgc2VjdGlvbjo1NTIgZWRpdGlvbjpwcmVsaW0pIE9SIChncmFudWxlaWQ6VVNDLXByZWxpbS10aXRsZTUtc2VjdGlvbjU1Mik%3D%7CdHJlZXNvcnQ%3D%7C%7C0%7Cfalse%7Cprelim), and the Department of Justice maintains a sectioned, explanatory [FOIA Guide](https://www.justice.gov/oip/doj-guide-freedom-information-act-0). Agency regulations and controlling decisions must be separate imports; the guide is not a substitute for them. ```text 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 withheld: FiniteSet } 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("responsive_record") case_input("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: ```text $ 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](https://malegislature.gov/Laws/GeneralLaws/PartI/TitleXXII/Chapter156C/Section5), [§ 12](https://malegislature.gov/Laws/GeneralLaws/PartI/TitleXXII/Chapter156C/Section12), and the Secretary of the Commonwealth's [LLC filing instructions](https://www.sec.state.ma.us/divisions/corporations/filing-by-subject/limited-liability/corporations-limited-liability-company.htm). ```text 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 managers: FiniteSet authorized_filers: FiniteSet real_property_signers: FiniteSet business_character: String requested_effective_time: Option