diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index d44538c4..8f849ca5 100644 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -29,14 +29,11 @@ jobs: working-directory: .ddraig-ssg run: idris2 Ddraig.idr -o ddraig - name: Build site + run: ./.ddraig-ssg/build/exec/ddraig build site _site https://nesy-prover.dev + - name: Add playground run: | - mkdir -p src - if [ ! -f src/index.md ] && [ -f README.md ]; then - cp README.md src/index.md - elif [ ! -f src/index.md ]; then - echo "# ${GITHUB_REPOSITORY}" > src/index.md - fi - ./.ddraig-ssg/build/exec/ddraig build src _site https://hyperpolymath.github.io/${GITHUB_REPOSITORY#*/} + mkdir -p _site/playground + cp echidna-playground/index.html echidna-playground/styles.css _site/playground/ - name: Upload artifact uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5.0.0 with: diff --git a/deno.lock b/deno.lock index ccc0e2ce..77b75dbe 100644 --- a/deno.lock +++ b/deno.lock @@ -1,4 +1,11 @@ { - "version": "4", - "remote": {} + "version": "5", + "specifiers": { + "jsr:@std/yaml@*": "1.1.2" + }, + "jsr": { + "@std/yaml@1.1.2": { + "integrity": "de612653c036749ba2044165e316f52412b0f0698afffb7ee80b5331d6d2abae" + } + } } diff --git a/echidna-playground/deno.json b/echidna-playground/deno.json index c9f1c3f2..5cc9a154 100644 --- a/echidna-playground/deno.json +++ b/echidna-playground/deno.json @@ -4,8 +4,8 @@ "tasks": { "build:res": "deno run -A --node-modules-dir=auto npm:rescript build", "clean:res": "deno run -A --node-modules-dir=auto npm:rescript clean", - "dev": "deno run --allow-net --allow-read server.ts", - "serve": "deno run --allow-net --allow-read server.ts", + "dev": "deno run --allow-net --allow-read jsr:@std/http@^1.0.0/file-server .", + "serve": "deno run --allow-net --allow-read jsr:@std/http@^1.0.0/file-server .", "res:build": "deno run -A --node-modules-dir=auto npm:rescript build", "res:clean": "deno run -A --node-modules-dir=auto npm:rescript clean", "res:watch": "deno run -A --node-modules-dir=auto npm:rescript build -w" diff --git a/echidna-playground/index.html b/echidna-playground/index.html index 14114068..8822aa23 100644 --- a/echidna-playground/index.html +++ b/echidna-playground/index.html @@ -3,37 +3,39 @@ - - jsCoq – Use Coq in Your Browser + ECHIDNA Playground – Coq in Your Browser
-

Welcome to the jsCoq Interactive Online System!

+ +

Welcome to the ECHIDNA jsCoq Playground

- Welcome to the jsCoq technology demo! - jsCoq is an interactive, - web-based environment for the Coq Theorem prover, and is a collaborative - development effort. See the list of contributors - below. + This page embeds jsCoq, an + interactive, web-based environment for the Coq theorem prover. + All the Coq code below is editable and runs directly in your + browser — no installation required. Once + jsCoq finishes loading, step + through the proof and watch the intermediate proof states in the + right-hand panel.

- jsCoq is open source. If you find any problem or want to make - any contribution, you are extremely welcome! We await your - feedback at GitHub - and Gitter. + jsCoq is open source — feedback + and contributions are welcome at + GitHub. The wider + ECHIDNA platform, which orchestrates Coq alongside many other + provers, lives at + github.com/hyperpolymath/echidna.

Instructions:

-

- The following document contains embedded Coq code. - All the code is editable and can be run directly on the page. - Once jsCoq finishes loading, you are - free to experiment by stepping through the proof and viewing intermediate - proof states on the right panel. -

Actions:
@@ -58,100 +60,62 @@
Actions:
ButtonKey bindingAction
Toggles the goal panel.
-
Saving your own proof scripts:
-

- The scratchpad offers simple, local - storage functionality. - Please go to CollaCoq if - you want to share your developments with other users. -

-

A First Example: The Infinitude of Primes

-

- We don't provide a Coq tutorial (yet), but as a showcase, we - display a proof of the infinitude of primes in Coq. The proof relies - in the Mathematical Components library by the - MSR/Inria team led - by Georges Gonthier, so our first step will be to load it and - set a few Coq options: -

