Formal model
Addition to the working formal model
The protocol defines records, states, confirmations and transitions. A confirmation includes action type, participant, authority, object, scope, time and conditions version. Candidate invariants: acknowledgment creates no commitment; an AI proposal does not replace a decision; material new versions require proper agreement; execution differs from acceptance; history and reasons for changes are retained. These requirements still need formalisation and verification.
Who → to whom → outcome → deadline → conditions → resources → dependencies → who accepts the outcome and by which criteria. Also record the basis, authority, version, confirmations, evidence and revision or dispute procedure. A resource promised more than once requires a joint feasibility check.
An executor’s responsibility is considered alongside commitments to supply resources, decisions and access. Managers, support services and the system operator also have verifiable commitments. A group’s commitment relies on its representative’s authority and supporting internal commitments; only information needed by other parties is disclosed.
How the protocol worksA draft language for commitments, authority and transitions.
Objects and relations
Entities: participant, goal, authority, resource, action, commitment, condition, dependency, evidence and acceptance. A commitment record connects the parties, expected outcome, deadline and grounds for confirmation. The network known to participants is not equated with all actual activity dependencies.
Transitions and candidate invariants
Proposal, confirmation, execution, acceptance, revision and dispute require definitions. Candidate invariants: actions require appropriate authority; environmental changes do not themselves rewrite agreements; term history is retained; execution and acceptance are distinct. These are draft requirements, not verified theorems.
Boundary of proof
Formal compatibility of commitments does not guarantee achievement of shared goals. Even a fulfilled network can rely on incorrect information, omit important dependencies or deliver only intermediate outcomes. Acceptance of an individual task and organisational success are assessed separately.
Artifacts and status
Status: draft specification. The definitions on this page are the available artefact. “Formally verified” requires a versioned executable specification, exact properties and assumptions, tool, verification bounds and reproducible output. That package is not yet provided here.