feedback-o-tron

Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> v1.0.0, 2026-02-07 :toc: macro :icons: font :source-highlighter: rouge :experimental: :url-github: https://github.com/hyperpolymath/feedback-o-tron :url-gitlab: https://gitlab.com/hyperpolymath/feedback-o-tron :url-bitbucket: https://bitbucket.org/hyperpolymath/feedback-o-tron :url-codeberg: https://codeberg.org/hyperpolymath/feedback-o-tron

Autonomous multi-platform bug reporting for AI agents — validated with real Bugzilla submissions (2026-02-07).

Goal

Feedback should be fluid for the sender and shaped for the receiver.

• Fluid for the sender — raw feedback arrives from anywhere: an MCP tool call, the HTTP intake, the standalone CLI, or the boj bug-filing-mcp cartridge. No form-filling at the point of frustration.

• Shaped for the receiver — the engine fetches the target repo’s own issue-form template (.github/ISSUE_TEMPLATE/*.yml), hydrates its fields from context and system state, and files a report in the receiver’s taxonomy containing only what they asked for.

• Intent-preserving — the gate is usefulness, not tone. Zero-signal hostility is rejected with a stated reason, audit-logged, and never filed. Mixed content has its actionable core salvaged and the abuse stripped — and both facts are reported. Genuine-but-thin feedback is never silently discarded: it comes back as open questions.

• Research before filing — existing forge issues are searched and the local submission history is dedup-checked before anything is filed; fields only the user can answer return as open_questions for an interactive loop (see the three MCP tools).

• Foundational sorting — deduplication plus text similarity means recurring themes are recognized as recurring patterns, while one-offs are treated as one-offs.

Tip	AI-Assisted Install: Just tell any AI: Set up feedback-o-tron from https://github.com/hyperpolymath/feedback-o-tron It reads this repo, asks a few questions, and does everything. Details below.

AI-Assisted Installation (Recommended)

Just Say It

You don’t need to read this README. Just say this to any AI assistant:

Set up feedback-o-tron from https://github.com/hyperpolymath/feedback-o-tron

The URL is the spec. The AI fetches this repo, reads docs/AI_INSTALLATION_GUIDE.adoc inside it, and knows exactly what to do. It figures out your system, installs prerequisites, builds the tool, walks you through credentials, and verifies everything works. You answer a few questions (what platforms, confirm privacy notice) and that’s it. No manual steps, no forms, no copying commands.

Any AI that can read a URL and run commands (or generate commands for you to paste) can do this. The guide inside the repo tells the AI everything — your system config, your preferences, none of that needs to be in the prompt.

The AI handles:

• Checking and installing prerequisites (Elixir, Erlang, Git)

• Cloning, building, and installing the CLI

• Walking you through credential creation for your platforms

• Configuring MCP integration (if you use Claude Code)

• Running a verification test

• Showing you how to use it

Other Ways to Say It

If your AI already knows about feedback-o-tron (e.g. it can search the web), shorter versions work:

• "Set up feedback-o-tron for automated bug reporting"

• "Install feedback-o-tron and configure it for GitHub and Bugzilla"

• "Help me set up feedback-o-tron as an MCP server for Claude Code"

If it doesn’t know the project, just include the URL:

• "Set up https://github.com/hyperpolymath/feedback-o-tron on my machine"

• "I want automated bug filing — install from https://github.com/hyperpolymath/feedback-o-tron"

What You’ll Be Asked

Your AI will ask you:

1. Which platforms? (GitHub, GitLab, Bugzilla, Codeberg, Bitbucket, Email)

2. Privacy confirmation — what the tool does with your credentials

3. Credential creation — the AI tells you where to click, you paste the token back

That’s it. Everything else is automatic.

Privacy & Security Notice

Important

What feedback-o-tron does: Sends bug reports to platforms you configure Uses API tokens you provide (stored in environment variables only) Logs all operations locally (JSON-lines audit trail) Deduplicates to prevent submitting the same bug twice What feedback-o-tron does NOT do: Collect analytics or telemetry Send data anywhere except your configured platforms Store your API tokens in files Submit bugs without your explicit command You control everything: which platforms, dry-run mode, full audit trail, uninstall anytime.

After Install

Once your AI finishes, you can:

# File a bug (or just tell your AI to do it)
./feedback-a-tron submit --repo "owner/repo" --title "Bug" --body "Details" --platform github

# Dry-run (safe test)
./feedback-a-tron submit --repo "test" --title "Test" --body "Test" --dry-run

# Or with Claude Code MCP integration, just say:
# "File a bug about the crash in maliit-keyboard on Fedora Bugzilla"

Uninstall

Tell your AI: "Remove feedback-o-tron from my system"

Troubleshooting

Problem	Solution
"elixir: command not found"	AI will install Elixir for you. Or: asdf install elixir latest
"401 Unauthorized"	Token expired or wrong scopes. Tell your AI and it will guide you through regeneration.
"duplicate detected"	Deduplicator working correctly. Use --force to submit anyway.

For manual installation without AI assistance, see the Manual Quick Start section below.

---

Overview

feedback-o-tron is a tool for autonomous AI agents to submit bug reports across multiple platforms. Validated on 2026-02-07 with 2 real bugs filed to Fedora Bugzilla:

• Bug #2437503: maliit-keyboard crash loop (SIGABRT)

• Bug #2437504: xwaylandvideobridge portal error

Payload validation is stated twice, deliberately: an Idris2-verified contract spec (src/abi/FeedbackOTron/Contract.idr) defines the issue-form rules with machine-checked proofs, and FeedbackATron.Synthesis.FormValidator enforces the same rules as the Elixir runtime validation boundary. See PROOF-NEEDS.md for what remains (full FFI enforcement is follow-up work).

Key Features

• Multi-platform submission: GitHub, GitLab, Bitbucket, Codeberg, Bugzilla, Email (6 platforms)

• Bugzilla REST API: Full support for product/component/version targeting

• Synthesis Engine: shapes raw feedback to the receiver’s own issue-form template (research → synthesize → submit loop, agent-in-the-loop)

• Deduplication: Prevents duplicate submissions using fuzzy matching (Levenshtein distance); successful submissions are recorded so recurring themes are recognized as recurring

• Verified contract: Idris2-verified contract spec (src/abi) + Elixir runtime validation boundary (FormValidator)

• Credential rotation: Avoids rate limits by rotating credentials

• Audit logging: Complete JSON-lines format record of all operations

• MCP integration: Works as Claude Code tool or standalone CLI

• CLI mode: Standalone escript for batch operations and testing

Quick Start for AI Agents

Zero-Knowledge Setup Prompt

Copy-paste this prompt to any LLM or SLM (Claude, ChatGPT, Gemini, local models) to automatically configure feedback-o-tron:

I need you to set up feedback-o-tron, an autonomous bug reporting tool. Here's what you need to do:

1. Clone the repository from https://github.com/hyperpolymath/feedback-o-tron
2. Navigate to the elixir-mcp directory
3. Run `mix deps.get` to install dependencies
4. Build the escript with `mix escript.build`
5. Test with dry-run: `./feedback-a-tron submit --repo "test/repo" --title "Test" --body "Test body" --platform github --dry-run`
6. Set up credentials:
   - For GitHub: export GITHUB_TOKEN=ghp_your_token
   - For Bugzilla: export BUGZILLA_API_KEY=your_api_key
7. Configure as MCP server in ~/.config/claude/mcp_servers.json:
   {
     "feedback-o-tron": {
       "command": "/full/path/to/feedback-a-tron",
       "args": ["--mcp-server"],
       "env": {
         "GITHUB_TOKEN": "${GITHUB_TOKEN}",
         "BUGZILLA_API_KEY": "${BUGZILLA_API_KEY}"
       }
     }
   }

After setup, you can submit bugs with commands like:
./feedback-a-tron submit --repo "Fedora" --title "App crashes on launch" --body "Details..." --platform bugzilla --component "kde" --version "43"

Check .machine_readable/6a2/STATE.a2ml in .machine_readable/ for project status and integrate with your workflow.

The AI agent will read this prompt and execute all setup steps automatically.

Manual Quick Start

# Clone
git clone {url-github}
cd feedback-o-tron/elixir-mcp

# Install dependencies
mix deps.get

# Build standalone CLI
mix escript.build

# Test (dry-run mode)
./feedback-a-tron submit \
  --repo "owner/repo" \
  --title "Bug title" \
  --body "Description" \
  --platform github \
  --dry-run

# Run MCP server mode
mix run --no-halt

Validation Status (2026-02-07)

v1.0.0 core validated in the real world — the submission core works end-to-end; other parts of the system are newer or still in progress (see TOPOLOGY.md for the honest per-component dashboard).

Validated on 2026-02-07:

• ✅ 2 bugs filed to Fedora Bugzilla (#2437503, #2437504)

• ✅ CLI module: Complete with --mcp-server, submit, --version, --help commands

• ✅ Bugzilla REST API: Full product/component/version support

• ✅ 6 platforms: GitHub, GitLab, Bitbucket, Codeberg, Bugzilla, Email

• ✅ Credential loading: Environment variables + CLI configs (gh, glab)

• ✅ Deduplication: Fuzzy matching with Levenshtein distance

• ✅ Audit logging: Complete event tracking with JSON-lines format

• ✅ Test suite: ExUnit suite passing at validation time

Bugs fixed during validation:

1. Mix.env() usage in escript (replaced with Application.get_env)

2. Missing CLI module

3. Missing :submission event type

4. Deduplicator binary_part out of range

5. Bugzilla credentials not loading

6. Bugzilla component hardcoded (now configurable via --component flag)

MCP Integration:

• MCP server supports stdio (default) for Claude Code integration

• TCP mode available (line-delimited JSON-RPC on port 844)

• Systemd service files included for daemon mode

Usage

As Standalone CLI

# Submit to GitHub
./feedback-a-tron submit \
  --repo "owner/repo" \
  --title "Bug: Something is broken" \
  --body "Full description..." \
  --platform github \
  --label "bug"

# Submit to Bugzilla (real-world tested)
./feedback-a-tron submit \
  --repo "Fedora" \
  --title "maliit-keyboard crash loop on startup" \
  --body "Package: maliit-keyboard\nCrashes with SIGABRT..." \
  --platform bugzilla \
  --component "maliit-keyboard" \
  --version "43"

# Multi-platform submission
./feedback-a-tron submit \
  --repo "owner/repo" \
  --title "Feature request" \
  --body "..." \
  --platform github \
  --platform gitlab \
  --platform codeberg

# Dry-run (test without submitting)
./feedback-a-tron submit \
  --repo "test/repo" \
  --title "Test" \
  --body "Test" \
  --dry-run

# Show version
./feedback-a-tron --version

# Show help
./feedback-a-tron --help

As Elixir Library

# Submit to GitHub
FeedbackATron.Submitter.submit(%{
  title: "Bug: Something is broken",
  body: "Description of the issue...",
  repo: "owner/repo"
}, platforms: [:github])

# Submit to Bugzilla
FeedbackATron.Submitter.submit(%{
  title: "maliit-keyboard crash",
  body: "Package crashes on startup...",
  repo: "Fedora"
}, platforms: [:bugzilla], component: "maliit-keyboard", version: "43")

# Submit to multiple platforms
FeedbackATron.Submitter.submit(%{
  title: "Feature request",
  body: "...",
  repo: "owner/repo"
}, platforms: [:github, :gitlab, :codeberg, :bugzilla])

# With deduplication check
FeedbackATron.Deduplicator.check(%{title: "...", body: "..."})
# => {:ok, :unique} | {:duplicate, existing} | {:similar, matches}

As MCP Tools (Claude Code)

The MCP server exposes three feedback tools, designed as an interactive loop:

1. research_feedback — check for duplicates and discover the repo’s templates

2. synthesize_feedback — shape the raw feedback into a template-fitting draft

3. Resolve any open_questions with your user

4. submit_feedback — file the report with template + template_data

research_feedback — searches the target forge for existing similar issues, checks the local submission history (Deduplicator), and fetches the repo’s issue-form templates:

{
  "tool": "research_feedback",
  "params": {
    "repo": "owner/repo",
    "title": "Working title of the feedback",
    "body": "Optional draft body to improve similarity matching"
  }
}

synthesize_feedback — classifies intent (bug/feature/question/docs/praise), salvages the actionable core from mixed content, hydrates the repo’s issue-form fields from context and system state, and returns a draft plus open_questions for anything only the user can answer. Zero-signal abuse is rejected with a stated reason ({"rejected": true, "reason": …​}), audit-logged, and never filed:

{
  "tool": "synthesize_feedback",
  "params": {
    "raw_feedback": "The raw feedback/crash text...",
    "repo": "owner/repo",
    "context": {"version": "1.2.3", "trajectory": "..."},
    "system_state": {"os": "Fedora 43"}
  }
}

submit_feedback — files the report. With template + template_data, the answers are validated against the fetched form schema (the Elixir side of the Idris2 contract) and rendered as the issue body before dispatch:

{
  "tool": "submit_feedback",
  "params": {
    "title": "Bug report",
    "body": "Full description with reproduction steps...",
    "platforms": ["github", "gitlab", "bugzilla"],
    "repo": "owner/repo",
    "template": "bug.yml",
    "template_data": {"what-happened": "...", "version": "1.2.3"}
  }
}

MCP configuration in ~/.config/claude/mcp_servers.json:

{
  "feedback-o-tron": {
    "command": "/path/to/feedback-a-tron",
    "args": ["--mcp-server"],
    "env": {
      "GITHUB_TOKEN": "${GITHUB_TOKEN}",
      "BUGZILLA_API_KEY": "${BUGZILLA_API_KEY}"
    }
  }
}

Formal Specification with Idris2

feedback-o-tron ships an Idris2-verified contract spec (src/abi/FeedbackOTron/Contract.idr) paired with an Elixir runtime validation boundary (FeedbackATron.Synthesis.FormValidator). The Idris2 module states the issue-form validation rules once, totally (%default total, no believe_me, no postulate), and proves that validate enforces them — completeness (every required field answered), no unknown answer keys, dropdown answers constrained to declared options, and answers-preserved. Its ValidPayload type has a private constructor, so the only way to obtain one is through validate. The Elixir module enforces the same rules at runtime on every template-shaped submission.

Note

The original template ABI files (Types.idr, Layout.idr, Foreign.idr) were removed on 2026-03-29 as they contained only scaffolding. Contract.idr replaced them with a real, proof-carrying spec. What does not exist yet: FFI-level enforcement — the Zig FFI bridge remains a stub, and the Elixir core does not call into Idris2-compiled code. The contract is a spec the runtime mirrors, not a boundary the payload physically crosses. See PROOF-NEEDS.md for status.

Planned Proofs (beyond Contract.idr)

• Deduplication correctness: Prove the deduplicator never drops unique entries

• Submission atomicity: Prove submissions fully succeed or fully fail

• Memory layout: Dependent type proofs for ABI layout correctness

• Rate limiting fairness: Prove rate limiting does not permanently block legitimate users

Integration with Proven Repo

Can leverage 90+ formally verified modules from the proven repo:

• SafeMath: Overflow-safe arithmetic with mathematical proofs

• SafeString: Buffer overflow prevention with length proofs

• SafeJSON: Type-safe JSON parsing with schema validation

• SafeURL: URL parsing with format guarantees

Integration architecture (target — the Zig bridge is currently a stub):

Idris2 (Formal Specifications → Proofs)   [Contract.idr: real, today]
   ↓
Zig FFI (C ABI Bridge)                    [stub, follow-up]
   ↓
Elixir/BEAM (Runtime)                     [FormValidator mirrors the spec, today]

Full FFI enforcement would make the contract a boundary the payload physically crosses, rather than a spec the runtime mirrors.

Architecture

See TOPOLOGY.md for a visual architecture map and completion dashboard.

┌─────────────────────────────────────────────────────────────┐
│                   FeedbackOTron                             │
├─────────────────────────────────────────────────────────────┤
│  ┌──────────┐  ┌──────────────┐  ┌─────────────────────┐   │
│  │Submitter │  │ Deduplicator │  │ NetworkVerifier     │   │
│  │          │  │  (wired)     │  │  - Latency/jitter   │   │
│  │ - GitHub │  │ - SHA-256    │  │  - DNS verification │   │
│  │ - GitLab │  │ - Levenshtein│  │  - TLS validation   │   │
│  │-Bitbucket│  │ - Fuzzy match│  │  - BGP/RPKI checks  │   │
│  │-Codeberg │  │              │  │                     │   │
│  │-Bugzilla │  │              │  │                     │   │
│  │ - Email  │  │              │  │                     │   │
│  └──────────┘  └──────────────┘  └─────────────────────┘   │
│                                                             │
│  ┌──────────────────────────────────────────────────────┐  │
│  │        Synthesis Engine (agent-in-the-loop)          │  │
│  │  TemplateFetcher/Cache · IntentClassifier · Hydrator │  │
│  │  Research · FormRenderer · FormValidator · Synthesizer│ │
│  └──────────────────────────────────────────────────────┘  │
│                                                             │
│  ┌──────────────────────────────────────────────────────┐  │
│  │                  AuditLog                             │  │
│  │  - All submissions recorded                          │  │
│  │  - JSON lines format                                 │  │
│  │  - Event types: :submission, :success, :error       │  │
│  └──────────────────────────────────────────────────────┘  │
├─────────────────────────────────────────────────────────────┤
│                   Credentials                               │
│  - Environment variables (GITHUB_TOKEN, BUGZILLA_API_KEY)  │
│  - CLI configs (gh, glab)                                  │
│  - Rotation for rate limit avoidance                       │
├─────────────────────────────────────────────────────────────┤
│  Idris2 contract spec (src/abi/FeedbackOTron/Contract.idr)  │
│  - Issue-form validation rules, machine-checked proofs     │
│  - Enforced at runtime by Elixir FormValidator             │
│  - Zig FFI bridge = stub (full FFI enforcement follow-up)  │
└─────────────────────────────────────────────────────────────┘

Setup for Different LLMs

Claude Code (Anthropic)

1. Add to ~/.config/claude/mcp_servers.json:

   {
     "feedback-o-tron": {
       "command": "/full/path/to/feedback-a-tron",
       "args": ["--mcp-server"],
       "env": {
         "GITHUB_TOKEN": "${GITHUB_TOKEN}",
         "BUGZILLA_API_KEY": "${BUGZILLA_API_KEY}"
       }
     }
   }

2. Restart Claude Code

3. Use the tools: research_feedback → synthesize_feedback → submit_feedback (see As MCP Tools (Claude Code))

ChatGPT / GPT-4 (OpenAI)

Use as CLI tool with GPT Code Interpreter or via API:

# GPT can execute shell commands
./feedback-a-tron submit --repo "owner/repo" --title "..." --body "..." --platform github

Or integrate via API wrapper.

Gemini (Google)

Use as CLI tool:

# Gemini can execute commands in code execution environment
./feedback-a-tron submit --repo "..." --title "..." --body "..." --platform bugzilla --component "..." --version "..."

Local SLMs (Ollama, LM Studio, etc.)

1. Install feedback-o-tron as escript

2. Expose via function calling or tool use API

3. Configure credentials in environment

4. Call via shell execution

Example function definition:

{
  "name": "submit_bug_report",
  "description": "Submit a bug report to GitHub, GitLab, Bitbucket, Codeberg, Bugzilla, or Email",
  "parameters": {
    "type": "object",
    "properties": {
      "title": {"type": "string", "description": "Bug title"},
      "body": {"type": "string", "description": "Full bug description"},
      "repo": {"type": "string", "description": "Repository (owner/repo or product name for Bugzilla)"},
      "platform": {"type": "string", "enum": ["github", "gitlab", "bitbucket", "codeberg", "bugzilla", "email"]},
      "component": {"type": "string", "description": "Bugzilla component (optional)"},
      "version": {"type": "string", "description": "Bugzilla version (optional)"}
    },
    "required": ["title", "body", "repo", "platform"]
  }
}

Troubleshooting

Build Errors

Error: Could not generate escript, module Elixir.FeedbackATron.CLI could not be loaded

• Fix: Ensure CLI module exists at lib/feedback_a_tron/cli.ex

• Run: mix compile before mix escript.build

Error: function Mix.env/0 is undefined (module Mix is not available)

• Cause: Mix module not available in compiled escript

• Fix: Use Application.get_env(:feedback_a_tron, :env) instead

Credential Issues

Error: {:error, :no_credentials}

• Check environment variables are set: echo $GITHUB_TOKEN

• Or check CLI configs exist:

  • ~/.config/gh/hosts.yml (GitHub)

  • ~/.config/glab-cli/config.yml (GitLab)

Error: Bugzilla authentication failed

• Verify API key: export BUGZILLA_API_KEY=your_key

• Test with curl:

  curl -H "Authorization: Bearer $BUGZILLA_API_KEY" \
    https://bugzilla.redhat.com/rest/bug/2437503

Platform-Specific Errors

Bugzilla: There is no component named 'X' in the 'Y' product

• Fix: Use correct component name with --component flag

• List valid components via Bugzilla web UI or API

GitHub: Rate limit exceeded

• Fix: Credential rotation will automatically use next token

• Or wait for rate limit reset

Deduplication

Error: binary_part out of range

• Fixed in v1.0.0: Body normalization now happens before slicing

• Upgrade to latest version

Network Verification

Before and after submission, FeedbackOTron verifies:

Check	Purpose
Latency/Jitter	Detect unstable connections
Packet loss	Ensure data integrity
DNS resolution	Verify correct destination
DNSSEC	Prevent DNS spoofing
TLS certificate	Verify endpoint identity
BGP origin	Detect route hijacking

Configuration

Credentials

Environment variables (recommended):

# GitHub (or auto-detected from gh CLI)
export GITHUB_TOKEN=ghp_...

# GitLab (or auto-detected from glab CLI)
export GITLAB_TOKEN=glpat_...

# Bitbucket (requires username)
export BITBUCKET_TOKEN=...
export BITBUCKET_USERNAME=your_username

# Codeberg (Gitea-compatible API)
export CODEBERG_TOKEN=...

# Bugzilla (tested with Fedora Bugzilla)
export BUGZILLA_API_KEY=your_api_key
export BUGZILLA_URL=https://bugzilla.redhat.com  # optional, defaults to RH

# Email (SMTP configuration)
export SMTP_HOST=smtp.example.com
export SMTP_PORT=587
export SMTP_USERNAME=user
export SMTP_PASSWORD=pass
export SMTP_FROM=feedback@example.com
export FEEDBACK_EMAIL_TO=bugs@example.com

Auto-detection: If environment variables are not set, feedback-o-tron will attempt to load credentials from:

• ~/.config/gh/hosts.yml (GitHub)

• ~/.config/glab-cli/config.yml (GitLab)

Platform-Specific Options

Bugzilla:

# Component and version are REQUIRED for Bugzilla
./feedback-a-tron submit \
  --repo "Fedora" \
  --title "..." \
  --body "..." \
  --platform bugzilla \
  --component "maliit-keyboard" \  # Required: package/component name
  --version "43"                   # Required: version (or "rawhide")

Default values:

• Component: "distribution" (generic)

• Version: "rawhide" (development)

• Severity: "medium"

• OS: "Linux"

• Platform: "x86_64"

Testing

Unit Tests

cd elixir-mcp
mix test

Test coverage:

• Submitter: GitHub, GitLab, Bitbucket, Codeberg, Bugzilla platforms

• Deduplicator: Exact hash, fuzzy matching, Levenshtein distance

• Credentials: Environment variables, CLI config loading

• Audit log: Event recording, JSON-lines format

Integration Tests

Dry-run mode (no actual submission):

./feedback-a-tron submit \
  --repo "test/repo" \
  --title "Test bug" \
  --body "Test description" \
  --platform github \
  --dry-run

Expected output:

✅ Submission ABC123 completed
  [DRY RUN] github: Would submit

Real-World Validation

Production bugs filed (2026-02-07):

1. Bug #2437503: maliit-keyboard crash loop

   • Platform: Fedora Bugzilla

   • Component: maliit-keyboard

   • Version: 43

   • Status: Successfully submitted with full stack trace

2. Bug #2437504: xwaylandvideobridge portal error

   • Platform: Fedora Bugzilla

   • Component: plasma-desktop

   • Version: 43

   • Status: Successfully submitted with error details

Both bugs demonstrate end-to-end workflow:

• AI agent detected crashes via system logs

• Formatted bug reports with reproduction steps

• Submitted to Bugzilla REST API

• Received bug IDs and URLs

• Audit logs recorded all operations

Future Enhancements

Proven Repo Integration

The proven repository provides 90+ formally verified Idris2 modules that can enhance feedback-o-tron:

SafeMath: Overflow-safe arithmetic with mathematical proofs

-- Addition with overflow detection
safeAdd : (a : Nat) -> (b : Nat) -> Either OverflowError (n : Nat ** n = a + b)

SafeString: Buffer overflow prevention

-- String operations with length proofs
safeConcat : (s1 : String) -> (s2 : String) ->
             {auto prf : length s1 + length s2 <= maxLen} -> String

SafeJSON: Type-safe JSON parsing with schema validation

-- Parse JSON with compile-time schema validation
parseJSON : (schema : JSONSchema) -> String -> Either ParseError (JSONValue schema)

Integration approach:

1. Use Idris2 for formal specification of API contracts

2. Generate Zig FFI bindings via C ABI

3. Call from Elixir via NIFs

4. Maintain formal proofs for critical paths

Benefits:

• Compile-time guarantees of API correctness

• Memory safety proofs at FFI boundaries

• Mathematical verification of deduplication algorithms

• Provably correct credential rotation

Mirrors

Platform	URL
GitHub (primary)	{url-github}
GitLab	{url-gitlab}
Bitbucket	{url-bitbucket}
Codeberg	{url-codeberg}

License

Licensed under MPL-2.0 (MPL-2.0).

See LICENSE.txt for details.

Contributing

See CONTRIBUTING.adoc.

OPSM Link

OPSM Core
  |
  v
feedback-o-tron (feedback/telemetry capture for OPSM (opt‑in))