-
-
- -
-
-
Ready to do Proofs!
+

A First Example: Addition and Zero

- Once the basic environment has been set up, we can proceed to - the proof: + As a showcase, we prove a small but genuine theorem about the + natural numbers: adding zero on the right leaves a number + unchanged. In Coq, nat is defined inductively — + a natural number is either 0 or the successor + S n of a natural number — and + + recurses on its first argument. That makes + 0 + n = n true by computation, but + n + 0 = n requires a proof by induction.

-

- The lemma states that for any number m, - there is a prime number larger than m. - - Coq is a constructive system, which among other things - implies that to show the existence of an object, we need to - actually provide an algorithm that will construct it. - - In this case, we need to find a prime number p - that is greater than m. - What would be a suitable p? - - Choosing p to be the first prime divisor of m! + 1 - works. - As we will shortly see, properties of divisibility will imply that - p must be greater than m. -

- -

- Our first step is thus to use the library-provided lemma - pdivP, which states that every number is divided by a - prime. Thus, we obtain a number p and the corresponding - hypotheses pr_p : prime p and p_dv_m1, - "p divides m! + 1". - The ssreflect tactic have provides a convenient way to - instantiate this lemma and discard the side proof obligation - 1 < m! + 1. + The lemma states that for every natural number n, + n + 0 equals n. We begin the proof by + induction on n, which splits the goal into a base + case for 0 and an inductive step for + S n:

- +

- It remains to prove that p is greater than m. - We reason by - contraposition with the divisibility hypothesis, which gives us - the goal "if p ≤ m then p is not a prime divisor of " - m! + 1". + The base case is settled by reflexivity, since + 0 + 0 computes to 0. In the inductive + step we may assume the hypothesis IHn : n + 0 = n; + simplification exposes the successor, and rewriting with the + hypothesis closes the goal:

-

- The goal follows from basic properties of divisibility, plus - from the fact that if p ≤ m, then p divides - m!, so that for p to divide - m! + 1 it must also divide 1, - in contradiction to p being prime. + And that is a complete, machine-checked proof. Try editing the + script — for instance, replace rewrite IHn with + something else and watch Coq object — or state and prove your + own lemma in the editor.

- jsCoq provides many other packages, - including Coq's standard library and the - mathematical components - library. - Feel free to experiment, and bear with the beta status of this demo. -

-

- ¡Salut! + This embedded build ships Coq's standard library packages + (arithmetic, collections, reals). The full ECHIDNA platform + drives Coq and many other provers through one dispatch + pipeline — see the + platform documentation.

-

The dev team

+

The jsCoq dev team

