Skip to main content

Your First Contract

Let's make a tiny local contract together. You'll create Alice and Bob, put them on the contract, and add a rule so later commits have to be signed by one of them. If you don't know Modality syntax yet, modal ai suggest-rule can write the rule for you after you point Modal at your choice of AI.

If you only have a modality command so far, install modal from the installation guide first.

Copy and run the bash blocks. Click > next to a command to peek at expected output. IDs and commit hashes on your machine will look different, and that's expected.

1. Create a Contract​

modal contract create --dir ./my-first-contract
✅ Contract created successfully!
   Contract ID: 12D3KooW…
   Directory: ./my-first-contract
   Genesis commit: 436d6c47…

Next steps:
  1. cd ./my-first-contract
  2. Edit model/default.modality to define your state machine
  3. Add rules in rules/*.modality
  4. modal commit --all --sign your.modal_passfile

That created ./my-first-contract with a .contract/ directory and a starter model/default.modality file. Next we'll give Alice and Bob keys.

2. Create Identities​

modal id create --name example/alice
✨ Successfully created a new Modality ID!
📍 Modality ID: 12D3KooW…
💾 Modality Passfile saved to: ~/.modality/passfiles/example/alice.mod_passfile
🪪 Public ID saved to: ~/.modality/ids/example/alice.id

🚨🚨🚨  IMPORTANT: Keep your passfile secure and never share it! 🚨🚨🚨
modal id create --name example/bob
✨ Successfully created a new Modality ID!
📍 Modality ID: 12D3KooW…
💾 Modality Passfile saved to: ~/.modality/passfiles/example/bob.mod_passfile
🪪 Public ID saved to: ~/.modality/ids/example/bob.id

🚨🚨🚨  IMPORTANT: Keep your passfile secure and never share it! 🚨🚨🚨

Those are Alice and Bob. Named passfiles live in ~/.modality/passfiles/example/, and public IDs in ~/.modality/ids/example/. Keep the passfiles on your machine and don't commit them — they're private keys.

3. Add Identities to Contract State​

Now put Alice and Bob on the contract so the rule can name them.

cd my-first-contract
modal checkout
✅ Checked out 0 file(s)
modal set-named-id /parties/alice.id example/alice
✅ Set state/parties/alice.id from example/alice
   12D3KooW…
modal set-named-id /parties/bob.id example/bob
✅ Set state/parties/bob.id from example/bob
   12D3KooW…
modal status
Contract Status
═══════════════

  Contract ID: 12D3KooW…
  Directory:   ./my-first-contract
  Model state: init

  Local HEAD:  436d6c47…
  Remote HEAD: (none) [origin]
  Remote URL:  (not configured)

  Total commits: 1
  ℹ️  No remote tracking configured.

  Run 'modal push --remote <url>' to set up remote.

Changes in state/:
  + /parties/alice.id
  + /parties/bob.id

  Run 'modal commit --all' to commit changes.

Their public identities are in the working state, ready to commit.

4. Add Protection Rules​

Here's the heart of it: every commit after this one must be signed by either Alice or Bob. You still get one bootstrap commit that installs their identities and the first model. After that, unsigned updates are refused.

You don't need to know Modality syntax yet. Point Modal at your choice of AI first — OpenAI, Anthropic, Grok, AWS Bedrock, a local Ollama model, or the Cursor Agent CLI in this contract directory. See AI Commands for modal ai set. Then ask the CLI to suggest a rule:

modal ai suggest-rule "after this commit either alice or bob must sign"
[] always([-signed_by(/parties/alice.id) -signed_by(/parties/bob.id)] false)

That's example output — yours may differ. The rest of this guide uses the authorized formula below so lint and synthesize stay deterministic:

modal add-rule --name authorized \
  '[] always([-signed_by(/parties/alice.id) -signed_by(/parties/bob.id)] false)'
✅ Rule 'authorized' added to /rules/authorized.modality

export default rule {
  starting_at $PARENT
  formula {
    [] always([-signed_by(/parties/alice.id) -signed_by(/parties/bob.id)] false)
  }
}

Run 'modal commit --all' to commit this rule.

The [] prefix is why the bootstrap still works. Plain always(...) would constrain the current step too. [] always(...) skips that first commit so you can install identities and the model without a signature, then every later step has to be signed.

5. Synthesize a Witness Model​

Before you commit, turn the rule into a witness model — a small state machine that shows the rule is possible. For now, review the synthesized candidate and write it to model/default.modality.

modality model lint rules/authorized.modality
✅ 1 formula(s) lint-clean in rules/authorized.modality
modality model synthesize \
  --rule rules/authorized.modality \
  --verify \
  --review-bundle review/authorized.md \
  -o model/default.modality
✅ Synthesized model:

model Contract {
  part flow {
    q0 --> q1
    q1 --> q1: +signed_by(/parties/alice.id)
  }
}

The review bundle review/authorized.md is a paper trail. It keeps the rule file, parser-backed extracted facts, passed verifier result, witness model, assumptions, and known gaps so you can see why this model is safe to commit:

# Modality Synthesis Review Bundle
Status: passed (`--verify`)
## Extracted Facts
## Witness Model
modality model validate model/default.modality --verbose
🔍 Validating contract: model/default.modality

📋 Model: Contract
   Parts: 1
   Transitions: 2

✅ Contract is valid!
   All properties are predicates or commit method labels (verifier-observed).
modality model mermaid model/default.modality
stateDiagram-v2
    q0 --> q1
    q1 --> q1 : "+signed_by(/parties/alice.id)"
modality model view model/default.modality

That writes a temp HTML file with the same Mermaid diagram and opens it in your default browser.

Same picture, different view. The same witness as a state diagram:

modality model mermaid prints that Mermaid stateDiagram-v2 source from model/default.modality. modality model view opens the rendered diagram in your default browser.

The synthesizer returns a smallest satisfying witness: an unlabeled first step, then Alice's signature on the self-loop. That proves the rule is possible. It does not have to mention Bob. After this model is installed, the first commit can be unsigned. After that, only Alice can sign.

You may have noticed something off about the witness model. We'll come back to that.

6. Commit and Verify​

The first real commit is unsigned: identities, the rule, and the witness model. That's the bootstrap [] skipped. After it lands, you're in q1.

modal commit --all -m "Initial contract setup"
✅ Commit created successfully!
   Contract ID: 12D3KooW…
   Commit ID: 8f1c2a9b…
   Parent: 436d6c47…

Next steps:
  - modal status  (view status)
  - modal push    (push to chain)
modal status
Contract Status
═══════════════

  Contract ID: 12D3KooW…
  Directory:   ./my-first-contract
  Model state: q1

  Local HEAD:  8f1c2a9b…
  Remote HEAD: (none) [origin]
  Remote URL:  (not configured)

  Total commits: 2
  ℹ️  No remote tracking configured.

  ✅ state/ matches committed state.
modal log
Contract: 12D3KooW…
Commits: 2

commit 8f1c2a9b12ab (8f1c2a9b...)
Parent: 436d6c47eef4...
Message: Initial contract setup
Signatures: 0
Actions:
  post /parties/alice.id
  post /parties/bob.id
  rule /rules/authorized.modality
  model /model/default.modality

That's the first real commit. The accepted rule, witness model, and synthesis review bundle are the local files that explain what happens next. Keep rules/authorized.modality, model/default.modality, and review/authorized.md with the contract. If a later commit is rejected, those files stay put — a rejected commit does not alter those accepted artifacts.

7. Prove the Rule Is Active​

Let's prove it. First, a normal signed update from Alice:

modal commit \
  --path /notes.text \
  --value "signed update" \
  --sign example/alice \
  -m "Signed update"
✅ Commit created successfully!
   Contract ID: 12D3KooW…
   Commit ID: c3e91d04…
   Parent: 8f1c2a9b…

Next steps:
  - modal status  (view status)
  - modal push    (push to chain)
modal status
  Model state: q1
  Total commits: 3
modal log
Message: Signed update
Signatures: 1
Signers:
  12D3KooW…

That should go through. Now try the same kind of update without a signature:

modal commit \
  --path /unsigned.text \
  --value "unsigned update" \
  -m "Unsigned update"
Error: No valid transition for local commit from current states {"q1"}
Closest candidate transition: candidate from current state q1: q1 --> q1 [+signed_by(/parties/alice.id)]; failed predicates: missing +signed_by(/parties/alice.id)
Candidate transitions ranked by predicate distance:
candidate from current state q1: q1 --> q1 [+signed_by(/parties/alice.id)]; failed predicates: missing +signed_by(/parties/alice.id)

That's the rule doing its job from rules/authorized.modality. The unsigned commit never landed.

modal status
  Total commits: 3
  Model state: q1
modal log
Message: Signed update

The log should still end at the last accepted signed update. Nothing unsigned snuck in.

Replay the working files and check that Alice's note is still there:

modal checkout
cat state/notes.text
✅ Checked out 1 file(s)
   state/
     /notes.text
     /parties/alice.id
     /parties/bob.id

signed update
ls state/unsigned.text
ls: state/unsigned.text: No such file or directory

The accepted rules/authorized.modality, model/default.modality, and review/authorized.md files should also be unchanged. That's the contract holding its shape.

When a rejection names current states {"q1"}, read the rest of the message against that accepted witness state first. If the verifier also shows similar transitions from other states, those are state-mismatch hints for review; they are not alternative ways the rejected commit could have landed.

8. Let Bob Replace the Witness​

That something off from step 5: the synthesized witness only lets Alice sign. The rule names Alice or Bob. Bob can sign, but this machine has no arrow for him.

Have Bob try a signed commit with nothing else in it. The rule should accept his signature. The witness is what gets in the way:

modal commit --sign example/bob -m "Bob tries to commit"
Error: No valid transition for local commit from current states {"q1"}
Closest candidate transition: candidate from current state q1: q1 --> q1 [+signed_by(/parties/alice.id)]; failed predicates: missing +signed_by(/parties/alice.id)
Candidate transitions ranked by predicate distance:
candidate from current state q1: q1 --> q1 [+signed_by(/parties/alice.id)]; failed predicates: missing +signed_by(/parties/alice.id)

The closest candidate is Alice's arrow. The rule itself does let him. It only says later commits must be signed by Alice or Bob:

[] always([-signed_by(/parties/alice.id) -signed_by(/parties/bob.id)] false)

It does not mention POST or MODEL, and it does not lock the witness to Alice. The matching witness keeps the unlabeled bootstrap, then one signed Alice transition and an alternative signed Bob transition:

cat > model/default.modality <<'EOF'
model Contract {
  part flow {
    q0 --> q1
    q1 --> q1: +signed_by(/parties/alice.id)
    q1 --> q1: +signed_by(/parties/bob.id)
  }
}
EOF
modality model validate model/default.modality --verbose
📋 Model: Contract
   Parts: 1
   Transitions: 3

✅ Contract is valid!

The same witness as a state diagram, now with a signed Alice move or a signed Bob move:

modal commit --all --sign example/bob -m "Let Bob replace the witness"
✅ Commit created successfully!
   Contract ID: 12D3KooW…
   Commit ID: a91e4c22…
   Parent: c3e91d04…
modal status
  Model state: q1
  Total commits: 4
modal log
Message: Let Bob replace the witness
Signatures: 1
Actions:
  model /model/default.modality

That replacement landed because the candidate model can replay the accepted history, still satisfies the rule, and now has a signed Alice transition or a signed Bob transition from q1. The old witness was a proof that the rule is possible, not a lock on Alice. The rule stayed put. Bob replaced the witness.

What's Next?​