Skip to main content

IETF Autoformalization Plan

Status: Phase 0 complete; Phase 2 (RFC 8555) complete
Created: 2026-07-06

Summary​

This initiative autoformalizes normative IETF protocol behavior into Modality contracts: temporal modal logic rules plus a synthesized governing model. The goal is verifiable governance over protocol events — who may perform which signed action, in what order, with what attestations — not wire-format or cryptographic implementation.

Modality's existing two-step pipeline (NL → formulas → model → verify) maps naturally onto RFCs whose correctness is expressed as role-bound state machines with MUST/SHALL ordering.

Scope boundary: We formalize cooperation obligations between named parties. We do not formalize message encoding, timers, retransmissions, or crypto primitives.

Fit Criteria​

Good fit​

RFC characteristicModality mapping
Defined roles (client, issuer, arbiter…)/users/*.id, signed_by predicates
Documented state machinegoverning model
MUST/SHALL ordering ("authorize before issue")always([+X] true -> eventually(<+Y> true))
Irrevocable commitments[<+ACTION>] (diamondbox)
External evidence (attestation, deadline)oracle_attests
Append-only audit trailcontract commit log (native)

Poor fit​

CategoryExamplesWhy
Transport layersTLS 1.3, QUICCrypto and loss recovery, not party obligations
Data formatsJWT, CBOR, UUIDSyntax, not behavioral contracts
Timing semanticsSIP retransmissions, ICEContinuous/real-time, hard to express in LTS
Bit-accurate wire specsHTTP/2 framesEncoding correctness, not cooperation

When an RFC mixes both (e.g. ACME), extract only the normative core — roles, states, ordering, authorization — and explicitly mark wire/crypto sections out of scope.

Pipeline​

Five-step methodology, aligned with experiments/llm-synthesizer/pipeline.md:

RFC normative core → NL obligations → MTL formulas → synthesized LTS → model checker

Step 1: Extract normative core​

From the RFC, collect:

  • Parties and their responsibilities
  • States (explicit or implied FSM)
  • Actions (events that change protocol state)
  • MUST/SHALL rules involving ordering or authorization
  • Evidence requirements (attestations, prior steps)

Use the checklist in experiments/ietf-autoformalization/methodology.md.

Step 2: Translate to NL obligations​

Rewrite each MUST rule as a plain-language obligation between parties:

  • "The authorization server MUST NOT issue a token until the user completes authorization"
  • "Only the account holder may finalize an order"

Avoid implementation detail. One obligation per candidate formula.

Step 3: Generate MTL formulas​

LLM-assisted conversion using patterns in rust/modality-lang/src/llm_synthesis.rs. Human review required before synthesis.

Example patterns:

always([+FINALIZE] true -> eventually(<+COMPLETE_AUTHORIZATION> true))
always([+FINALIZE] true -> <+signed_by(/users/account_holder.id)> true)
always([+REVOKE] true -> always([-USE_CERTIFICATE] true))

Step 4: Synthesize model​

Run formula synthesis via rust/modality-lang/src/formula_synthesis.rs (synthesize_from_formulas). The model is a witness; formulas remain the specification.

Step 5: Verify and iterate​

  • Model checker confirms M ⊨ F1 ∧ F2 ∧ …
  • On failure: refine formulas first, then re-synthesize
  • Document counterexamples and resolution in per-RFC synthesis-notes.md (Phase 1+)

Tier-1 RFC Catalog​

Corpus location: experiments/ietf-autoformalization/

DirectoryRFCFocusPilot order
rfc8628-device-authorizationRFC 8628Device authorization grant FSM1 (smallest)
rfc8555-acmeRFC 8555Certificate issuance lifecycle2
rfc8693-token-exchangeRFC 8693Delegation / act-on-behalf-of3
rfc7644-scimRFC 7644Identity provisioning lifecycle4
rfc9334-ratsRFC 9334Remote attestation → appraisal4
rfc9421-http-message-signaturesRFC 9421HTTP request-signing policy5

Phased Roadmap​

PhaseStatusDeliverable
0CompleteThis plan + corpus stubs
1PendingComplete RFC 8628: filled normative core, real rules, synthesized model, verification notes
2CompleteRFC 8555 ACME contract + corpus regression test
3PendingRFC 8693 delegation contract (agent-cooperation demo)
4PendingRFC 9334 RATS + RFC 7644 SCIM (oracle + lifecycle patterns)
5PendingCLI integration (modality model synthesize --rfc <id>) or corpus regression tests

Reference contracts for patterns: examples/escrow_enforced.modality, experiments/agent-service-contract.modality.

Repository Layout​

docs/progress/
└── IETF_AUTOFORMALIZATION_PLAN.md     # this document

experiments/ietf-autoformalization/
├── README.md
├── methodology.md
├── rfc8628-device-authorization/
│   ├── README.md
│   ├── normative-core.md
│   └── rules.modality.stub
├── rfc8555-acme/
│   ├── model/default.modality
│   ├── rules/governance.modality
│   ├── normative-core.md
│   └── synthesis-notes.md
├── rfc8693-token-exchange/
├── rfc7644-scim/
├── rfc9334-rats/
└── rfc9421-http-message-signatures/

Phase 1+ adds per-RFC: rules/*.modality, model/default.modality, synthesis-notes.md.

Future CLI (Phase 5):

modality model synthesize --rfc 8628 --verify

Success Metrics​

MetricTarget (Phase 1 pilot)Target (Phase 5)
Model checker pass rate on tier-1 corpus1/6 RFCs verified6/6 RFCs verified
Formulas per RFC (normative core)5–15Stable, reviewed set
Manual review time per RFC< 2 hours< 30 min with tooling
Synthesis without manual model edit≥ 80% of formulas≥ 95%
False positives (over-constrained model)Document and refineRegression-tested

Open Questions​

  1. Oracle binding for RATS: How do oracle_attests predicates map to real attestation evidence without formalizing TPM quote formats?
  2. OAuth scope: Formalize token-issuance governance only, or also scope/audience constraints as state?
  3. RFC versioning: How do we track RFC updates and maintain corpus compatibility?
  4. Partial formalization: Is a "governance slice" of a larger RFC sufficient for agent trust use cases?
  5. Regression corpus: Should tier-1 RFCs become permanent synthesis benchmarks in rust/modality-lang tests?