- diff --git a/site/docs/api/core.md b/site/docs/api/core.md new file mode 100644 index 00000000..58e86e52 --- /dev/null +++ b/site/docs/api/core.md @@ -0,0 +1,181 @@ +--- +title: Core Server API Reference +description: HTTP API of the echidna server binary, as hosted at api.nesy-prover.dev +date: 2026-07-28 +template: default +--- + +# Core Server API Reference + +This is the API of the `echidna server` binary — the service hosted at +`https://api.nesy-prover.dev` and the one you get from the published +container image. Self-hosted instances serve the same routes over plain +HTTP on the port given to `--port` (default 8081); the public instance +is the same service behind a TLS-terminating proxy. + +Every route below is documented from `src/rust/server.rs`. There is no +authentication; the public instance is rate-limited and caps request +bodies, so treat it as an evaluation endpoint rather than a backend for +production workloads. + +Prover names are the `ProverKind` variant names — `Z3`, `CVC5`, `Coq`, +`Lean`, `Isabelle`, `Agda`, `Metamath`, `HOLLight`, and so on. Use +`/api/provers` for the list your instance actually exposes. + +## Service + +### Health + +``` +GET /api/health +``` + +```json +{ "status": "ok", "version": "2.3.0" } +``` + +`GET /api/diagnostics/health` returns a richer report covering solver +availability and pipeline state. `GET /.well-known/groove` returns the +service's Groove capability manifest. + +### List provers + +``` +GET /api/provers +``` + +```json +{ "provers": [ { "name": "Z3", "tier": 1, "complexity": 2 } ] } +``` + +## Proving and verification + +### Verify a proof or SMT script + +``` +POST /api/verify +``` + +Request: + +```json +{ "prover": "Z3", "content": "(assert (forall ((x Int)) (= (+ x 0) x)))(check-sat)" } +``` + +Response — `outcome` is the primary field (one of `PROVED`, +`NO_PROOF_FOUND`, `INVALID_INPUT`, `UNSUPPORTED_FEATURE`, `TIMEOUT`, +`INCONSISTENT_PREMISES`, `PROVER_ERROR`, `SYSTEM_ERROR`); `valid` is a +backward-compatible boolean that is true exactly when the outcome is +`PROVED`: + +```json +{ + "valid": true, + "outcome": "PROVED", + "goals_remaining": 0, + "tactics_used": 0 +} +``` + +`POST /api/verify_parallel` takes the same request shape and dispatches +across the portfolio. + +### Verify with raw prover output + +``` +POST /api/verify_raw +``` + +Same request shape as `/api/verify`. The response exposes the backend +process result directly, which is what you want when debugging a script: + +```json +{ "valid": true, "exit_code": 0, "stdout": "unsat\n", "stderr": "", "message": "" } +``` + +### Prove a goal + +``` +POST /api/prove +``` + +```json +{ "prover": "Coq", "content": "Lemma t : forall n, n + 0 = n.", "timeout": 30, "neural": false } +``` + +```json +{ "success": true, "goals": 0, "message": "" } +``` + +`timeout` is in seconds and optional; `neural` optionally enables +neural premise selection. + +### Suggest tactics + +``` +POST /api/suggest +``` + +```json +{ "prover": "Coq", "content": "forall n : nat, n + 0 = n", "limit": 5 } +``` + +```json +{ "suggestions": ["induction n", "simpl", "reflexivity"] } +``` + +Suggestions come from the Julia ML service when it is reachable and +fall back to the prover's built-in heuristics otherwise, so this route +works on instances with no ML sidecar. + +### Search + +``` +GET /api/search?q= +``` + +The `q` parameter is required; a request without it returns 400. + +```json +{ "results": ["Nat.add_0_r"], "count": 1 } +``` + +## Interactive sessions + +Sessions hold proof state in server memory across tactic applications. + +### Create a session + +``` +POST /api/session/create +``` + +```json +{ "prover": "Coq" } +``` + +```json +{ "session_id": "b3f1c2de-..." } +``` + +### Inspect and drive a session + +``` +GET /api/session/{id}/state +POST /api/session/{id}/apply +GET /api/session/{id}/tree +``` + +`state` returns `{ "goals": 1, "complete": false, "tactics_applied": 0 }`. +`apply` takes `{ "tactic": "induction n" }` and reports +`{ "success": true, "complete": false, "goals_remaining": 2, ... }`. +`tree` returns the proof tree built so far. + +## Other routes + +`POST /api/agent/plan` performs Pareto-ranked prover selection from +goal aspect tags. `GET /api/aspect-tags` lists the tag vocabulary. +`POST /api/tactics/suggest` and `GET /api/theorems/search` back the +bundled UI. + +[Documentation index](/docs/index.html) diff --git a/site/docs/api/graphql.md b/site/docs/api/graphql.md new file mode 100644 index 00000000..5a11aa7d --- /dev/null +++ b/site/docs/api/graphql.md @@ -0,0 +1,159 @@ +--- +title: GraphQL Interface Reference +date: 2026-07-28 +template: default +--- + +# GraphQL Interface Reference + +The `echidna-graphql` binary is an optional self-hosted service. It +binds `127.0.0.1:8081` over plain HTTP and serves both the GraphQL +endpoint and the interactive playground at the server root — a `POST` +to `/` executes operations, a `GET` renders the playground. There is a +separate `GET /health`. + +Documented from `src/interfaces/graphql/{main,schema}.rs`. + +## Queries + +### provers + +```graphql +query { + provers { + kind + version + tier + complexity + available + } +} +``` + +### proofState + +Takes `id`, not a session identifier: + +```graphql +query { + proofState(id: "proof-uuid") { + id + prover + goal + status + proofScript + goalsRemaining + timeElapsed + errorMessage + } +} +``` + +### listProofs + +```graphql +query { + listProofs(limit: 20) { + id + prover + status + goalsRemaining + } +} +``` + +### suggestTacticsByProofId + +The query form of tactic suggestion, keyed by an existing proof: + +```graphql +query { + suggestTacticsByProofId(proofId: "proof-uuid", limit: 5) { + name + args + description + confidence + } +} +``` + +### proverStatus + +```graphql +query { + proverStatus(prover: "Coq") { + available + } +} +``` + +## Mutations + +### submitProof + +```graphql +mutation { + submitProof(goal: "forall n : nat, n + 0 = n", prover: COQ) { + id + status + goalsRemaining + } +} +``` + +### applyTactic + +`proofId`, `tactic`, and `args` are all required; pass an empty list +when the tactic takes no arguments: + +```graphql +mutation { + applyTactic(proofId: "proof-uuid", tactic: "induction", args: ["n"]) { + id + status + proofScript + goalsRemaining + } +} +``` + +### verifyProof + +Verifies prover source directly, without a proof session: + +```graphql +mutation { + verifyProof(prover: "Z3", content: "(check-sat)") { + status + message + proverOutput + durationMs + artifacts + } +} +``` + +### suggestTactics + +Tactic suggestion is a **mutation**, not a query, and takes a goal +state rather than a proof identifier: + +```graphql +mutation { + suggestTactics(prover: "Coq", context: "", goalState: "forall n : nat, n + 0 = n") { + tactic + confidence + explanation + } +} +``` + +### cancelProof + +```graphql +mutation { + cancelProof(proofId: "proof-uuid") +} +``` + +[Documentation index](/docs/index.html) diff --git a/site/docs/api/grpc.md b/site/docs/api/grpc.md new file mode 100644 index 00000000..d90cbee8 --- /dev/null +++ b/site/docs/api/grpc.md @@ -0,0 +1,129 @@ +--- +title: gRPC Interface Reference +date: 2026-07-28 +template: default +--- + +# gRPC Interface Reference + +The `echidna-grpc` binary is an optional self-hosted service listening +on `localhost:50051`. The authoritative schema is +`src/interfaces/grpc/proto/echidna.proto`; everything below is taken +from it. + +## Service definition + +```protobuf +service ProofService { + rpc SubmitProof (SubmitProofRequest) returns (ProofResponse); + rpc GetProofStatus (GetProofStatusRequest) returns (ProofResponse); + rpc StreamProof (StreamProofRequest) returns (stream ProofUpdate); + rpc ApplyTactic (ApplyTacticRequest) returns (TacticResponse); + rpc CancelProof (CancelProofRequest) returns (CancelProofResponse); + rpc ListProvers (ListProversRequest) returns (ListProversResponse); + rpc SuggestTactics (SuggestTacticsRequest) returns (SuggestTacticsResponse); +} +``` + +## Methods + +### SubmitProof + +Submit a goal for verification. `prover` is the `ProverKind` enum and +the timeout is expressed in seconds. + +```protobuf +message SubmitProofRequest { + string goal = 1; + ProverKind prover = 2; + optional uint32 timeout_seconds = 3; +} + +message ProofResponse { + string proof_id = 1; + ProverKind prover = 2; + string goal = 3; + ProofStatus status = 4; + repeated string proof_script = 5; + optional double time_elapsed = 6; + optional string error_message = 7; +} +``` + +`GetProofStatus` takes `{ proof_id }` and returns the same +`ProofResponse`. + +### StreamProof + +Streams progress for a proof that has already been submitted, so the +request is just its identifier: + +```protobuf +message StreamProofRequest { + string proof_id = 1; +} + +message ProofUpdate { + string proof_id = 1; + ProofStatus status = 2; + string message = 3; + optional double progress = 4; +} +``` + +### ApplyTactic + +Note the field names: `tactic_name` and a repeated `tactic_args`. + +```protobuf +message ApplyTacticRequest { + string proof_id = 1; + string tactic_name = 2; + repeated string tactic_args = 3; +} + +message TacticResponse { + bool success = 1; + ProofResponse proof_state = 2; +} +``` + +### CancelProof + +Takes `{ proof_id }`, returns `{ success }`. + +### ListProvers + +Takes an empty request and returns `ProverInfo` entries carrying kind, +version, tier, complexity, and availability. + +### SuggestTactics + +Keyed by proof, not by goal text: + +```protobuf +message SuggestTacticsRequest { + string proof_id = 1; + optional uint32 limit = 2; +} + +message Tactic { + string name = 1; + repeated string args = 2; + optional string description = 3; + optional float confidence = 4; +} +``` + +## Connecting + +```bash +grpcurl -plaintext localhost:50051 echidna.ProofService/ListProvers + +grpcurl -plaintext -d '{ + "goal": "forall n, n + 0 = n", + "prover": "COQ" +}' localhost:50051 echidna.ProofService/SubmitProof +``` + +[Documentation index](/docs/index.html) diff --git a/site/docs/api/rest.md b/site/docs/api/rest.md new file mode 100644 index 00000000..a28085fc --- /dev/null +++ b/site/docs/api/rest.md @@ -0,0 +1,106 @@ +--- +title: REST Interface Reference +date: 2026-07-28 +template: default +--- + +# REST Interface Reference + +The `echidna-rest` binary is an optional self-hosted service that +exposes an OpenAPI-documented `/api/v1` surface, separate from the +[core server API](/docs/api/core.html). It binds `127.0.0.1:8000` over +plain HTTP — put it behind a TLS-terminating proxy before exposing it. + +Documented from `src/interfaces/rest/{main,handlers,models}.rs`. + +## Endpoints + +### Health check + +``` +GET /health +``` + +Note that health sits at the server root, not under `/api/v1`. + +### Provers + +``` +GET /api/v1/provers +GET /api/v1/provers/{kind} +``` + +Each entry carries the prover kind, version string, tier, complexity, +and whether the backend binary is available on this host: + +```json +{ "kind": "Coq", "version": "8.19", "tier": 1, "complexity": 3, "available": true } +``` + +`{kind}` is a `ProverKind` variant name, for example `Coq`, `Lean`, `Z3`. + +### Proofs + +``` +POST /api/v1/proofs +GET /api/v1/proofs +GET /api/v1/proofs/{id} +DELETE /api/v1/proofs/{id} +``` + +Submit request — the timeout field is `timeout_seconds` and is optional: + +```json +{ + "goal": "forall n : nat, n + 0 = n", + "prover": "Coq", + "timeout_seconds": 30 +} +``` + +Response: + +```json +{ + "id": "proof-uuid", + "prover": "Coq", + "goal": "forall n : nat, n + 0 = n", + "status": "Verified", + "proof_script": ["induction n", "reflexivity"], + "time_elapsed": 0.42 +} +``` + +`error_message` is present only on failure. + +### Tactics + +``` +POST /api/v1/proofs/{id}/tactics +``` + +The request is a tactic name plus its arguments; `args` is required and +may be an empty array: + +```json +{ "name": "induction", "args": ["n"] } +``` + +The response wraps the updated proof state: + +```json +{ "success": true, "proof_state": { "id": "proof-uuid", "status": "InProgress" } } +``` + +### Exchange and consultation + +``` +GET /api/v1/proofs/{id}/export +POST /api/v1/exchange/import +POST /api/v1/consult +``` + +`export` and `import` move proofs across provers via the exchange +layer; `consult` runs a portfolio consultation. + +[Documentation index](/docs/index.html) diff --git a/site/docs/index.md b/site/docs/index.md new file mode 100644 index 00000000..429e2a07 --- /dev/null +++ b/site/docs/index.md @@ -0,0 +1,81 @@ +--- +title: ECHIDNA Platform Documentation +description: Architecture, features, and API quick start +date: 2026-07-28 +template: default +--- + +# Platform Documentation + +**Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance** + +A trust-hardened neurosymbolic theorem proving platform supporting a broad +portfolio of prover backends with a comprehensive verification pipeline. + +## Features + +- **Prover portfolio**: Coq, Lean 4, Isabelle/HOL, Z3, CVC5, Agda, Idris2, and many more — see the canonical tier table in the repository's `docs/PROVER_COUNT.md` +- **Trust pipeline**: solver integrity, proof certificates, axiom tracking, confidence scoring +- **API interfaces**: REST (OpenAPI), GraphQL, gRPC +- **Neural premise selection**: Julia ML layer with tactic prediction +- **Proof exchange**: cross-prover via OpenTheory and Dedukti + +## API Quick Start + +The hosted core server at `https://api.nesy-prover.dev` exposes the +primary HTTP API: + +```bash +curl https://api.nesy-prover.dev/api/health +curl https://api.nesy-prover.dev/api/provers +``` + +Verifying an SMT script takes a prover name and its source: + +```bash +curl -X POST https://api.nesy-prover.dev/api/verify \ + -H "Content-Type: application/json" \ + -d '{"prover": "Z3", "content": "(assert (forall ((x Int)) (= (+ x 0) x)))(check-sat)"}' +``` + +See the [core server API reference](/docs/api/core.html) for every +route. A self-hosted instance serves the same routes over plain HTTP on +the port passed to `--port` (default 8081) — front it with a TLS proxy +before exposing it. + +Three further interface services ship as separate optional binaries, +each binding loopback over plain HTTP: + +### REST interface (port 8000) + +An OpenAPI-documented `/api/v1` surface — see the +[REST interface reference](/docs/api/rest.html). + +### GraphQL interface (port 8081) + +Endpoint and interactive playground both at the server root — see the +[GraphQL interface reference](/docs/api/graphql.html). + +### gRPC interface (port 50051) + +See the [gRPC interface reference](/docs/api/grpc.html) and the proto +definition at `src/interfaces/grpc/proto/echidna.proto`. + +## Architecture + +ECHIDNA follows a trust-hardened architecture: + +1. **Solver Binary Integrity** — SHAKE3-512 + BLAKE3 verification +2. **SMT Portfolio Solving** — cross-checking across solvers +3. **Proof Certificate Checking** — Alethe, DRAT/LRAT, TSTP +4. **Axiom Usage Tracking** — 4 danger levels (Safe, Noted, Warning, Reject) +5. **Solver Sandboxing** — Podman, bubblewrap, or none +6. **Confidence Scoring** — 5-level trust hierarchy +7. **Mutation Testing** — specification robustness testing + +## License + +AGPL-3.0-or-later. Source at +[github.com/hyperpolymath/echidna](https://github.com/hyperpolymath/echidna). + +[Back to home](/index.html) diff --git a/site/index.md b/site/index.md new file mode 100644 index 00000000..a8acb9e1 --- /dev/null +++ b/site/index.md @@ -0,0 +1,66 @@ +--- +title: ECHIDNA — Neurosymbolic Theorem Proving +description: Trust-hardened neurosymbolic theorem proving platform +date: 2026-07-28 +template: default +--- + +# ECHIDNA + +**Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance** + +ECHIDNA is a trust-hardened neurosymbolic theorem-proving platform. A Rust +core orchestrates a broad portfolio of interactive proof assistants, SMT +solvers, first-order ATPs, and constraint solvers behind a single dispatch +pipeline, with neural premise selection and tactic prediction provided by a +Julia ML layer. + +Every proof result passes through a trust-hardening pipeline before it is +reported: solver-binary integrity verification, portfolio cross-checking, +proof-certificate checking, axiom-usage tracking, sandboxed execution, and +statistical confidence scoring. + +## Explore + +- [Platform documentation](/docs/index.html) — architecture, features, and API quick start +- [Core server API](/docs/api/core.html) — the API served at api.nesy-prover.dev +- [REST interface](/docs/api/rest.html) +- [GraphQL interface](/docs/api/graphql.html) +- [gRPC interface](/docs/api/grpc.html) +- [Coq playground](/playground/) — prove theorems in your browser with jsCoq + +## Live API + +A public instance of the ECHIDNA core server is available at +`https://api.nesy-prover.dev`. + +Check service health: + +```bash +curl https://api.nesy-prover.dev/api/health +``` + +List the core prover backends: + +```bash +curl https://api.nesy-prover.dev/api/provers +``` + +Verify a small SMT goal with Z3: + +```bash +curl -X POST https://api.nesy-prover.dev/api/verify \ + -H 'Content-Type: application/json' \ + -d '{"prover": "Z3", "content": "(assert (forall ((x Int)) (= (+ x 0) x)))(check-sat)"}' +``` + +The public instance is rate-limited and intended for evaluation. For +sustained or private use, run your own instance — the container image is +published at `ghcr.io/hyperpolymath/echidna`. + +## Source and license + +ECHIDNA is free software, licensed under AGPL-3.0-or-later. Development +happens at +[github.com/hyperpolymath/echidna](https://github.com/hyperpolymath/echidna), +where issues and contributions are welcome.