Corvid is a general-purpose programming language built for AI-native software.
Python, TypeScript, Rust, Go, and JavaScript can call models through libraries. Corvid makes the AI parts visible to the compiler: agents, tools, prompts, approvals, grounding, budgets, confidence, model routing, streaming, replay, and verification are language constructs.
The goal is not to be a RAG DSL. The goal is a real language for CLIs, servers, data pipelines, automation, embedded hosts, and AI agents where the compiler understands the parts of the program that spend money, call models, cross approval boundaries, stream partial results, and act on a user's behalf.
effect transfer_money:
cost: $0.50
trust: human_required
reversible: false
tool issue_refund(id: String) -> Receipt dangerous uses transfer_money
@budget($1.00)
@trust(human_required)
agent refund(id: String) -> Receipt:
approve IssueRefund(id)
return issue_refund(id)
Remove the approve line and the program does not compile. Increase the composed cost above $1.00 and the program does not compile. Return Grounded<T> without retrieval provenance and the program does not compile. That is the point: AI safety is not an SDK convention; it is part of the language.
Install (Windows PowerShell — macOS / Linux below):
curl -fsSL https://raw.githubusercontent.com/Micrurus-Ai/Corvid-lang/main/install/install.sh | shOfficial installers also detect VS Code, Cursor, VSCodium, and Windsurf
and install the bundled Corvid extension automatically. Opening a .cor
file therefore gets syntax highlighting and language support immediately.
Set CORVID_SKIP_EDITOR_EXTENSION=1 only when editor integration is not
wanted.
First program:
corvid new hello
cd hello
corvid runThen explore:
- The 5-minute quickstart in the book
- The shipped invention tour:
corvid tour --list - The full book index
For the full install options (Windows PowerShell, custom paths,
env overrides, cargo install from source, planned package-
manager paths), see Install below.
- Verifiable launch surface — signed cdylib +
claim --explain - Invention catalog — every shipped invention with proof matrix
- Architecture
- Status
- Install
- Install from source
- Developer commands
- Documentation
- License
Corvid's strongest production claim is not prose; it is a signed cdylib workflow that emits externally checkable artifacts:
cargo run -q -p corvid-cli -- build app.cor --target=cdylib --sign=key.hex
cargo run -q -p corvid-cli -- claim --explain target/release/libapp.so --key pub.hex --source app.cor
cargo run -q -p corvid-abi-verify -- --source app.cor target/release/libapp.so
cargo run -q -p corvid-cli -- receipt verify-abi target/release/libapp.so --key pub.hexThose commands are the public claim boundary:
corvid build --signrefuses to sign when source-declared contracts are not covered by registered, non-out_of_scopeguarantee ids.- The cdylib embeds
CORVID_ABI_DESCRIPTORand, when signed,CORVID_ABI_ATTESTATION. corvid claim --explainprints the descriptor-carried guarantee ids, signing-key fingerprint, and source/binary descriptor agreement when--keyand--sourceare supplied.corvid-abi-verifyrebuilds the ABI descriptor from source through a separate process and byte-compares it with the cdylib's embeddedCORVID_ABI_DESCRIPTOR(catches post-link tampering and build-cache drift; full second-implementation TCB shrinkage is post-v1.0).corvid receipt verify-abiverifies the DSSE attestation and descriptor match.
For the exact trust boundary and non-goals, read docs/security/model.md. For the canonical guarantee table, read docs/reference/core-semantics.md.
Run the shipped invention tour:
cargo run -q -p corvid-cli -- tour --list
cargo run -q -p corvid-cli -- tour --topic approve-gatesThe tour demos are compiler-checked in CI-style tests, so the catalog below is not detached marketing copy.
Each entry has a runnable tour topic, a spec link, a roadmap pointer, a test pointer, and an explicit non-scope. Corvid should be ambitious, but every claim below is tied to shipped source.
Dangerous tools are not hidden behind decorators. The compiler requires an explicit approval boundary before irreversible actions.
This makes "approval happened before action" a type/effect property instead of a runtime best effort.
tool issue_refund(id: String) -> Receipt dangerous
agent refund(id: String) -> Receipt:
approve IssueRefund(id)
return issue_refund(id)
Spec: typing rules
Tour: corvid tour --topic approve-gates
Roadmap: Phase 20 safety wave
Proof: approval checker tests
Non-scope: Corvid proves the approval boundary exists; it does not decide whether approval is morally or legally correct.
For served applications, an approval boundary also requires a verified requester and a complete route policy. If a route can reach approve—directly or through called agents—but omits requires authenticated or any @approval(...) field, the compiler rejects it. Reviewer role, risk, data class, expiry, cost ceiling, and reversibility come from source and travel through the Application Contract into the queue; serve invents none of them. At decision time Corvid verifies that the reviewer holds the exact declared role plus approvals.decide, in the same tenant, with valid CSRF, and is not the requester.
server payments:
@approval(role: "finance_reviewer", risk: "financial_transfer", data: "financial", expires_ms: 600000, max_cost_usd: $2500.0, irreversible: true)
route POST "/payments" body Payment -> json Receipt requires authenticated:
return submit_payment(body)
Effects are not flat tags. Cost, trust, reversibility, data, latency, confidence, and user-defined dimensions compose through their own algebra.
That lets the compiler reason about AI workflows as resource- and authority-carrying programs, not just function calls.
effect llm_call:
cost: $0.05
trust: autonomous
prompt summarize(text: String) -> String uses llm_call:
"Summarize {text}"
@budget($0.10)
@trust(autonomous)
agent summarize_twice(text: String) -> String:
first = summarize(text)
return summarize(first)
Spec: composition algebra
Tour: corvid tour --topic dimensional-effects
Roadmap: Phase 20a and Phase 20g
Proof: effect composition tests
Non-scope: Declared effects are compiler contracts; external providers still need operational verification.
Grounded<T> means the value must flow from a retrieval source. The typechecker rejects grounded returns without a provenance chain.
At runtime the value carries its provenance, so later prompts and traces can inspect where the answer came from.
effect retrieval:
data: grounded
tool fetch_doc(id: String) -> Grounded<String> uses retrieval
agent research(id: String) -> Grounded<String>:
return fetch_doc(id)
Spec: grounding
Tour: corvid tour --topic grounded-values
Roadmap: Phase 20b
Proof: grounded effect tests
Non-scope: Grounding proves source linkage, not that the source itself is true.
A prompt can name the grounded context it must cite. The compiler proves the cited parameter is grounded, and runtime checks the model response.
That turns "please cite your sources" from prompt text into a checked contract.
prompt answer(ctx: Grounded<String>) -> Grounded<String>:
cites ctx strictly
"Answer from {ctx}"
Spec: grounding and citation contracts
Tour: corvid tour --topic strict-citations
Roadmap: Phase 20b cites ctx strictly
Proof: VM citation tests
Non-scope: Citation checks textual evidence, not the truth of the cited document.
Grounded values stay grounded as they flow through ordinary code. Add a Grounded<String> to a plain String, pass it as a call argument, return it through a branch — the wrapper carries through and the runtime delivers what the type promises.
Mark an agent @grounded_pure and the compiler refuses to launder. Every silent Grounded<T> -> T coercion, every .unwrap_discarding_sources(), every call into an agent that isn't itself @grounded_pure — all rejected at compile time. The moat composes through the call graph the same way @deterministic does.
effect retrieval:
data: grounded
prompt audit() -> String uses retrieval:
"Audit"
# `+` lifts `String + Grounded<String>` to `Grounded<String>`
# via the contagion law; the wrapper rides through to return.
@grounded_pure
agent run() -> Grounded<String>:
head = "Summary: "
tail = audit()
return head + tail
Spec: grounded propagation design
Tour: corvid tour --topic provenance-propagation
Roadmap: Provenance Propagation phase
Proof: proof tests + corpus fixtures (grounded_pure_* + tests/corpus/combined_all.cor, tests/corpus/legacy_grounded_coercion.cor)
Non-scope: @grounded_pure forbids laundering inside an agent's body; it does not validate that the cited source is truthful (citation contracts handle one layer; trust in the upstream retrieval is the operator's responsibility).
@budget is a static constraint over composed declared cost. The compiler rejects workflows whose worst-case cost exceeds the bound.
Cost becomes part of the program contract instead of a surprise on the provider invoice.
effect cheap_call:
cost: $0.05
prompt classify(text: String) -> String uses cheap_call:
"Classify {text}"
@budget($0.10)
agent bounded(text: String) -> String:
first = classify(text)
return classify(first)
Spec: cost budgets
Tour: corvid tour --topic cost-budgets
Roadmap: Phase 20d
Proof: cost analysis tests
Non-scope: Static budgets use declared costs; provider billing reconciliation is still an operational concern.
Confidence is a first-class dimension with weakest-link composition. Agents can require a floor before acting autonomously.
Low-confidence paths can route into approval instead of silently pretending every model answer is equally reliable.
effect llm_decision:
confidence: 0.95
@min_confidence(0.90)
agent bot(query: String) -> String:
return search(query)
Spec: confidence gates
Tour: corvid tour --topic confidence-gates
Roadmap: Phase 20e
Proof: minimum confidence tests
Non-scope: Confidence only means something when model adapters report calibrated signals.
agent, tool, prompt, effect, approve, model, eval, and streaming constructs are syntax the compiler understands.
The language stays general-purpose, but the AI boundaries are visible instead of buried in framework calls.
model local:
capability: basic
prompt say(name: String) -> String:
requires: basic
"Hello {name}"
agent hello(name: String) -> String:
return say(name)
Spec: dimensional syntax
Tour: corvid tour --topic language-keywords
Roadmap: Phase 20 language surface
Proof: parser tests
Non-scope: Keywords do not replace ordinary application code; they expose AI-specific boundaries to the compiler.
Corvid evals can assert process, not just output. They can check that an agent called, approved, ordered, and spent as intended.
This targets the failure mode where an AI system gets the right answer through the wrong process.
agent always_refund() -> Bool:
return true
eval refund_accuracy:
result = always_refund()
assert result == true
Spec: verification
Tour: corvid tour --topic eval-traces
Roadmap: Phase 20c
Proof: eval assertion tests
Non-scope: This is language/checker support; the full eval runner is later workflow tooling.
Executions become evidence. Traces, deterministic replay, trace-diff, lineage, and signed receipts make behavior changes reviewable.
That gives AI-native programs an audit trail developers can diff, verify, and bundle.
@deterministic
@replayable
agent classify(text: String) -> String:
return text
Spec: replay and bundle format
Tour: corvid tour --topic replay-receipts
Roadmap: Phase 21 and Phase 22
Proof: bundle verification tests
Non-scope: Receipts are evidence of observed behavior, not full formal verification of every possible run.
The only agent skill system where you read a skill's permissions like a nutrition label — and the compiler holds it to them. A skill's skill.toml declares its capability ceiling; corvid add skill COMPUTES the audit from the source (a dishonest label refuses to install), renders it for consent, and vendors visible, git-diffable code. Every corvid check/corvid run re-verifies: edit a vendored skill past its label and the next check fails naming the exceeded dimension. DSSE-signed without a registry (one verification proves publisher identity AND content integrity), hash-pinned sources (local, git:, github:), and corvid skill update with fresh consent on change.
corvid add skill github:acme/skills/summarize-repo@v1.2 --publisher-key acme.hexcapability label (verified against the source):
uses: http, llm
max trust: supervisor_required
max cost: $0.2500 per call
reach: hosts api.github.com (enforced at runtime by [http] allow)
signed — publisher key `bc7cbcb5636375fa` verified; content hashes match.
Guide: Extending your agent
Proof: skill audit + signing + pin tests
Non-scope: hosted registry (post-v1.0); reach hosts/paths are enforced at runtime by [http] allow / [io] root, declared on the label.
corvid add mcp <name> --cmd ...|--url ... discovers the server's tools and generates a typed module — one typed agent per tool from the server's own JSON schemas, arguments built with the std/json builder so escaping is never string concatenation. Untrusted servers stay approval-gated through the generated wrappers; corvid mcp regen refreshes the module when the server changes. corvid add connector <provider> does the same for the shipped connectors, rendering each manifest into scope effects + operation tools with dangerous on quarantined writes.
Guide: Extending your agent
Proof: MCP codegen tests + connector scaffold tests
Non-scope: nested schema shapes fall back to one args_json parameter, stated in the generated comment.
OWASP's #1 LLM risk, caught by the type system instead of runtime hope. An effect declared data: untrusted marks its results — retrieved documents, user messages, untrusted MCP output — as Tainted<T>. Taint is contagious: concatenation preserves it, and a prompt that reads tainted content produces tainted output (the LLM read attacker-controlled text). Tainted<T> is never assignable to T, and passing it to an approval-requiring call (a dangerous tool, or one at supervisor/human trust) is a compile error.
effect web_content:
data: untrusted
tool fetch_page(url: String) -> String uses web_content
tool pay(recipient: String, amount: Float) -> String dangerous uses send_money
agent assistant(url: String) -> String:
page = fetch_page(url)
recipient = extract_recipient(page) # Tainted<String>
return pay(recipient, 100.0) # error: untrusted content
# cannot parameterize pay
The only way through is the explicit, greppable trusted(expr) boundary — one reviewable place a human asserts the value was constrained. It is Grounded<T>'s provenance machinery inverted: instead of tracking where trusted data came from, it tracks where untrusted data must not go.
Spec: injection-taint design
Tour: corvid tour --topic injection-taint
Guarantee: taint.untrusted_cannot_reach_dangerous (Static)
secret_read solves the secrets-in-traces problem instead of ignoring it: the program receives the real value, the recorded trace event carries a redacted copy (<redacted:XY> + value_redacted: true — a RuntimeChecked guarantee, secrets.trace_never_carries_value), and Substitute-mode replay re-reads the live environment instead of substituting, so a rotated credential diverges honestly instead of replaying a value the trace never stored. A missing secret is Ok with present: false.
import "./std/secrets" use secret_read
agent api_key() -> Result<String, String>:
key = secret_read("ANTHROPIC_API_KEY")?
if not key.present:
return Err("set ANTHROPIC_API_KEY")
return Ok(key.value)
Spec: std.secrets reference
Tour: corvid tour --topic replay-safe-secrets
Proof: secrets + cache e2e tests
Non-scope: forwarding a secret into another tool's arguments records it in that tool's events — the structural SecretHandle taint is the tracked post-v1.0 deepening.
cache_put / cache_get / cache_invalidate / cache_invalidate_provenance — an in-run cache whose eviction composes with provenance: entries carry the provenance key of the source they were derived from, and one call drops everything computed from a changed source, across namespaces. Misses are modeled Ok states (hit: false); all four tools record and replay-substitute as ordinary tool events, so replayed runs see identical cache behavior.
Spec: std.cache reference
Tour: corvid tour --topic provenance-cache
Proof: secrets + cache e2e tests
Non-scope: in-memory, per-run scope; String values in v1.
Language-level schedule "<cron>" zone "<tz>" -> agent(args) declarations execute under the scheduler runner: corvid schedule run --source app.cor registers each declaration as a durable schedule manifest and fires due jobs through the durable-jobs worker pool. Scheduled agents inherit the whole durable story — per-job tracing (JSONL traces for @replayable agents), retries with backoff, dead-letters, idempotent fires, DST-aware timezone handling, and missed-fire recovery policies — because scheduling rides the same queue everything else does, instead of a side mechanism with weaker guarantees.
Guide: Jobs and schedules Proof: scheduler runner e2e tests Non-scope: schedule arguments are literals (the manifest is a durable artifact); computation belongs in the target agent.
@replayable durable jobs record a typed JSONL trace on their first run. corvid jobs replay --source <path>.cor --job <id> reproduces the run from the trace, and during replay every side-effect surface refuses to escape: LLM adapter calls, outbound HTTP, application store writes, and filesystem writes. Recorded calls substitute from the trace; unrecorded ones fail closed with a typed QuarantineViolation naming the surface.
This makes "replay didn't leak" a runtime invariant instead of a property of the test harness.
@replayable
agent daily_brief(user_id: String) -> String:
return "brief for " + user_id
corvid jobs run --source app.cor --state queue.db --workers 1 --max-runtime-ms 0
corvid jobs replay --source app.cor --job <job_id>Spec: phase-38 replay-quarantine design
Tour: corvid tour --topic replay-quarantine
Roadmap: Phase 38 audit-correction track 35V2-P38-C-replay-quarantine
Proof: replay quarantine corpus
Non-scope: Quarantine ensures no real side effect escapes a Substitute-mode replay; it does not verify the original recording was correct, and it does not cover surfaces the runtime does not own (e.g. raw process spawns outside IoRuntime).
Models are declarations with capabilities and policy dimensions. Prompt dispatch is checked against those contracts.
Instead of stringly selecting models in application code, routing becomes part of the typed program.
model fast:
capability: basic
model deep:
capability: expert
prompt answer(q: String) -> String:
route:
q == "hard" -> deep
_ -> fast
"Answer {q}"
Spec: typed model substrate
Tour: corvid tour --topic model-routing
Roadmap: Phase 20h
Proof: dispatch tests
Non-scope: Routing declarations do not automatically benchmark model quality.
A prompt can try cheap models first and escalate only when confidence falls below a typed threshold.
That makes cost-quality tradeoffs explicit and reviewable rather than hidden in orchestration glue.
prompt classify(q: String) -> String:
progressive:
cheap below 0.80
medium below 0.95
expensive
"Classify {q}"
Spec: progressive refinement
Tour: corvid tour --topic progressive-routing
Roadmap: Phase 20h slice E
Proof: progressive dispatch tests
Non-scope: Thresholds depend on calibrated adapter confidence.
One prompt can dispatch to several models concurrently and fold answers through a typed voting strategy.
The strategy is source-level, so reviewers can see when consensus is required instead of guessing from runtime code.
prompt classify(q: String) -> String:
ensemble [opus, sonnet, haiku] vote majority
"Classify {q}"
Spec: ensemble voting
Tour: corvid tour --topic ensemble-voting
Roadmap: Phase 20h slice F
Proof: ensemble tests
Non-scope: Majority voting is shipped; arbitrary custom vote functions require future function-value work.
Model declarations can carry regulatory dimensions such as jurisdiction, compliance, and privacy tier.
That lets the compiler enforce declared routing constraints before data crosses a boundary.
model eu_private:
jurisdiction: eu_hosted
compliance: gdpr
privacy_tier: strict
capability: expert
Spec: regulatory dimensions
Tour: corvid tour --topic privacy-routing
Roadmap: Phase 20h slice D
Proof: dimension law tests
Non-scope: The compiler enforces declared facts; legal compliance still requires operations, contracts, and audits.
Streams are typed values that carry effects while data is still arriving. Budgets, confidence, provenance, and backpressure are not after-the-fact logs.
This makes streaming AI workflows safer without forcing users into untyped callback systems.
agent count() -> Stream<Int>:
yield 1
yield 2
Spec: streaming
Tour: corvid tour --topic streaming-effects
Roadmap: Phase 20f
Proof: stream tests
Non-scope: Provider token streaming is REAL as of slice 46d — a plain -> Stream<String> prompt streams SSE deltas from all four provider adapters through this algebra (mid-stream token limits, confidence floors, budget termination), and the trace records chunk boundaries so replay re-chunks identically. Structured Stream<T> and prompts using multi-model dispatch clauses (route/progressive/rollout/ensemble/adversarial) still make one whole call and yield it as a single chunk; provider-native continuation additionally depends on provider APIs.
Partial<T> lets a program read complete fields as they arrive while the rest of a structured response is still forming.
The type system exposes incomplete state safely instead of asking users to parse half-valid JSON.
type Plan:
title: String
body: String
agent read(snapshot: Partial<Plan>) -> Option<String>:
return snapshot.title
Spec: streaming
Tour: corvid tour --topic partial-streams
Roadmap: Phase 20f Stream<Partial>
Proof: partial stream tests
Non-scope: Full native parity for every partial-stream path remains backend work. Until slice 46d wires provider token streaming, Partial<T> values from LLM prompts arrive complete rather than progressively (see the Streaming Effects non-scope above).
ResumeToken<T> captures the typed stream element contract so continuation cannot resume the wrong prompt shape.
This gives interrupted streams a language-level recovery boundary instead of an ad hoc provider session string.
agent capture(topic: String) -> ResumeToken<String>:
stream = draft(topic)
return resume_token(stream)
Spec: streaming
Tour: corvid tour --topic stream-resume
Roadmap: Phase 20f resumption tokens
Proof: stream resume tests
Non-scope: Provider-native session continuation waits on provider APIs; local fallback is shipped. Live mid-stream interruption of provider tokens requires 46d (see the Streaming Effects non-scope above).
Streams can split by structured fields and merge back with deterministic ordering.
The stream topology is visible in the program, so effects and ordering can be preserved through orchestration.
agent fanout() -> Stream<Event>:
groups = source().split_by("kind")
return merge(groups).ordered_by("fair_round_robin")
Spec: streaming
Tour: corvid tour --topic stream-fanout
Roadmap: Phase 20f fan-out/fan-in
Proof: stream type tests
Non-scope: Field-keyed split is shipped; first-class lambda extractors wait for function values.
Corvid can distribute pieces of the effect algebra as signed artifacts with law checks, proofs, and regression programs.
This is how the language can grow new policy dimensions without turning the compiler into a trust bottleneck.
effect local_policy:
data: pii
reversible: true
tool read_profile(id: String) -> String uses local_policy
Spec: dimension artifacts
Tour: corvid tour --topic effect-registry
Roadmap: Phase 20g invention 9
Proof: dimension registry tests
Non-scope: The registry distributes declarations, not executable code or unverified trust.
The compiler ships with a bypass-attempt taxonomy so AI can attack Corvid's own effect system in CI.
That turns "AI safety" into a regression target instead of a slogan.
tool refund(id: String) -> String dangerous uses transfer_money
@trust(human_required)
agent safe_refund(id: String) -> String:
approve Refund(id)
return refund(id)
Spec: adversarial taxonomy
Tour: corvid tour --topic adversarial-tests
Roadmap: Phase 20g adversarial generator
Proof: adversarial tests
Non-scope: Live LLM generation expands the corpus; deterministic seeds remain the safety gate.
Corvid's std/io module ships three executing tools — io_read_text, io_write_text, io_list_dir — that flow through typed effect rows (io_read, io_write, io_list) and a runtime-enforced [io] root confinement boundary.
The security boundary is declared in corvid.toml and signable: a signed cdylib carries io_source.fs_path_confinement + the two replay-quarantine guarantees in its claim manifest, so a host can verify the binary refuses to operate outside the declared root.
import "./std/io" use io_read_text, io_write_text
agent persist_summary(date: String, body: String) -> Result<String, String>:
io_write_text(date + ".txt", body)?
return Ok(date)
All three tools return Result — a missing file, an OS error, or a policy refusal is an Err VALUE naming the cause, never a crash. Calls outside the configured [io] root return Err with a structured diagnostic naming the offending path AND the root. Calls inside a @deterministic agent are rejected at typecheck. Calls during replay either substitute from the recorded trace or diverge — the filesystem is provably untouched.
Spec: std.io reference
Tour: corvid tour --topic file-io
Roadmap: Phase 33S1
Proof: executing I/O tests + replay-quarantine corpus + path-confinement tests
Non-scope: Confines paths to the declared root; does not police what user code does with the contents.
Corvid's std/http module ships two executing tools — http_get, http_post_json — that flow through typed effect rows (http_egress_get, http_egress_post) and a two-layer security boundary: an always-on structural SSRF block that refuses RFC1918 / loopback / link-local hosts regardless of allowlist, plus a required [http] allow allowlist that fails closed when unconfigured.
The security boundary is declared in corvid.toml and signable: a signed cdylib carries io_source.http_ssrf_structural_block, io_source.http_allowlist_enforcement, and io_source.http_quarantine_on_replay in its claim manifest, so a host can verify the binary refuses to reach private networks AND can only reach explicitly approved hosts AND cannot escape replay quarantine.
import "./std/http" use http_get, http_post_json, http_ok
agent ship_event(url: String, body: String) -> Result<Bool, String>:
response = http_post_json(url, body)?
return Ok(http_ok(response))
Both tools return Result — policy refusals and transport failures are Err VALUES the program observes (an error HTTP status like 404 is still Ok; inspect status).
[http]
allow = ["hooks.example.com"]A URL whose host is not in [http] allow is refused with a structured diagnostic naming the host AND the configured allowlist. A URL whose host resolves to a private range is refused by the structural SSRF block before the allowlist is consulted — even a misconfigured [http] allow = ["127.0.0.1"] cannot reach loopback. Calls inside a @deterministic agent are rejected at typecheck. Calls during Substitute-mode replay either substitute from the recorded trace or diverge — the network is provably untouched.
Spec: std.http reference
Tour: corvid tour --topic http-client
Roadmap: Phase 33S2
Proof: end-to-end HTTP tests + policy tests + replay-quarantine corpus
Non-scope: Enforces SSRF + allowlist + replay quarantine on the URL host; does not police response-body content or rewrite request headers.
Corvid's std/db module ships three executing tools — db_open, db_query, db_execute — that flow through typed effect rows (db_egress_open, db_egress_read, db_egress_write) and three load-bearing structural properties:
-
SQL injection is prevented structurally, not by escaping. The
db_query/db_executetools'List<DbParam>signature forces every value through the typed constructors (db_param_int,db_param_text, etc.), and the runtime binds viarusqlite::params_from_iterover typedDbValues. There is noformat!call anywhere on the dispatch path; a literal"'; DROP TABLE users; --"placed indb_param_textsurvives as text data and never reaches SQLite's parser. The structural argument is pinned by a runtime unit test AND an end-to-end driver test against a real Corvid program. -
[io] rootpath confinement reuses the file-I/O boundary.db_openroutes through the sameIoToolPolicythe io tools use; SQLite is structurally as narrow asio_write_text. No separate[db]allowlist exists. The documented special case":memory:"bypasses path resolution. -
DbHandleis an opaque, refcounted primitive type. Constructed only bydb_open's typed-Value dispatch path; user code cannot forge a handle through JSON round-trip (the VM'sjson_to_valueREFUSES to mint aType::DbHandlefrom any payload, including the trace-debug sentinel shape).
The security boundary is declared in corvid.toml (via [io] root) and signable: a signed cdylib carries io_source.sqlite_parameter_binding_only, io_source.sqlite_write_quarantine_on_replay, io_source.sqlite_read_passthrough_on_replay, and the reused io_source.fs_path_confinement in its claim manifest.
import "./std/db" use db_open, db_execute, db_query, db_param_int, db_param_text
agent record_user(email: String) -> Result<Int, String>:
handle = db_open(":memory:")?
db_execute(handle, "CREATE TABLE users(id INTEGER PRIMARY KEY, email TEXT NOT NULL)", [])?
db_execute(handle, "INSERT INTO users(id, email) VALUES (?, ?)", [db_param_int(1), db_param_text(email)])?
rows = db_query(handle, "SELECT id FROM users WHERE email = ?", [db_param_text(email)])?
return Ok(rows[0].rows_affected)
All three tools return Result — open failures, SQL errors, and confinement refusals are Err VALUES naming the cause.
Calls inside a @deterministic agent are rejected at typecheck. Calls during Substitute-mode replay refuse db_execute with QuarantineViolation { surface: "db", .. } — the database is provably untouched. SQLite only; the Postgres path remains envelope-only (declare a Postgres tool in user code and reach corvid-runtime::PostgresDbRuntime from a tool wrapper).
Spec: std.db reference
Tour: corvid tour --topic sqlite
Roadmap: Phase 33S3
Proof: end-to-end SQLite tests + DbHandleRegistry tests + replay-quarantine corpus
Non-scope: SQLite only — the Postgres path remains envelope-only. Path confinement reuses [io] root; no separate [db] allowlist exists.
Corvid's std/json module ships 13 executing tools across TWO complementary shapes — the load-bearing "no Python required for JSON" promise of the batteries umbrella:
-
Opaque path —
json_parse(text) -> Result<JsonValue, String>, typed accessors (json_get_int,json_get_string, ...), fluent builder (json_object_new→json_object_set_*→json_object_finish). For dynamic JSON: LLM responses of unknown shape, debug tooling, polymorphic APIs. -
Typed-decoder convention — user declares
tool decode_<X>_from_json(text: String) -> Result<X, String>where X is any Corvid type the runtime can convert from JSON. The interpreter pattern-matches the tool name + return type and routes throughserde_json::from_str+json_to_valueagainst the declared target. No per-type runtime handler exists — the dispatch is generic over the declared signature. For typed APIs and the 33S4 HTTP→JSON→SQLite tutorial.
The surface enforces two load-bearing structural safety properties:
- Parse safety —
json_parseagainst arbitrary bytes returnsResult::Err(message)rather than panicking. The typed-decoder convention inherits this. - Field-type safety —
json_get_intagainst a String field returnsResult::Err, never coerces. The typed-decoder convention inherits this too — JSON shape mismatches surface asResult::Errrather than runtime panics.
The security boundary is structural in the typechecker: a signed cdylib carries json.parse_safety_no_panic and json.field_type_safety_at_access_boundary in its claim manifest.
effect json_decode_eff:
reversible: true
type User:
id: Int
email: String
import "./std/json" use json_parse, json_get_int
tool decode_user_from_json(text: String) -> Result<User, String> uses json_decode_eff
agent typed_decoder(text: String) -> Result<Int, String>:
user = decode_user_from_json(text)?
return Ok(user.id)
Calls inside a @deterministic agent are rejected at typecheck. JSON parse/build are deterministic and process-internal so replay-mode dispatch runs IDENTICALLY to live (no quarantine flag needed). The cdylib corvid_json_* C-ABI exports already exist in corvid-runtime::ffi_bridge::json_exports; cdylib codegen for JsonValue / JsonBuilder is interpreter-only in 33R5b (follow-up slice).
Spec: std.json reference
Tour: corvid tour --topic json
Roadmap: Phase 33R5b
Proof: end-to-end JSON tests + runtime JSON tests + replay-quarantine corpus
Non-scope: No JSON Path / JSONata / JMESPath query language (nested access via json_get_object chains). cdylib codegen for the opaque types is a follow-up slice; the C-ABI exports already exist.
std/rag's rag_ingest / rag_search are retrieval with the moat attached — the part every RAG framework leaves to convention, Corvid enforces:
- Path confinement: index paths resolve through the same
[io] rootpolicy as file I/O — fails closed when unconfigured, rejects traversal and absolute escapes. - Honest failures: missing index, bad arguments, embedder errors, and policy rejections are
Result::Errvalues, never traps. - Provenance on every chunk: each retrieved
RagChunkEnvelopecarries itsprovenance_key+effect_meta— checkable, threadable values. - Replay substitution: the calls are traced like every executing tool; on replay the recorded results return and the embedder never fires.
- Honest degradation: with no
[rag]embedder in corvid.toml, search falls back to term-scored lexical matching over the same index — identical program behavior, lower recall.
Embedders (OpenAI / Ollama) configure in corvid.toml [rag]; ingestion chunks with overlap and embeds in one call.
Spec: std.rag reference
Tour: corvid tour --topic governed-retrieval
Roadmap: Slice 46g
Proof: end-to-end RAG tests
Non-scope: No loaders on the tool surface (PDF/HTML loaders exist runtime-side); no reranking; effect-level Grounded<T> wrapping waits for cross-module provenance composition (post-v1.0) — provenance travels explicitly in the envelope values.
Consume any Model Context Protocol tool server through mcp_call — with the moat intact: servers are untrusted by default (calls go through the runtime approver before any transport I/O; trust = "autonomous" loosens explicitly), every call is traced and replay-substituted (replays never contact a server), and every failure including approval denial is an Err value. stdio + HTTP transports. Try corvid tour --topic mcp.
Roadmap: Slice 46f
Proof: MCP integration tests
Non-scope: client only (MCP server is post-v1.0); no compile-time tool introspection — pair with std/json typed accessors.
parallel: runs named arms concurrently and joins when all complete — with the governance intact: arm costs sum into @budget, arm traces flush in arm order so corvid replay reproduces a concurrent run deterministically (zero trace-schema changes), and failures are arm-ordered, not completion-ordered. Try corvid tour --topic parallel.
Roadmap: Slice 46e Proof: parallel tests Non-scope: racing/select, cancellation, streaming arms (post-v1.0); each arm is one call — wrap richer logic in an agent.
Corvid's std/time and std/random modules make the two most common sources of hidden nondeterminism — clock reads and random draws — visible to the effect system. time_now_utc, time_monotonic_ms, random_float, and random_int are tools flowing through typed effect rows (time_wall, time_monotonic, rand_draw), which means:
- Replay substitutes them. Tool calls are traced; in Substitute-mode replay the recorded instant / draw is returned instead of touching the live clock or entropy source. A time-dependent agent re-runs deterministically with no seed-management convention.
@deterministicrejects them at compile time. The declaration-kind classifier already rejects tool calls inside@deterministicbodies — an agent that secretly reads the clock or rolls dice is a compile error.
The pure math methods (abs, min, max, pow, sqrt, floor, ceil, round) live on the builtin-method table under the always-checked rule (Int overflow traps; sqrt of a negative traps; floor/ceil/round return Int and trap on NaN). Durations are plain Int milliseconds — checked arithmetic IS the duration API.
import "./std/time" use time_now_utc, time_format_iso
import "./std/random" use random_int
agent schedule_followup(days: Int) -> String:
now = time_now_utc()
return time_format_iso(now.epoch_ms + days * 86400000)
agent roll() -> Int:
return random_int(1, 6)
Spec: std.time reference + std.random reference
Tour: corvid tour --topic deterministic-time
Roadmap: slice 45m in ROADMAP.md
Proof: end-to-end time/math/random test + replay substitution test
Non-scope: UTC only (no timezone database or calendar arithmetic); no seeded PRNG surface — reproducibility comes from replay.
A Corvid backend describes its whole public interface as a machine-readable Application Contract. From that one artifact the compiler emits a standard OpenAPI 3.1 document, an AI-native corvid-ai.json (streaming events, grounding, approvals, confidence, cost, latency — the behavior OpenAPI cannot express), a universal corvid dev console, and typed client SDKs in TypeScript / Swift / Kotlin / Python, plus React hooks and a runnable frontend scaffold — all reading the SAME contract, so no two platforms disagree about a type.
Typed error enums carry @status/@ui per variant (exhaustive frontend handling); uploads and cursor pagination are first-class HTTP-boundary types. identity declares sign-in providers where every OAuth safe-default is mandatory — an insecure session is a compile error absent a loud opt-out, account-linking never silently merges by email, and a per-user connector token is a distinct credential from the login session.
public type Answer:
text: String
score: Int where between(0, 100)
identity app_users:
provider google
provider github
provisioning:
first_login: open
tenant: fixed("public")
public agent classify(question: String) -> Answer:
return Answer(question, 90)
public agent chat(message: String) -> Stream<String>:
return echo_stream(message)
corvid contract app | openapi | ai # the contract + its projections
corvid generate sdk --language ts|swift|kotlin|python
corvid generate frontend --framework react
corvid dev # a universal, contract-driven consoleA running corvid serve also advertises its own surface at /.well-known/corvid and /openapi.json.
Spec: Application Surface
Tour: corvid tour --topic application-surface
Roadmap: Phase 51 application surface
Proof: contract + OpenAPI + SDK generators + core-semantics contract.matches_compiled_surface
Non-scope: Corvid owns the AI-backend↔frontend boundary — it describes the surface precisely enough that existing frontends consume it safely; it does not become a frontend language or design your app's UI.
Phase 51 makes a Corvid backend describe its interface; Phase 52 makes the runtime prove it implements it. Every declared route shape executes through the interpreter — a path parameter (path.id), a typed query struct (query.status), and a typed JSON body (body.item) each run their handler body through the ordinary agent machinery, so effects, approval, provenance, and replay apply to route execution automatically. Malformed boundary input is a structured 400, never a 500. And the HTTP-boundary types execute: a Stream<T> route streams as Server-Sent Events (one data: event per yield, event: done to close); an Upload<Format> body is parsed from multipart under its required source-declared @upload(max_mb: N, mime: "...") policy and read via body.text()/bytes()/filename(); a Page<Item> response built with Page(items, next_cursor) serves the {items, next_cursor, has_more} cursor envelope. Omitting an upload maximum is a compile error—there is no hidden runtime limit.
server imports:
@upload(max_mb: 25, mime: "text/csv")
route POST "/imports" body Upload<Csv> -> json ImportReceipt:
return import_rows(body)
Contract Closure keeps the advertised surface and the runtime from ever drifting: before corvid serve binds a listener it asserts a runtime execution path exists for every route the contract advertises. A route it cannot yet serve is a startup error (E5204), never a silent runtime 501. That mechanism carried the runtime to completion — route execution, streaming, uploads, pagination, and now authorization enforcement all serve. A requires authenticated|role|permission route resolves the caller's session to a verified typed actor and enforces tenant + role + permission (and CSRF double-submit on mutations) before the handler or any effect runs; an unauthenticated request is a 401 and an under-privileged one a 403.
corvid serve examples/reference_app/src/main.cor # path/query/body/stream/upload/page routes all execute
corvid serve secure_app.cor # STARTS — a `requires authenticated` route now serves
curl -i secure_app/secret # 401: the session is resolved and enforced before the handlerSpec: The Complete Application Runtime
Tour: corvid tour --topic contract-closure
Roadmap: Phase 52 the complete application runtime
Proof: route execution + authorization enforcement + contract closure + core-semantics contract.runtime_closure
Non-scope: Closure grew in lockstep with the runtime — each Phase 52 slice flipped one capability on, and the interpreter tier is now complete; the refuse-to-start mechanism still guards any future capability and the native tier. Native-tier route execution is later work.
A parallel: block runs its arms concurrently and fails fast — when one arm errors, the others are asked to stop. Corvid adds the guarantee that makes concurrent effects safe: a branch past a non-reversible effect boundary is never cancelled. The moment an arm dispatches an irreversible tool (a write, a POST — any effect whose composed row is reversible: false) it is shielded and runs to completion, even if a sibling failed; only arms that have done nothing irreversible are cancelled, and they stop at a tool-dispatch boundary before their next effect. Cancellation is cooperative, not a preemptive abort, so it holds that line without a race. And because live cancellation is timing-dependent, every block records each arm's outcome + reversibility + dispatch boundary, and Substitute-mode replay reproduces the exact run deterministically — a cancelled arm replays to its recorded boundary, a shielded arm reaches its recorded terminal, and non-cancelling blocks replay byte-identically.
Spec: Cancel Fast, But Never Past a Point of No Return
Tour: corvid tour --topic parallel-cancellation
Roadmap: Phase 52 effect-aware scheduling
Proof: the parallel scheduler + replay reproduction + core-semantics parallel.cancellation_reversibility
Non-scope: Cooperative cancellation at tool-dispatch boundaries (an arm in a tight pure loop is not preempted); a tool is shielded exactly when it declares an irreversible effect.
Declare an identity block and corvid serve mounts the whole login surface — /auth/{provider}/login, /callback, /logout, /session — wired to Authorization Code + PKCE, a single-use signed state, an OIDC nonce, and JWKS verification, with a Secure/HttpOnly/SameSite session cookie. The invention is what the compiler makes you decide first: how an unknown, verified user becomes an account. An identity block that declares OAuth providers but omits its first-login policy is a compile error (E5210 First-login policy required) — no silent default, so an enterprise app can never accidentally ship open registration. You pick open (public signup) or invited (only against a pre-existing invitation); approval_required won't compile until the runtime can execute it. Identity is always established server-side and keyed on the provider's own authoritative id — (issuer, subject) from a verified ID token, or (provider, user_id) from a server-to-server userinfo fetch for OAuth2-only providers — never an email, never a caller-controlled claim.
identity users:
provider google
provider github
provisioning:
first_login: invited # omit this block → E5210, does not compile
tenant: from_invitation
Spec: First Login Is An Explicit Compile-Time Decision
Tour: corvid tour --topic oauth-login
Roadmap: Phase 52 identity runtime
Proof: the login routes + the provisioning executor + the E5210 checker gate
Non-scope: The login/session and route-authorization runtime is complete; durable approval_required first-login provisioning remains a later slice.
Declare an external API in source as a connector — base URL, secret(...) credentials (a bare-string credential is a parse error), and a reliability posture — and each operation is a callable tool with a declarative HTTP body. The mode is chosen at the boundary with no default: a connector declares the modes it may run in, the deployment picks one with corvid run --mode, and omitting modes (or selecting one the connector doesn't allow) is a compile error / startup refusal — a program can never reach a real provider by silence. The same unchanged file runs three ways: mock evaluates the compiled mock: payload, real makes the HTTP request (the credential resolves at dispatch into a header and never enters the IR, a trace, or an error), and replay serves a recorded interaction and never falls through to a real call. Because an operation IS a tool, the moat composes: a dangerous operation still needs approve, and on status <code> -> Variant turns an HTTP status into a typed Result error the compiler makes you handle.
connector github:
base_url: "https://api.github.com"
auth: bearer(secret("GITHUB_TOKEN"))
rate_limit: 60 per 60s
modes: [mock, replay, real] # omit → compile error; no default
operation get_repo(owner: String, repo: String) -> Result<Repo, GithubError> uses http_read:
GET "/repos/{owner}/{repo}"
on status 404 -> NotFound # HTTP status → typed Err variant
mock: Ok(Repo("corvid"))
Spec: Protocol-Typed Connectors
Tour: corvid tour --topic connectors
Roadmap: Phase 52 connectors
Proof: the connector modes + the request builder + status→error coherence
Non-scope: The runtime enforces the Corvid-declared contract (modes, credentials, egress, typed errors, reliability), not provider honesty; provider-drift quarantine is a later 52i slice.
Some provider calls don't finish when the response arrives — you submit, and the work happens later. Everywhere else that's a hand-rolled poll loop, and the poll loop is where the bugs live: the timeout nobody tuned, the retry that submits a second job, the restart that loses the work. An async: block declares the temporal contract instead, and the compiler proves it: statuses declared once, transition tables total, every state reaching a terminal, non-zero bounds, a non-mutating poll, and a mutating submit passing dangerous approval. The worst-case observation count multiplies the operation's cost, so a protocol cannot poll its way past a @budget. At runtime the intent is checkpointed before the submit leaves the process and the provider job id binds only from the JSON-decoded response, so a crash cannot lose the work and a job that already recorded its submit is never re-submitted on resume. The call returns only on a declared terminal state; a submit response is never mistaken for completion.
Cancelling is honest: exact before submit, compensated through a declared cancel endpoint after it, and explicitly detached when none is declared. Editing a protocol with intents in flight requires on_protocol_change — and you never bump a version number, because Corvid fingerprints the protocol graph and tells you what changed.
Exactly-once needs the provider's help, so Corvid makes you declare how to ask for it: idempotency: intent via header "Idempotency-Key" sends the intent key on the submit, and omitting it is a compile error. Durability alone cannot cover the window where the provider accepted a submit but the process died before recording it — only the provider can recognise the repeat, and only if it was given something to recognise.
operation submit_shipment(order: String) -> Job dangerous uses http_write:
POST "/shipments" body order
async:
statuses: [queued, processing, completed, failed]
initial: queued
terminal: [completed, failed]
deadline: 600s # bounds the poll loop AND the budget
deadline_target: failed
idempotency: intent # checkpointed before submit
poll GET "/shipments/{id}" # {id} binds from the DECODED response
every: 30s
cancel POST "/shipments/{id}/cancel"
on_protocol_change: refuse # omit → compile error; no default
state queued:
on processing -> processing
on completed -> completed
on failed -> failed
corvid connectors simulate <file> explores what a provider could do to you before you deploy — including the behaviours that never terminate on their own:
[non_terminating] reporting `processing` forever holds the intent in `processing`;
after 600s (20 observations) the declared deadline forces `failed`
[deadline_reachable] `failed` is reachable without the provider ever failing —
a slow provider is enough
Spec: Verified Provider Protocols
Tour: corvid tour --topic verified-provider-protocols
Roadmap: Phase 52 verified provider protocols
Proof: the durable lifecycle + the transition engine + the simulator
Non-scope: Validating that a provider's payload matches its declared shape once it arrives — live conformance and drift quarantine are a later 52i slice. The deadline and cadence are declared and checked, never defaulted.
source .cor
-> lex / parse
-> resolve names
-> typecheck
-> effect, budget, confidence, grounding, approval, routing checks
-> typed IR
-> interpreter, native Cranelift backend, Python backend, WASM backend
-> traces, replay, receipts, bundles
The language is designed as one compiler pipeline with multiple execution tiers. Safety properties belong in the shared frontend and IR, not in one backend's runtime glue.
Corvid is pre-v1.0 and under active development. The compiler, interpreter, effect system, model substrate, streaming substrate, replay/bundle infrastructure, native backend, signed cdylib attestation, separate-binary ABI descriptor verifier, and claim explanation workflow are in the repository today. Some backend paths intentionally reject newer high-level features until parity work lands; signed builds fail closed when contract-like syntax is not mapped to a registered guarantee.
A 2026-04-29 internal audit of Phases 35-41 found four phase-done bullets in Phases 38-41 that were structurally absent (multi-worker job runner + crash-recovery / DST tests, real JWT verification + corvid auth/approvals CLI, OTel SDK conformance, connector real mode + corvid connectors CLI). The ROADMAP now carries audit-correction tracks (35-N, 38K-M, 39K-L, 40J-K, 41K-M) that close the gaps end-to-end. Slice checkmarks before those tracks land are honest only at the layer the slice named — composition with the surfaces above stays disabled.
Use the roadmap for source-of-truth status:
rg -n "^- \\[ \\]" ROADMAP.mdWindows (PowerShell):
irm https://raw.githubusercontent.com/Micrurus-Ai/Corvid-lang/main/install/install.ps1 | iexmacOS / Linux:
curl -fsSL https://raw.githubusercontent.com/Micrurus-Ai/Corvid-lang/main/install/install.sh | shThe installer downloads a prebuilt corvid for your OS/arch into ~/.corvid/, adds ~/.corvid/bin to your PATH, and runs corvid doctor. If a prebuilt archive is not available for your platform, it falls back to a cargo install from source.
Override defaults with CORVID_REPO, CORVID_VERSION (e.g. v0.1.0), or CORVID_HOME.
Status: the install scripts above (
install/install.{sh,ps1}) are the canonical install path for Corvid v1.0. The package- manager manifests below are tracked as Phase 33P slices inROADMAP.mdand ship post-v1.0 — none of them is the "installer," each is additive metadata that a language-installer manager's central repo consumes and routes back to the GitHub Release artifactsrelease.ymlproduces. They're filed but not built yet; running them today will report "formula/manifest not found."
| Manager | End-user command (post-v1.0) | Filed slice |
|---|---|---|
| Homebrew (macOS / Linux) | brew install Micrurus-Ai/corvid/corvid |
33P1-homebrew-tap |
| Scoop (Windows) | scoop bucket add corvid https://github.com/Micrurus-Ai/scoop-corvid && scoop install corvid |
33P2-scoop-bucket |
| winget (Windows) | winget install Micrurus-Ai.Corvid |
33P3-winget-manifest |
| Chocolatey (Windows) | choco install corvid |
33P4-chocolatey-package |
| AUR (Arch Linux) | yay -S corvid-bin (or equivalent AUR helper) |
33P5-aur-package |
| APT / RPM (Debian / Fedora) | apt install corvid / dnf install corvid after one-time repo add |
33P6-apt-rpm-repo |
If you want to track or contribute any of these,
ROADMAP.md's Phase 33P block names each
filed slice with what it actually does. Manifest contributions are
welcome at any time — the GitHub Release artifacts they consume
(release.yml) are already shipping; the manifests are
post-v1.0 only because Path A defers public packaging-manager
listings until launch by deliberate design.
cargo install --path crates/corvid-cli
corvid doctorPython runtime pieces are only needed when using the Python backend. Native and interpreter work do not require a Python deployment target.
cargo check --workspace
cargo test --workspace
cargo run -q -p corvid-cli -- tour --list
cargo run -q -p corvid-cli -- check examples/refund_bot_demo/refund.corIf cargo fmt --check fails because cargo-fmt is not installed, install the Rust formatter for the active toolchain before treating formatting as validated.
- ROADMAP.md: build plan and shipped slices.
- docs/reference/inventions.md: standalone invention catalog and proof matrix.
- docs/internals/effect-spec/: AI-native effect system, grounding, budgets, confidence, streaming, model substrate, replay, and verification specs.
- docs/reference/core-semantics.md: generated guarantee registry with ids, classes, phases, and test references.
- docs/security/model.md: signed artifact trust boundary, host acceptance workflow, and explicit non-goals.
- docs/operations/ci.md: CI matrix, including optional Python FFI feature coverage.
- docs/internals/bundle-format.md: signed bundle and receipt format.
- ARCHITECTURE.md: compiler design and repo structure.
- CONTRIBUTING.md: project rules and contribution expectations.
- docs/internals/effect-spec/bounty.md: public submission process for effect-system bypasses and false positives. Accepted reports are credited to the reporter and added to docs/internals/effect-spec/counterexamples/ as permanent regression fixtures.
- docs/internals/package-manager-scope.md: what the package manager does today vs what would require a hosted registry service. Corvid ships package format and local/self-hosted registry tooling; no Corvid-hosted package registry service runs yet.
- dev-log.md: chronological build journal.
- learnings.md: durable engineering lessons.
Corvid is released under the MIT License.
Contributions are licensed under the same MIT terms (inbound = outbound) unless the contributor marks otherwise.