Can organisational intent be expressed as a formally structured specification…

Can organisational intent be expressed as a formally structured specification from which artefacts are derived and consistency is machine-checked?

2026-03-14 · governance-policy knowledge-management formal-methods · medium · source → · wiki →

key claims

Goal-Oriented Requirements Engineering frameworks — particularly iStar's Strategic Rationale (SR) model extended by Formal Tropos — provide machine-checkable goal hierarchy specifications with formal properties; the T-Tool (NuSMV model checker) finds non-trivial gaps and inconsistencies in goal specifications at scale comparable to strategy portfolios
Catala (Merigoux et al., ICFP 2021) demonstrates in production that a single canonical source generating both human-readable artefacts and an executable correct-by-construction specification is viable; its French family benefits implementation (~1,500 lines including embedded legislative text) uncovered a bug in the official government implementation that all prior informal review missed
Consistency (no contradiction between elements) and derivability (an initiative is formally derivable from a stated objective) are distinct properties requiring different formal machinery; conflating them produces underpowered specifications that cannot catch the most consequential class of misalignment — initiatives approved without formal grounding in any stated objective
Hoshin Kanri's X-matrix is structurally equivalent to an iStar contribution map — the most widely deployed near-formal derivation chain in practitioner strategy — but lacks the three properties needed for machine-checking: formal syntax for elements, typed derivation annotations on correlation marks (+/−), and a constraint solver; adding these three properties would produce a machine-checkable near-equivalent at modest incremental authorship cost
Beyond Budgeting's critique of annual funding cycles identifies a structural decoupling that is directly addressable in a formal strategy spec by expressing resource allocation as conditional deontic obligations — O(allocate(R, I) | condition C) — enabling automated detection of allocation decisions that contradict stated strategic conditions; the barrier to doing so is organisational, not computational
Simon's near-decomposability theorem (1962) implies that mission-level values propagated top-down without layer-level invariant specification produce no detectable short-run constraint violations — misalignment accumulates through aggregate long-run effects — so each hierarchy layer must independently encode its relevant constraints rather than inheriting them from above
The EOSIO Ricardian Template Toolkit demonstrates in production blockchain infrastructure that dual-artefact generation (one canonical source producing both a machine-executable specification and a human-readable HTML presentation) is achievable; the critical design principle — treating the formal spec as canonical and generating prose from it — is the required inversion from current strategy document practice, where prose is primary and formal representations are derived post-hoc
No production tool currently implements formal consistency or derivability checking at organisation-level strategy scale; the gap between academic GORE tools and commercial OKR software platforms represents approximately 10–15 years of the maturation timeline that formal software specification tools followed from informal requirements documents to type systems

Research Question

Can organisational intent — mission, values, strategy, resource allocation — be expressed as a formally structured specification from which human-readable artefacts are derived, and against which Objectives and Key Results (OKRs), funding decisions, and initiative prioritisation can be continuously checked for logical consistency and derivability?

Findings

(Populated from §6 Synthesis above.)

Executive Summary

Organisational intent can in principle be expressed as a formally structured specification against which OKRs, funding decisions, and initiative prioritisation are machine-checked for consistency and derivability — but no production tool currently does this, and the gap is primarily one of authorship cost and organisational adoption, not technical feasibility. The formal machinery exists across three bodies of work: Goal-Oriented Requirements Engineering (GORE) frameworks (iStar, Formal Tropos) provide machine-checkable goal hierarchy models; defeasible deontic logic provides normative conflict detection; and Catala's prose-specification inversion and the EOSIO Ricardian Template Toolkit both demonstrate single-source dual-artefact generation in production. Consistency checking (no contradictions between elements) and derivability checking (an initiative is formally derived from a stated objective) require different machinery and represent a practical gradient — organisations can implement consistency checking at modest cost before committing to full derivability. The primary non-technical barrier is that strategic ambiguity is a political resource: narrative strategy documents enable coalition-building through deliberate imprecision, and formalisation eliminates that imprecision by design.

