`api_verify`

Rerun the available safety checks from the typed IR of the given Bosatsu sources. Reports which properties still hold after edits. Topology is an input: undeclared defaults to multi-instance, where RMW and interleaving findings are violations. Do not deploy unless proven is true.

Kind: Verify. Origin: Yichus/Mcp::catalog.

CLI: yichus api verify — the same safety proof over the same sources; the tool adds the instances argument the CLI takes as a flag.

Parameters

sources (required, array) — JSON array of {fileName, source} Bosatsu files for the API module.
instances (optional, string) — Deployment topology: 1 for a single engine instance, many (default) for multiple instances sharing one DB.

Example

This response was produced by calling this tool with the displayed request when these docs were generated. Analysis examples use the owner-scoped notes specimen; scaffold examples supply a resource specification.

Request

{
  "sources": [
    {
      "fileName": "notes-api.bosatsu",
      "source": "package Demo/Service/NotesApi\n\n# Owner-scoped notes API. One row per caller, keyed by Principal.user_id.\n# `yichus api verify` / api_access_check prove the scoping from Matchless IR.\n\nfrom Yichus/IO import IO, flat_map\nfrom Yichus/Access import Principal, AccessRule, AccessSpec, OwnerScoped\nfrom Yichus/Data import Db, Table, table, db_read, db_write, db_delete\nfrom Yichus/Service import handler, route, service_def, ReadPerm, WritePerm, DeletePerm\n\nexport (notes_api, access_rules, Note())\nexposes (Yichus/Access, Yichus/Service)\n\nstruct Note(title: String)\n\naccess_rules = AccessSpec([\n  AccessRule(\"notes\", OwnerScoped),\n])\n\ndef notes_table(db: Db) -> Table[List[Note]]:\n  table(db, \"notes\")\n\ndef list_notes(db: Db, p: Principal) -> IO[List[Note]]:\n  Principal(uid, _) = p\n  db_read(notes_table(db), uid)\n\ndef put_notes(db: Db, p: Principal, items: List[Note]) -> IO[List[Note]]:\n  Principal(uid, _) = p\n  db_write(notes_table(db), uid, items)\n\ndef add_note(db: Db, p: Principal, item: Note) -> IO[List[Note]]:\n  Principal(uid, _) = p\n  items <- flat_map(db_read(notes_table(db), uid))\n  db_write(notes_table(db), uid, [item, *items])\n\ndef clear_notes(db: Db, p: Principal) -> IO[Unit]:\n  Principal(uid, _) = p\n  db_delete(notes_table(db), uid)\n\nnotes_api = service_def(\n  \"notes\",\n  [\n    route(\"/notes\", handler(\"list_notes\", list_notes), [ReadPerm(\"notes\")]),\n    route(\"/notes/put\", handler(\"put_notes\", put_notes), [WritePerm(\"notes\")]),\n    route(\"/notes/add\", handler(\"add_note\", add_note), [ReadPerm(\"notes\"), WritePerm(\"notes\")]),\n    route(\"/notes/clear\", handler(\"clear_notes\", clear_notes), [DeletePerm(\"notes\")]),\n  ]\n)\n"
    }
  ],
  "instances": "1"
}

Response

