Skip to main content
Glama
Sign In

AILANG Executor

by io.github.sunholo-data
OverviewDiscussionsAdmin

Check AILANG code

ailang_check
Read-onlyIdempotent

Type-check AILANG source. code is a whole module; the module line may be omitted or be module main. Returns the ai-check JSON report on stdout: check.passed and check.errors (with locations and fixes), and verify: each function's requires/ensures proved with Z3 (verify.results: verified, counterexample with a witness, or inconclusive after 5s per function). Only pure functions (or ! {}) are proved; others report skipped/NOT_PURE. verification names the overall result; "unavailable" means this server had no solver, so the code was type-checked only and its contracts were not proved (prove them locally with ailang verify).

Tool call template

Replace each placeholder with a value matching the input schema. Only required parameters are included; add optional parameters as needed.

{
  "id": 1,
  "jsonrpc": "2.0",
  "method": "tools/call",
  "params": {
    "arguments": {
      "code": "<code>"
    },
    "name": "ailang_check"
  }
}

Input Schema

NameRequiredDescriptionDefault
codeYes

Schema Changelog

Changes observed during successful MCP inspections.

  1. First observed

TDQS

A4.1/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Adds substantial behavior beyond the annotations: it names the output shape (ai-check JSON on stdout), the key fields (check.passed, check.errors with locations and fixes), the Z3 verification flow with a per-function 5s timeout, the possible per-function outcomes (verified, counterexample with witness, inconclusive), and the NOT_PURE/skipped rule for non-pure functions. It also explains what 'unavailable' means operationally and what the agent should do instead. That is exactly the kind of context annotations cannot carry.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Front-loaded with the core action and the input requirement, then the return contract, then the verification caveat — a sensible order. The parenthetical asides and quoted field names make it dense but every clause conveys real information. Slightly heavy for a single-parameter tool, but nothing is filler.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Complete for a checker tool with no output schema: the description documents both the type-check portion and the verification portion of the response, plus the degraded mode when no solver is present. An agent can predict what it will get back and interpret 'unavailable' or NOT_PURE without further probing.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 0%, so the description carries the burden for the single `code` parameter. It does so well by specifying that `code` is a whole module and that the module header is optional or `module main` — semantics the bare string schema cannot convey. It does not discuss size limits or multi-module input, keeping it just under a 5.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

States a specific verb and resource: 'Type-check AILANG source.' That is clearly distinct from running or evaluating siblings, and the description keeps the focus on static checking plus contract verification. It stops short of naming an alternative tool, which is the only thing separating it from a 5.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Usage is implied rather than stated: it explains that `code` must be a whole module and that the module line may be omitted or set to `module main`. It also tells the agent what to do when verification is 'unavailable' (prove locally with `ailang verify`). But there is no explicit 'use this when…' versus aliLang_run/ailang_eval, so the agent has to infer the boundary.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

All AILANG Executor toolsInspect
Try in Browser
One endpoint for every MCP toolRayrun runs every MCP server behind one URL and holds the credentials. Each call is decided per client, tool, and argument, then recorded.ray.runAd

Glama MCP Gateway

Add one secure layer between your agents and this server.

Resources