Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> v1.0.0, 2026-09-14 :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).
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-mcpcartridge. 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_questionsfor 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: |
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-tronThe 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
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"
Your AI will ask you:
-
Which platforms? (GitHub, GitLab, Bugzilla, Codeberg, Bitbucket, Email)
-
Privacy confirmationβββwhat the tool does with your credentials
-
Credential creationβββthe AI tells you where to click, you paste the token back
Thatβs it. Everything else is automatic.
|
Important
|
What feedback-o-tron does:
What feedback-o-tron does NOT do:
You control everything: which platforms, dry-run mode, full audit trail, uninstall anytime. |
Once your AI finishes, you can:
# File a bug (or just tell your AI to do it)
feedback-o-tron submit --repo "owner/repo" --title "Bug" --body "Details" --platform github
# Dry-run (safe test)
feedback-o-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"| Problem | Solution |
|---|---|
"elixir: command not found" |
Install Elixir from your distribution first: |
"401 Unauthorized" |
The token is expired or lacks scopes. For GitHub, |
"duplicate detected" |
The deduplicator found an existing report. Read it first; if it is genuinely different, change the title so it is. |
For manual installation without AI assistance, see the Manual Quick Start section below.
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).
-
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
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-o-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. Register it as an MCP server:
claude mcp add feedback-o-tron \
-e GITHUB_TOKEN="$GITHUB_TOKEN" \
-- /full/path/to/feedback-o-tron serve
After setup, drafting a report is yours to run and mine to confirm:
./feedback-o-tron submit --repo "owner/repo" --title "..." --body "..." --platform github
The command prints the entire payload and waits for a typed "y". I type
it, not you β with no terminal the command refuses and exits 3. Add
--dry-run to see the payload and send nothing.
Project status is in .machine_readable/6a2/STATE.a2ml.The AI agent will read this prompt and execute all setup steps automatically.
Four things must be installed before the clone: Git, Elixir 1.17 or newer,
Erlang/OTP 27 or newer, and the GitHub CLI (gh). A bare container or a
freshly imaged machine has none of them.
# Fedora/RHEL
sudo dnf install git elixir erlang gh
# Debian/Ubuntu
sudo apt install git elixir erlang gh
# macOS
brew install git elixir ghIf the distributionβs Elixir is older than 1.17, the mise and asdf routes are in the installation guide.
Authentication is needed only for a real send, never for the --dry-run
below. gh auth login lets the GitHub CLI hold the token; GITHUB_TOKEN in
the environment is read first when it is set.
# Clone and build
git clone https://github.com/hyperpolymath/feedback-o-tron
cd feedback-o-tron/elixir-mcp
mix deps.get
mix escript.build
# Check it built
./feedback-o-tron --version # feedback-o-tron v1.0.0
# Preview a report without sending anything
./feedback-o-tron submit \
--repo "owner/repo" \
--title "Bug title" \
--body "Description" \
--platform github \
--dry-run
# Run the engine: MCP on stdin/stdout, HTTP intake on 127.0.0.1:7722
./feedback-o-tron servev1.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:
-
β 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:
-
Mix.env() usage in escript (replaced with Application.get_env)
-
Missing CLI module
-
Missing :submission event type
-
Deduplicator binary_part out of range
-
Bugzilla credentials not loading
-
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), off by default; enable with
FEEDBACK_A_TRON_MCP_TCP=1, port 7979 (FEEDBACK_A_TRON_MCP_TCP_PORT), loopback only -
Systemd service files included for daemon mode
# Submit to GitHub
./feedback-o-tron submit \
--repo "owner/repo" \
--title "Bug: Something is broken" \
--body "Full description..." \
--platform github \
--label "bug"
# Submit to Bugzilla (real-world tested)
./feedback-o-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-o-tron submit \
--repo "owner/repo" \
--title "Feature request" \
--body "..." \
--platform github \
--platform gitlab \
--platform codeberg
# Dry-run (test without submitting)
./feedback-o-tron submit \
--repo "test/repo" \
--title "Test" \
--body "Test" \
--dry-run
# Show version
./feedback-o-tron --version
# Show help
./feedback-o-tron --help# 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}The MCP server exposes three feedback tools, designed as an interactive loop:
-
research_feedbackβ check for duplicates and discover the repoβs templates -
synthesize_feedbackβ shape the raw feedback into a template-fitting draft -
Resolve any
open_questionswith your user -
submit_feedbackβ file the report withtemplate+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"}
}
}Register the server with Claude Code:
claude mcp add feedback-o-tron \
-e GITHUB_TOKEN="$GITHUB_TOKEN" \
-- /full/path/to/feedback-o-tron serveFor a host that takes a JSON config file instead (a project .mcp.json, or
the hostβs own settings file):
{
"mcpServers": {
"feedback-o-tron": {
"command": "/full/path/to/feedback-o-tron",
"args": ["serve"],
"env": {
"GITHUB_TOKEN": "${GITHUB_TOKEN}"
}
}
}
}One command runs everything in one OS process:
./feedback-o-tron serveThat opens two doors:
-
MCP on stdin/stdout, for Claude Code and any other MCP host. With this door open the process exits when stdin closes, so a host that goes away does not leave an orphan behind.
-
HTTP intake on
127.0.0.1:7722, forbojand local tools.GET /healthanswers{"status":"ok","service":"feedback-o-tron","intake":"http"}.
Close either one: --no-stdio, --no-http. Closing both is an error β
there would be nothing to serve. --http-port N moves the intake;
FEEDBACK_O_TRON_HTTP_PORT and FEEDBACK_O_TRON_HTTP_BIND do the same from
the environment.
Nothing is sent from the CLI without a personβs yes. submit prints the
whole payload β every field, exactly as it will be sent β and waits. If
stdin is not a terminal it refuses and exits 3. There is no --yes; use
--dry-run to preview.
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.
|
-
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
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.
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) β
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ-
Register the server:
claude mcp add feedback-o-tron \ -e GITHUB_TOKEN="$GITHUB_TOKEN" \ -- /full/path/to/feedback-o-tron serve -
Restart Claude Code
-
Use the tools:
research_feedbackβsynthesize_feedbackβsubmit_feedback(see As MCP Tools (Claude Code))
Use as CLI tool with GPT Code Interpreter or via API:
# GPT can execute shell commands
./feedback-o-tron submit --repo "owner/repo" --title "..." --body "..." --platform githubOr integrate via API wrapper.
Use as CLI tool:
# Gemini can execute commands in code execution environment
./feedback-o-tron submit --repo "..." --title "..." --body "..." --platform bugzilla --component "..." --version "..."-
Install feedback-o-tron as escript
-
Expose via function calling or tool use API
-
Configure credentials in environment
-
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"]
}
}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 compilebeforemix 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
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
Bugzilla: There is no component named 'X' in the 'Y' product
-
Fix: Use correct component name with
--componentflag -
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
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 |
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.comAuto-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)
Bugzilla:
# Component and version are REQUIRED for Bugzilla
./feedback-o-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"
cd elixir-mcp
mix testTest 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
Dry-run mode (no actual submission):
./feedback-o-tron submit \
--repo "test/repo" \
--title "Test bug" \
--body "Test description" \
--platform github \
--dry-runExpected output:
β Submission ABC123 completed [DRY RUN] github: Would submit
Production bugs filed (2026-02-07):
-
Bug #2437503: maliit-keyboard crash loop
-
Platform: Fedora Bugzilla
-
Component: maliit-keyboard
-
Version: 43
-
Status: Successfully submitted with full stack trace
-
-
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
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} -> StringSafeJSON: Type-safe JSON parsing with schema validation
-- Parse JSON with compile-time schema validation
parseJSON : (schema : JSONSchema) -> String -> Either ParseError (JSONValue schema)Integration approach:
-
Use Idris2 for formal specification of API contracts
-
Generate Zig FFI bindings via C ABI
-
Call from Elixir via NIFs
-
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
| Platform | URL |
|---|---|
GitHub (primary) |
{url-github} |
GitLab |
{url-gitlab} |
Bitbucket |
{url-bitbucket} |
Codeberg |
{url-codeberg} |
Licensed under MPL-2.0 (MPL-2.0).
See LICENSE.txt for details.