echidnabot

echidnabot — Proof-Aware CI Bot for Formal Verification

When you push code with formal proofs, echidnabot automatically verifies them and reports the results in your pull requests.

The Problem

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

The Solution

echidnabot bridges the gap between code platforms (GitHub, GitLab, Bitbucket) and the ECHIDNA theorem proving platform. Every push, every PR—proofs get verified automatically.

  GitHub/GitLab/Bitbucket
           │
           │ webhook (push/PR)
           ▼
   ┌───────────────────┐
   │    echidnabot     │  ◄── Rust, Tokio, Axum
   │  ┌─────────────┐  │
   │  │ Dispatcher  │──┼──► ECHIDNA Core (Agda, Coq, Lean, Z3...)
   │  │ Scheduler   │  │
   │  │ GraphQL API │  │
   │  └─────────────┘  │
   └───────────────────┘
           │
           │ Check Runs / Comments
           ▼
       ✓ Proof verified
       ✗ Proof failed (line 42: goal not discharged)

Features

Multi-Prover Support

Tier	Provers	Status
Tier 1	Coq, Lean 4, Agda, Isabelle/HOL, Z3, CVC5	Ready
Tier 2	Metamath, HOL Light, Mizar	MVP
Tier 3	PVS, ACL2, HOL4	Planned

Multi-Platform Integration

• GitHub — Check Runs, PR comments, status checks

• GitLab — Merge request pipelines, commit status

• Bitbucket — Build status, PR comments

• Codeberg — Planned

Bot Modes

Like Oikos Bot, echidnabot operates in multiple modes:

• Verifier — Silent pass/fail on proof files

• Advisor — Suggestions on failing proofs

• Consultant — Answer questions about proof state

• Regulator — Block merges on proof failures

ML-Powered Tactic Suggestions

When proofs fail, echidnabot can suggest tactics via ECHIDNA’s Julia ML backend:

❌ Proof failed at theorem `list_append_assoc`
   Goal: ∀ xs ys zs, xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

💡 Suggested tactics:
   1. induction xs; simpl; auto.
   2. intros; rewrite app_assoc; reflexivity.

Quick Start

Installation

# From source
git clone https://github.com/hyperpolymath/echidnabot
cd echidnabot
cargo build --release

# Or with Cargo
cargo install echidnabot

# Or with Guix
guix install echidnabot

Configuration

Create echidnabot.toml in your repository:

[repository]
platform = "github"
owner = "your-org"
name = "your-repo"

[provers]
enabled = ["coq", "lean4", "agda"]

[webhook]
secret = "${ECHIDNABOT_WEBHOOK_SECRET}"

[echidna]
endpoint = "https://echidna.your-domain.com/graphql"

Running the Server

# Start the webhook server
echidnabot serve --port 8080

# Register a repository
echidnabot register --platform github --repo owner/name

# Manually trigger verification
echidnabot check --commit HEAD

Architecture

echidnabot is built in Rust for reliability and performance:

Component	Technology	Purpose
Webhook Server	Axum 0.7	Receive platform events
Job Scheduler	Tokio	Async job queue with priorities
Platform Adapters	Octocrab	GitHub/GitLab/Bitbucket APIs
GraphQL API	async-graphql	Query and control interface
Database	SQLx	SQLite (dev) / PostgreSQL (prod)
ECHIDNA Client	Reqwest	Communicate with proof backends

Project Structure

echidnabot/
├── src/
│   ├── api/              # GraphQL & webhooks
│   │   ├── graphql.rs    # Query/mutation resolvers
│   │   └── webhooks.rs   # Platform webhook handlers
│   ├── adapters/         # Platform integrations
│   │   ├── github.rs     # GitHub Check Runs
│   │   ├── gitlab.rs     # GitLab pipelines
│   │   └── bitbucket.rs  # Bitbucket builds
│   ├── dispatcher/       # ECHIDNA communication
│   ├── scheduler/        # Job queue management
│   ├── store/            # Database models
│   └── main.rs           # CLI entry point
├── docs/                 # Documentation site
├── wiki/                 # GitHub Wiki content
└── justfile              # Task automation

API

GraphQL

# Register a repository
mutation {
  registerRepository(input: {
    platform: GITHUB
    owner: "your-org"
    name: "your-repo"
    enabledProvers: [COQ, LEAN4]
  }) {
    id
    webhookUrl
  }
}

# Query verification status
query {
  job(id: "...") {
    status
    result {
      success
      verifiedFiles
      failedFiles
    }
  }
}

REST Webhooks

POST /webhooks/github   # GitHub webhook endpoint
POST /webhooks/gitlab   # GitLab webhook endpoint
POST /webhooks/bitbucket # Bitbucket webhook endpoint

Development

Prerequisites

• Rust 1.83+ (stable)

• PostgreSQL 15+ (or SQLite for development)

• Access to ECHIDNA Core instance

Using Guix (Recommended)

guix shell -D -f guix.scm
just build
just test

Using Nix

nix develop
just build

Using Cargo Directly

cargo build
cargo test
cargo clippy

Common Tasks

just              # Show all available tasks
just build        # Build debug binary
just test         # Run all tests
just lint         # Run clippy + fmt check
just run          # Start development server
just docs         # Generate documentation

Deployment

Docker

# Build image
podman build -t echidnabot:latest .

# Run with environment config
podman run -d \
  -p 8080:8080 \
  -e ECHIDNABOT_DATABASE_URL=postgres://... \
  -e ECHIDNABOT_ECHIDNA_ENDPOINT=https://... \
  -e GITHUB_WEBHOOK_SECRET=... \
  echidnabot:latest

Systemd

# Install service
sudo cp dist/echidnabot.service /etc/systemd/system/
sudo systemctl enable --now echidnabot

Roadmap

Phase	Target	Features
Phase 1	MVP	GitHub webhooks, Metamath verification, Check Runs
Phase 2	Multi-Prover	Coq, Lean, Agda, Z3 support
Phase 3	Intelligence	ML tactic suggestions, auto-fix PRs
Phase 4	Production	PostgreSQL scaling, horizontal workers, dashboards

Related Projects

• ECHIDNA — The theorem proving platform (backend)

• Oikos Bot — Ecological & economic code analysis

• poly-ssg — Language-native static site generators

• RSR — Repository quality standards

About hyperpolymath

hyperpolymath builds politically autonomous software for ecologically and economically conscious development. Our tools prioritize:

• Formal correctness — Proofs over tests where possible

• Sustainability — Carbon-aware computing

• Independence — No Big Tech dependencies

• Openness — AGPL/MIT licensing, reproducible builds

License

This project is licensed under AGPL-3.0-or-later.

We also encourage adherence to the principles of the Palimpsest License — a framework for consent-based digital interaction.

Contributing

See CONTRIBUTING.adoc for guidelines.

Key points:

• Rust code follows cargo fmt and cargo clippy

• All commits signed with GPG

• PRs require passing CI and proof verification

---

Part of the hyperpolymath ecosystem. Proof-aware CI for mathematically certain software.