Key Findings

Goal-Oriented Requirements Engineering frameworks — particularly iStar's Strategic Rationale (SR) model extended by Formal Tropos — provide machine-checkable goal hierarchy specifications with formal properties; the T-Tool (NuSMV model checker) finds non-trivial gaps and inconsistencies in goal specifications at scale comparable to strategy portfolios. [Confidence: high]
Catala (Merigoux et al., ICFP 2021) demonstrates in production that a single canonical source generating both human-readable artefacts and an executable correct-by-construction specification is viable; its French family benefits implementation (~1,500 lines including embedded legislative text) uncovered a bug in the official government implementation that all prior informal review missed. [Confidence: high]
Consistency (no contradiction between elements) and derivability (an initiative is formally derivable from a stated objective) are distinct properties requiring different formal machinery; conflating them produces underpowered specifications that cannot catch the most consequential class of misalignment — initiatives approved without formal grounding in any stated objective. [Confidence: high]
Hoshin Kanri's X-matrix is structurally equivalent to an iStar contribution map — the most widely deployed near-formal derivation chain in practitioner strategy — but lacks the three properties needed for machine-checking: formal syntax for elements, typed derivation annotations on correlation marks (+/−), and a constraint solver; adding these three properties would produce a machine-checkable near-equivalent at modest incremental authorship cost. [Confidence: medium]
Beyond Budgeting's critique of annual funding cycles identifies a structural decoupling that is directly addressable in a formal strategy spec by expressing resource allocation as conditional deontic obligations — O(allocate(R, I) | condition C) — enabling automated detection of allocation decisions that contradict stated strategic conditions; the barrier to doing so is organisational, not computational. [Confidence: high]
Simon's near-decomposability theorem (1962) implies that mission-level values propagated top-down without layer-level invariant specification produce no detectable short-run constraint violations — misalignment accumulates through aggregate long-run effects — so each hierarchy layer must independently encode its relevant constraints rather than inheriting them from above. [Confidence: high]
The EOSIO Ricardian Template Toolkit demonstrates in production blockchain infrastructure that dual-artefact generation (one canonical source producing both a machine-executable specification and a human-readable HTML presentation) is achievable; the critical design principle — treating the formal spec as canonical and generating prose from it — is the required inversion from current strategy document practice, where prose is primary and formal representations are derived post-hoc. [Confidence: high]
No production tool currently implements formal consistency or derivability checking at organisation-level strategy scale; the gap between academic GORE tools and commercial OKR software platforms represents approximately 10–15 years of the maturation timeline that formal software specification tools followed from informal requirements documents to type systems. [Confidence: medium]
Teece–Pisano–Shuen dynamic capabilities (1997) provide a near-formal rule for build-vs-buy decisions — capabilities that are distinctive, inimitable, and process-embedded cannot be purchased below the cost of acquiring the firm itself — but the classification criteria are qualitative judgements that require human encoding before they become machine-checkable derivation conditions. [Confidence: medium]
Real Options theory (Trigeorgis, 1996) provides formal vocabulary for initiative investment decisions under uncertainty — option type, exercise conditions, underlying asset, volatility — all groundable in elements of a formal strategy specification; the main technical gap is estimating volatility for strategic capabilities without historical price data analogous to financial assets. [Confidence: medium]
The primary barrier to formal strategy specification adoption is not technical feasibility but the political function of strategic ambiguity: narrative strategy documents allow incompatible stakeholder interpretations to coexist and enable coalition formation, and formalisation eliminates this by making contradictions undeniable rather than deferrable. [Confidence: medium — inference from historical parallels in software formal methods adoption; no direct empirical study of this dynamic in strategy contexts was found]
Defeasible deontic logic (Governatori and Rotolo, 2008) provides logical foundations for normative consistency checking across abstraction layers, including contrary-to-duty obligations that arise when a primary obligation is violated — a structure directly applicable to modelling strategy override conditions, escalation clauses, and contingency policies. [Confidence: high]

