Mayfly

Natural language in. Formally verified APIs out.

Agents and chat can understand what you want from your data. What they can't do safely is act on it — you can't hand an LLM a live database connection, and you can't hand-build an API ahead of time for every request someone might make.

Mayfly is the missing piece. An agent (or a person, in chat) describes a capability it needs; Mayfly synthesizes a contract, proves it safe against your policy, and hands back a deterministic, typed, ephemeral endpoint. The model produces the what; a proof guarantees the safe; a plain query does the work. The LLM never touches your data, and it's out of the loop the instant the endpoint exists.

The sharpest case is writes. "Bulk-reassign these deals" is exactly where raw text-to-SQL is too dangerous to allow and a hand-built API doesn't exist yet. Mayfly turns it into a one-glance, human-approvable, provably-bounded capability:

"Reassign my stale deals over $50k to Priya — no more than 100 at a time."

POST /ephemeral/reassign-stale         TTL: 1h        ⚠ needs approval
├─ reads  deals(id, value, owner)   scope: team_id = caller.team_id
├─ writes deals(owner)  ≤ 100 rows  pk-pinned · re-scoped to caller
└─ ✓ VERIFIED  tenant-isolated (Z3 proof) · bounded write · no PII egress

You approve a verified spec, not a paragraph of model output — and once approved it's a deterministic tool the agent can call, not a fresh roll of the dice each time.

Try it in 30 seconds

No database, no API key, no config:

npx mayfly-api demo              # try it instantly
# or install the CLI globally — the command is `mayfly`:
npm install -g mayfly-api

The npm package is mayfly-api; the CLI command it installs is mayfly.

Using an AI agent? One command wires Mayfly in as an MCP tool — try it on the demo with zero setup:

npx -y mayfly-api install --demo   # writes .mcp.json; restart your agent

