SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (hyperpolymath) –>

echidnabot — Proof-Aware CI Bot

The canonical README is README.adoc. This Markdown file exists for renderers that prefer .md (some package indexes, some doc tooling); it is a thin summary that links into the AsciiDoc version for the full story.

---

What is it?

A formal-verification CI bot that orchestrates the ECHIDNA theorem-proving platform for automatic proof verification on every push and pull request. Written in Rust on Tokio/Axum.

Part of the gitbot-fleet (Tier-1 Verifier role), coordinated by Hypatia.

Why does it exist?

You’re writing formally verified software — proofs in Coq, Lean, Agda, or Isabelle. But your CI pipeline doesn’t understand proofs:

• Tests pass, but proofs are broken.

• PRs merge with unverified theorems.

• No one notices until a dependent build fails.

• Manual verification is slow and error-prone.

echidnabot bridges the gap. Push proof files; get verified.

Features (high-level)

• 12 provers via ECHIDNA — Coq, Lean 4, Agda, Isabelle/HOL, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, HOL4 (see wiki/Supported-Provers.md; upstream supports 113, drift documented in EXPLAINME.adoc).

• 3 platforms — GitHub, GitLab, Bitbucket (Codeberg planned).

• 4 bot modes — Verifier / Advisor / Consultant / Regulator (configured via .machine_readable/bot_directives/echidnabot.a2ml).

• Container isolation — podman rootless with bwrap fallback; fail-safe (refuses to run proofs without isolation).

• Trust bridge — 5-level confidence, SHA-256 solver-integrity verification, axiom-usage tracking.

• Retry + circuit breaker — exponential backoff, opens after 5 failures, auto-resets after 5 minutes.

• 184 tests (137 lib + 17 lifecycle + 32 integration + 12 property

  • 15 seam + 8 smoke).

Install / configure / run

# Build (requires gitbot-fleet layout — see CONTRIBUTING.md)
cargo build --release

# Initialise database
echidnabot init-db

# Start the webhook server
export DATABASE_URL=sqlite:echidnabot.db
export ECHIDNA_URL=http://localhost:8080
echidnabot serve --port 8080

Full instructions: wiki/Getting-Started.md and docs/content/configuration.md.

Documentation map

Audience	File
Users (overview)	README.adoc — full canonical README
Users (setup)	wiki/Getting-Started.md
Users (config)	docs/content/configuration.md
Users (FAQ)	wiki/FAQ.md
Devs (architecture)	wiki/Architecture.md
Devs (contrib)	CONTRIBUTING.md
Devs (ABI/FFI)	ABI-FFI-README.md
Devs (roadmap)	ROADMAP.adoc
Devs (claims)	EXPLAINME.adoc — receipts behind README claims
AI assistants	.claude/CLAUDE.md 0-AI-MANIFEST.a2ml
Security	SECURITY.md .well-known/security.txt
Releases	RELEASE_CHECKLIST.md
Compliance	RSR_COMPLIANCE.adoc

License

MPL-2.0 (Palimpsest License). See LICENSE and PALIMPSEST.adoc.

Contributing

See CONTRIBUTING.md and CODE_OF_CONDUCT.md.

Security

Vulnerabilities → SECURITY.md. Do not open public issues for security reports.

---

Maintainer: Jonathan D.A. Jewell — hyperpolymath