{
  "ok": true,
  "tool": "api_verify",
  "topology": "single-instance",
  "verdict": {
    "artifactClass": "api-safety-1.0",
    "schemaVersion": "api-safety-1.0",
    "sources": {
      "hash": "246f6f0eb42eff551b73f10f1fb86d539c9cdb5d979e980d5bc67f079d7b77c3",
      "files": [
        {
          "name": "notes_api",
          "sha256": "fc78988841dc4584fb3dce5d210bb363af6c7cf40553bdbc3ed1ebde53009d08"
        }
      ]
    },
    "proven": true,
    "properties": [
      {
        "id": "compiles",
        "title": "Parses and type-checks",
        "status": "proven",
        "details": []
      },
      {
        "id": "access-spec-declared",
        "title": "Access rules declared or storage absence established",
        "status": "proven",
        "details": [
          "notes: OwnerScoped"
        ]
      },
      {
        "id": "access-coverage",
        "title": "Every DB operation covered by a declared rule",
        "status": "proven",
        "details": []
      },
      {
        "id": "access:notes",
        "title": "\"notes\": each user reads and writes only their own rows",
        "status": "proven",
        "details": [
          "Demo/Service/NotesApi::list_notes db_read on \"notes\": key derives from the authenticated Principal (user_id or owner_key)",
          "Demo/Service/NotesApi::put_notes db_write on \"notes\": key derives from the authenticated Principal (user_id or owner_key)",
          "Demo/Service/NotesApi::add_note db_read on \"notes\": key derives from the authenticated Principal (user_id or owner_key)",
          "Demo/Service/NotesApi::add_note db_write on \"notes\": key derives from the authenticated Principal (user_id or owner_key)",
          "Demo/Service/NotesApi::clear_notes db_delete on \"notes\": key derives from the authenticated Principal (user_id or owner_key)"
        ]
      },
      {
        "id": "route-permissions",
        "title": "Route permissions match handler effects",
        "status": "proven",
        "details": [
          "/notes -> list_notes: match",
          "/notes/put -> put_notes: match",
          "/notes/add -> add_note: match",
          "/notes/clear -> clear_notes: match"
        ]
      },
      {
        "id": "route-authority",
        "title": "Route authority declarations are enforceable",
        "status": "proven",
        "details": [
          "/notes: authenticated",
          "/notes/add: authenticated",
          "/notes/clear: authenticated",
          "/notes/put: authenticated"
        ]
      },
      {
        "id": "rmw-transactions",
        "title": "Handlers that read then write cannot lose updates",
        "status": "warning",
        "details": [
          "Demo/Service/NotesApi::add_note reads then writes \"notes\"; with multiple instances on one DB, run this handler in a transaction (or a single-writer queue) to avoid lost updates (accepted: instances=1 declared; one instance runs each request's IO plan atomically)"
        ],
        "accepted": "instances=1"
      },
      {
        "id": "integrity",
        "title": "Concurrent requests keep the data consistent",
        "status": "warning",
        "details": [
          "race-free:notes: 6 valid orderings over 'notes' produce differing effect sequences (accepted: instances=1 declared; one instance runs each request's IO plan atomically)"
        ],
        "accepted": "instances=1"
      }
    ],
    "errors": []
  },
  "narrative": "'Parses and type-checks' is proven, where proven means established by a known-good method for every input.\n'Access rules declared or storage absence established' is proven. Details: notes: OwnerScoped.\n'Every DB operation covered by a declared rule' is proven.\n'\"notes\": each user reads and writes only their own rows' is proven. Details: Demo/Service/NotesApi::list_notes db_read on \"notes\": key derives from the authenticated Principal (user_id or owner_key); Demo/Service/NotesApi::put_notes db_write on \"notes\": key derives from the authenticated Principal (user_id or owner_key); Demo/Service/NotesApi::add_note db_read on \"notes\": key derives from the authenticated Principal (user_id or owner_key); Demo/Service/NotesApi::add_note db_write on \"notes\": key derives from the authenticated Principal (user_id or owner_key); Demo/Service/NotesApi::clear_notes db_delete on \"notes\": key derives from the authenticated Principal (user_id or owner_key).\n'Route permissions match handler effects' is proven. Details: /notes -> list_notes: match; /notes/put -> put_notes: match; /notes/add -> add_note: match; /notes/clear -> clear_notes: match.\n'Route authority declarations are enforceable' is proven. Details: /notes: authenticated; /notes/add: authenticated; /notes/clear: authenticated; /notes/put: authenticated.\n'Handlers that read then write cannot lose updates' is warning, where warning means established only under a disclosed acceptance, which the details name. Details: Demo/Service/NotesApi::add_note reads then writes \"notes\"; with multiple instances on one DB, run this handler in a transaction (or a single-writer queue) to avoid lost updates (accepted: instances=1 declared; one instance runs each request's IO plan atomically).\n'Concurrent requests keep the data consistent' is warning. Details: race-free:notes: 6 valid orderings over 'notes' produce differing effect sequences (accepted: instances=1 declared; one instance runs each request's IO plan atomically)."
}

Run tools in the browser: api-mcp.html?webmcp=1.

Read the result according to this tool’s scope: static checks, bounded execution checks, and descriptive diagrams answer different questions. A successful call is not a general approval of the program. The safety and permissions guide compares the checks and provides editable ownership, guard, and role examples.