Then the agent has conjure_endpoint / call_endpoint / … See Agent setup (there's a copy-paste block you can hand straight to Claude Code) and AGENTS.md.

Want it wired into your own app? First, let Mayfly read your schema so you confirm the boundary instead of guessing it:

npx -y mayfly-api inspect --db "$DATABASE_URL"   # detected tenant column, PII, unscoped tables

Then it's one call to construct — no config file, no schema editing:

import { Mayfly } from "mayfly-api";

const mayfly = await Mayfly.create({
  db: process.env.DATABASE_URL,          // postgres:// | mysql:// | sqlite path
  tenantColumn: "org_id",                // the column that scopes rows per tenant
  pii: ["users.email", "api_keys.secret"], // columns that must never leave
});

// per request, scoped to the caller's tenant (from your auth, never request input):
const r = await mayfly.conjure("archive my done projects", { caller: { org_id: session.orgId } });
// autonomous: it verified, so it's live — the proof is the gate, no approval step.
await mayfly.call(r.endpoint.id, { caller: { org_id: session.orgId }, path: "/bulk-update", params: { new_value: "archived" } });

Or let a coding agent do the whole integration — paste into Claude Code / Cursor:

Set up mayfly-api in this project: run npx -y mayfly-api guide and follow the playbook it prints — detect my stack, DB, and how I identify the current tenant; wire that as Mayfly's caller context; add a demo verified read and a bounded write; then tell me how to test.

The result: one conjured endpoint serves every tenant, and Mayfly proves each call can't cross tenants — runnable reference here.

This scaffolds a sample CRM (SQLite), then walks you through the whole loop:

1. conjures a scoped read from a plain-language intent and prints the Z3 proof transcript,
2. calls the verified endpoint (the model is no longer in the loop),
3. watches the verifier reject two unsafe contracts — one missing tenant scope, one leaking PII — each with a concrete counterexample,
4. shows the append-only audit log.

Then point it at your own database — SQLite, Postgres, or MySQL:

mayfly init --db ./my.db                          # SQLite file
mayfly init --db postgres://user@host/mydb        # or a Postgres URL
mayfly init --db mysql://user@host/mydb           # or a MySQL URL
# tag pii/tenant columns in mayfly.catalog.json, then:
mayfly conjure "read-only endpoint for open deals by owner, expires in 1h"
mayfly serve --mcp                                # expose to an agent over MCP

init introspects your schema and seeds obvious PII/tenant tags; you review and adjust them. The same contract, verifier, and proofs run identically on either engine — only the SQL dialect (? vs $n) differs underneath.

New here? The Getting Started guide walks from zero to an agent conjuring its own bounded write capability.

Is this for you?

Reach for Mayfly when:

• an agent needs to act on production data — read, compute, and especially write — and you can't pre-build a tool for every request it might make;
• chat-driven writes need to be safe: bounded, tenant-scoped, and human-approvable, not "trust the model's SQL";
• capabilities should expire — least privilege by default, standing access as the rare exception you grant on purpose;
• you want an auditable artifact (contract + proof + every call) instead of a query log you have to reverse-engineer.

Probably not what you want if you need a read-only BI dashboard over trusted internal users — a static layer like PostgREST or Hasura is simpler. Mayfly earns its keep where capabilities are created on demand and must be provably safe before they run — the agent-and-writes quadrant nothing off-the-shelf covers.

Why this exists

Every existing way of connecting LLMs to data makes a bad tradeoff:

| | Flexible (generated on demand) | Verifiable (auditable before execution) | |--------------------------|:---:|:---:| | Text-to-SQL | ✅ | ❌ every query is a fresh roll of the dice | | Static auto-APIs (PostgREST, Hasura) | ❌ predefined by a developer | ✅ | | Hand-written agent tools | ❌ | ✅ | | Code interpreters | ✅ | ❌ arbitrary code against your data | | Mayfly | ✅ | ✅ |

Mayfly is the missing quadrant. The LLM's output is never executed directly — it's an artifact: a typed schema with declared reads, writes, bounds, and scopes. Verification happens once, at creation time, not on every call. After that, the endpoint is deterministic. The model is in the loop when capability is created — never when data is accessed.

Formal verification, not vibes

"The LLM probably wrote a safe query" is not a security model. Mayfly makes safety a decidable check.

The verified surface of a contract — its reads, writes, filters, scopes, bounds, and egress schema — is a small specification language with no loops, no recursion, no dynamic dispatch, deliberately not Turing-complete, so verification always terminates. (A compose transform is arbitrary code, but it's never part of what's verified — it's made safe by containment; see Beyond queries.) Before an endpoint is instantiated, the verifier proves the contract satisfies your policy invariants:

• Tenant isolation — "every read and write is filtered by team_id = caller.team_id." This one is a real theorem, discharged by Z3: the verifier proves (⋀ filters) ⇒ (team_id = caller.team_id) by checking that (⋀ filters) ∧ (team_id ≠ caller.team_id) is UNSAT. If it's SAT, Z3 hands back the concrete row that would leak across tenants.
• No PII egress — "no column tagged pii may appear in any response schema." A decidable set check over the contract's declared read columns — not a regex over SQL strings.
• Bounded writes — "no write may affect more than N rows." Discharged by construction: the executor materializes at most maxRows primary keys before mutating, so the proven bound is enforced, not trusted.
• Temporal — "endpoints touching payments expire within 1 hour and require human approval for writes."

If the proof fails, you get a counterexample — the concrete input that would violate policy — which is fed back to the model to repair the contract, or surfaced to the human. Unverifiable endpoints never exist.

# policy/invariants.yaml
invariants:
  - type: no-pii-egress
    tag: pii
  - type: tenant-isolation
    column: team_id
    callerField: team_id
  - type: bounded-writes
    maxRows: 100
  - type: temporal
    tableTag: sensitive
    maxTtlSeconds: 3600
    requireApprovalForWrites: true

This is the core bet: generation is probabilistic, so execution must be provable. You don't trust the model. You trust the proof.

Ephemerality is the security model

Endpoints are born with a TTL and die on schedule. This isn't a quirk — it's least-privilege as a first-class primitive:

• Capabilities exist only while needed. Attack surface trends to zero at rest.
• Expired endpoints leave a complete audit log: who conjured it, the full contract, the proof transcript, every call made through it.
• Standing access becomes the exception you explicitly grant, not the default you forget to revoke.

Think of it as IAM for LLM–data interaction, where credentials are typed APIs and grants are theorems.

How agents use it (MCP)

Mayfly ships as an MCP server. Run mayfly serve --mcp and any MCP client (Claude, Cursor, LangGraph, your own harness) gets these tools:

| tool | what it does | |------|--------------| | conjure_endpoint(intent, ttl_seconds?) | synthesize → verify → instantiate; returns the endpoint + proof transcript, or counterexamples on failure | | call_endpoint(endpoint, path?, params?) | invoke a live endpoint — deterministic, typed, no model involved | | describe_endpoint(endpoint) | get the endpoint's OpenAPI 3.1 schema (typed params + responses, proof status) | | list_endpoints() | list live endpoints | | approve_endpoint(endpoint) | approve writes | | get_audit(limit?) | read the audit log |

Why this matters for agent reliability:

1. Determinism — conjure once, call 500 times. Same inputs, same outputs, until TTL.
2. Testability — you can write assertions against an endpoint. You cannot write assertions against "whatever the model generates next time."
3. Cost & latency — the expensive model call happens once at creation. Every subsequent call is a plain function/HTTP call.

How humans use it (chat / CLI / HTTP)

The same primitive. You ask for a capability; Mayfly shows you the contract — reads, writes, bounds, scopes, proof status — before anything executes. Writes require explicit approval by default. You're not approving prose; you're approving a verified spec.

mayfly conjure "bulk-reassign my stale deals to a new owner" --ttl 7200
#   ↳ prints contract + proof, endpoint is live but writes are gated
mayfly approve <endpoint-id>
mayfly call <endpoint-id> --param new_value=frank
#   ↳ ✓ 5 row(s) affected (bound ≤ 100)   — team-2 rows never touched

Or over HTTP:

mayfly serve --http --port 8787
curl -X POST localhost:8787/_mayfly/conjure -d '{"intent":"open deals over $50k"}'
curl localhost:8787/ephemeral/open-deals/list -H 'x-mayfly-caller: {"team_id":1}'

The contract language

A contract is a small JSON artifact. This is what the model emits and what the verifier proves — SQL is just a compilation target behind it.

{
  "name": "stale-deals",
  "ttlSeconds": 3600,
  "requiresApproval": false,
  "operations": [
    {
      "method": "GET", "path": "/list", "kind": "read",
      "table": "deals",
      "columns": ["id", "title", "value", "owner"],     // response schema (verified PII-free)
      "filters": [
        { "column": "team_id", "op": "=", "value": { "kind": "caller", "field": "team_id" } },
        { "column": "value",   "op": ">", "value": { "kind": "literal", "value": 50000 } }
      ],
      "limit": 200
    }
  ]
}

A value is a literal, a request param, or a caller field. Caller fields are bound server-side from trusted context and can never be overridden by request input — that's what makes tenant isolation real at execution, not just at proof time.

Verify a hand-written contract in CI:

mayfly verify my-contract.json    # exits non-zero if any obligation fails

Beyond queries: verified transformations

A real API isn't a SELECT — it joins, aggregates, extracts, reshapes, and often calls other services. Mayfly expresses this with a compose operation, and it stays safe through one idea:

Verify the capabilities, not the computation.

A compose op has three parts: scoped read handles (each a tenant-isolated, PII-free input — DB tables or external HTTP sources), an arbitrary transform (JavaScript the model wrote — untrusted), and a typed egress schema.

{
  "method": "GET", "path": "/report", "kind": "compose",
  "reads": [
    { "source": "table", "name": "deals",    "table": "deals",
      "columns": ["id","owner"], "filters": [/* team_id = caller.team_id */] },
    { "source": "http",  "name": "scores", "url": "https://api/scores",
      "scope": { "queryParam": "team_id", "callerField": "team_id" } }
  ],
  "transform": "(i) => { /* join, aggregate, bucket, reshape — anything */ }",
  "output": [ { "name": "owner", "type": "string" }, { "name": "revenue", "type": "int" } ]
}

The transform can be any code, because it runs in a hermetic WASM sandbox (QuickJS) with no process, no fetch, no require, no host access of any kind, and a bounded memory + instruction budget (so it can't exhaust the host or loop forever). It is handed only the scoped, PII-free inputs, and only its declared output fields are allowed to leave.

So the safety argument is structural, not a proof about the code:

• It can't leak another tenant's data — it was never handed it (every read handle is Z3-proven tenant-scoped).
• It can't leak PII — the PII column never entered the sandbox (read handles are proven PII-free), so egress is PII-free by containment.
• It can't smuggle fields out — anything not in the egress schema is dropped.
• It can't touch the host or run forever — the WASM boundary and the fuel limit forbid it.

This is the quadrant a code interpreter can't reach (it hands the model a live connection) and a database RLS layer can't reach (it can't sandbox a transformation or span two sources). Try it:

mayfly load examples/contracts/revenue-by-owner.json   # verify + instantiate a compose endpoint
mayfly call revenue-by-owner --path /report

Computed writes

A compose op can also write — the same containment principle, applied to mutation. It declares write handles (bounded, tenant-scoped mutation capabilities), and the transform returns write intents { handle, key, values } instead of touching the database:

"writes": [ { "name": "setStage", "target": "deals", "set": ["stage"], "maxRows": 100 } ],
"transform": "(i) => ({ writes: i.deals.filter(hot).map(d => ({ handle: 'setStage', key: d.id, values: { stage: 'hot' } })) })"

Every intent is funneled through its handle at execution: pinned to a primary key, re-scoped by team_id = caller.team_id, limited to the declared set columns, and capped at maxRows. So the untrusted transform can decide what to change but can't exceed the grant — a forged key from another tenant matches nothing, an undeclared column is ignored, and the bound holds no matter how many intents it emits. Writes require human approval by default.

mayfly load examples/contracts/mark-hot-deals.json     # a computed, bounded write
mayfly approve <endpoint-id>
mayfly call mark-hot-deals --path /recompute

Transports & typed clients

How you call an endpoint is a delivery detail below the contract — the proof and execution don't care. Two transports ship:

• MCP (mayfly serve --mcp) — the primary path for agents. conjure_endpoint / call_endpoint / describe_endpoint / approve_endpoint / get_audit as tools.
• HTTP + JSON (mayfly serve --http) — universally consumable by services, chat, and humans.

Because every endpoint carries a fully typed contract, Mayfly emits OpenAPI 3.1 for it — so you get typed, codegen-ready clients over plain HTTP without gRPC's static-proto mismatch with ephemeral, dynamically-shaped endpoints. The proof status rides along under x-mayfly, so a client (or an auditor) can see the endpoint was verified from the spec alone.

mayfly openapi <endpoint>                       # print the schema; pipe to any codegen
curl localhost:8787/_mayfly/openapi.json        # every live endpoint
curl localhost:8787/ephemeral/<name>/openapi.json

gRPC/binary transports would be an optional adapter for high-throughput internal service meshes — not a default, since a call is usually a bounded SQL round-trip where the DB dominates latency. Transport is pluggable; the contract is the constant.

Architecture

 intent (chat / MCP tool call)
        │
        ▼
 ┌──────────────┐   contract (typed spec: declared reads/writes/bounds/scopes)
 │  Synthesizer │──────────────┐          Claude if ANTHROPIC_API_KEY set,
 └──────────────┘              ▼          else a deterministic offline heuristic
        ▲              ┌──────────────┐   counterexample on failure
        └──────────────│   Verifier   │◄── policy invariants (Z3 / SMT)
         repair loop   └──────┬───────┘
                              │ proof ✓
                              ▼
                      ┌──────────────┐
                      │ Instantiator │── ephemeral endpoint + TTL + audit log
                      └──────────────┘
                              │
                              ▼
                   deterministic execution (SQLite / Postgres / MySQL)
                   (LLM is no longer in the loop)

Use it as a library, too:

import { Engine, loadProject } from "mayfly";

const engine = new Engine(loadProject());
const { ok, endpoint, verification } = await engine.conjure({
  intent: "open deals over $50k",
  ttlSeconds: 3600,
});
console.log(verification?.transcript);
const { result } = engine.call(endpoint!.id, {}, {}, { team_id: 1 });

What Mayfly is not

• Not text-to-SQL. SQL generation is an implementation detail behind the contract; the contract is what's verified and what executes.
• Not an agent framework. It's infrastructure below agents: a trust boundary between intent and data.
• Not a general code sandbox. Compose transforms do run arbitrary code — but in a hermetic WASM box with no host access, fed only capabilities that were proven safe first. The trust is in the boundary (scoped inputs, typed egress, fuel limits), never in the code.

Status & roadmap

Shipped in this release:

• [x] Contract language + typed policy invariants
• [x] Z3-backed tenant-isolation proofs with counterexamples
• [x] no-PII-egress, bounded-writes, and temporal invariants
• [x] SQLite, Postgres, and MySQL adapters (pluggable DbAdapter interface)
• [x] Ephemeral endpoints, TTL expiry, append-only audit log
• [x] MCP server, HTTP server, and CLI
• [x] Synthesizer: Claude (when ANTHROPIC_API_KEY is set) + deterministic offline fallback + verify/repair loop
• [x] Compose operations — transformations over scoped read handles (DB + HTTP) in a hermetic WASM sandbox, with a typed egress schema
• [x] Computed writes — transform-emitted write intents funneled through bounded, PK-pinned, tenant-scoped, human-approvable write handles
• [x] OpenAPI 3.1 emission per endpoint — typed clients over HTTP, with proof status under x-mayfly

Next:

• [ ] Richer egress refinement types
• [ ] Proof-carrying endpoint export (ship the contract and its proof to auditors)
• [ ] More source adapters for read handles (more SaaS APIs, gRPC)
• [ ] Endpoint promotion: graduate a battle-tested ephemeral API to a permanent one, proof intact

Contributions welcome — see CONTRIBUTING.md. Good first issues: a new database adapter, a new invariant kind, or a synthesizer backend.

License

Apache-2.0

Generation is probabilistic. Execution should be provable.