Assumptions

Assumption: A formal strategy specification tool would be computationally tractable at organisation scale (tens of objectives, hundreds of initiatives). Justification: Formal Tropos/T-Tool demonstrates tractable model checking for comparable-scale early requirements. Governatori NP-completeness applies to concurrent parallel execution paths, not sequential strategy portfolios.
Assumption: Catala's prose-spec interweaving maps structurally onto strategy's "guiding policy with conditional exceptions." Justification: Both use a default rule + conditional override structure; the analogy breaks where strategy involves qualitative judgements not reducible to computable rules.
Assumption: Political resistance to formalisation is a primary adoption barrier beyond cost. Justification: Inferred from historical adoption pattern of formal methods in software and the observation that strategy ambiguity serves coalition-building; no direct empirical study in strategy contexts was found.

Analysis

The evidence divides into two tiers. The first tier — formal machinery exists and is production-viable in adjacent domains — is supported by primary sources with high confidence: Formal Tropos/T-Tool (2004), Catala (2021), EOSIO Ricardian Toolkit (2018–present), Deon Digital CSL (commercial product). The second tier — whether this machinery transfers to strategy artefacts — is supported by structural analogies and inferences with medium confidence, because no direct implementation of a formal strategy specification language exists in production.

The key tension is between technical tractability (high, based on adjacent-domain evidence) and adoption tractability (low, based on the political-ambiguity argument and the historical pattern of formal methods adoption). Catala partially resolves this tension for statutory law by making prose the visually primary authorship layer (programmers annotate text rather than writing formal rules that generate prose); a strategy specification tool would need a similarly prose-first authorship model to achieve adoption.

The consistency/derivability distinction matters practically: an organisation wanting only consistency checking (no contradictions between stated objectives, approved initiatives, and funding allocations) needs a lighter-weight tool than one wanting full derivability checking (every initiative provably derived from a stated objective). Consistency checking is closer to current workshop practice and represents a tractable first step; full derivability checking is a qualitatively more demanding commitment.

The Hoshin Kanri finding is the most actionable: it is the only practitioner framework already close enough to machine-checkable form that incremental formalisation — adding typed link annotations and a constraint solver — could produce a working tool without requiring organisations to learn a new paradigm.

Risks, Gaps, and Uncertainties

No empirical study of the political-ambiguity-barrier hypothesis in strategy contexts was found; this is an inference from historical parallels.
Volatility estimation for Real Options applied to strategic capabilities has no established methodology analogous to financial asset pricing.
Formal Tropos / model checking scaling behaviour for enterprise-scale strategy specifications (thousands of initiatives) is not confirmed; T-Tool was validated only on academic case studies.
Deon Digital CSL has minimal recent GitHub activity (post-2019), suggesting limited practitioner adoption despite sound technical foundations; the company's current commercial status is unclear.
Catala has active academic development but limited practitioner adoption outside the French government tax/benefit domain as of early 2026.

Open Questions

What would a Catala-style strategy specification language look like? What is the minimum formal grammar enabling consistency and derivability checking while preserving a prose-first authoring experience? (Candidate backlog item.)
How should volatility of a strategic capability be estimated for Real Options purposes in the absence of historical price data? Are there empirical proxies (capability age, investment duration, competitive imitation rate)?
What does layer-level invariant specification look like in practice for large engineering organisations? Are Amazon's "input metrics" or similar constructs a working precedent?
Could an existing language (Alloy, Z notation, Constraint Handling Rules) serve as the foundation for a strategy specification language, or is a domain-specific language required?
Is there an empirical study of conditions that have historically triggered adoption of more formal strategy representations (regulatory pressure, crisis, leadership change)?

sources

← newerSWAT technique in a fresh-context loop

older →Hosting options for the Research repo