The safest language you've never tried — and it can prove your code is correct.
Ada didn't lose on merit. It lost on vibes and friction: a "defense-only" reputation, a painful first hour, no modern package manager (until Alire), and — the quiet modern killer — AI assistants that can't write it because there's so little Ada on GitHub to train on.
Meanwhile Ada has quietly had, for 40 years, the thing everyone suddenly wants: memory safety, range/contract checking, and — via SPARK — the ability to mathematically prove your code has no runtime errors. The US government (CISA/NSA/ONCD) lists Ada/SPARK as a recommended memory-safe language right next to Rust. Almost nobody knows.
This repo is an attempt to fix the friction, ride the memory-safety wave, and make Ada delightful again.
- Make the first 90 seconds delightful. Zero install, in the browser, on a phone. Show — not tell — the one thing Ada does that no mainstream language does: prove your code can't fail at runtime. → Why Ada is different
- Fix the AI gap. Give AI assistants the ability to write, run, and prove real Ada, so
picking Ada in 2026 doesn't mean coding without a copilot. →
packages/mcp-kit - Build a reason to come back. Advent of Ada — challenges that reward proven solutions, not just correct ones.
- Be genuinely contributable. Mock-first design means anyone can hack on any layer without
installing a toolchain. →
CONTRIBUTING.md·docs/roadmap.md
This is a community passion project. If you've never written a line of Ada, you're exactly who it's for — and your confusion is the most valuable bug report we can get.
Two products that reinforce each other, plus shared plumbing:
| Package | What it is | Status |
|---|---|---|
packages/playground-frontend |
Proving Ground — an in-browser Ada editor. Write code, run it, and watch SPARK prove it's bug-free. | Skeleton |
packages/playground-backend |
HTTP API that compiles, runs, and proves Ada snippets in a sandbox. | Skeleton |
packages/ada-runner |
Shared library that actually invokes the Ada toolchain (Alire / GNAT / GNATprove). Used by both the backend and the MCP kit. | Skeleton |
packages/mcp-kit |
ada-mcp — a Model Context Protocol server that gives Claude/Copilot the ability to compile, run, prove, and look up Ada. Fixes the "AI can't help me write Ada" problem. | Skeleton |
examples/ |
The emotional-payoff snippets: the same off-by-one bug that crashes in C, won't compile in Rust, and is proven impossible in SPARK. | Ready |
Plus Advent of Ada (docs) — a challenge engine baked into the playground whose leaderboard rewards proven solutions, not just correct ones. The retention loop.
Verified in mock mode: the backend API, the MCP server (4 tools over stdio), the playground UI (run + prove + the 🥇 PROVEN challenge flow), and the shared runner all run end-to-end today with no Ada toolchain installed.
The strategy: the playground is the front door (attention), the MCP kit is the retention layer (people stick when their AI assistant can help them). See
docs/roadmap.md.
The skeleton ships with a mock runner so you can develop the whole stack without installing GNAT. Everything compiles, runs, and returns believable canned results.
# 1. Install deps for all workspaces
npm install
# 2. Start the playground backend (mock mode is the default)
npm run dev:backend # -> http://localhost:8080
# 3. In another terminal, start the frontend
npm run dev:frontend # -> http://localhost:5173
# 4. (optional) run the MCP server over stdio
npm run dev:mcpOpen http://localhost:5173, hit Run and Prove, and you'll see the mock pipeline
end-to-end. To wire the real toolchain, see Real mode
below and docker/ada-toolchain.Dockerfile.
Set ADA_RUNNER_MODE=docker and build the toolchain image:
docker build -t ada-toolchain -f docker/ada-toolchain.Dockerfile .
ADA_RUNNER_MODE=docker npm run dev:backendThe runner then shells into a sandboxed container to run gnatmake, execute the binary,
and run gnatprove. See packages/ada-runner/README.md
for the exact contract and the security model.
ada-revival/
├── README.md ← you are here
├── ARCHITECTURE.md ← how the pieces fit together
├── CONTRIBUTING.md ← how to help
├── docs/
│ ├── getting-started.md
│ ├── why-ada.md ← how Ada differs from a "regular" language
│ ├── architecture.md ← deep dive (mirrors ARCHITECTURE.md)
│ ├── advent-of-ada.md ← the challenge/retention feature
│ └── roadmap.md ← the plan, phased
├── examples/ ← Ada + SPARK "prove-it" snippets
├── docker/
│ └── ada-toolchain.Dockerfile
└── packages/
├── ada-runner/ ← shared toolchain wrapper (mock | docker | local)
├── playground-backend/ ← compile / run / prove HTTP API
├── playground-frontend/ ← the in-browser editor (Proving Ground)
└── mcp-kit/ ← ada-mcp: Ada superpowers for AI assistants
- Rides an existing wave. We don't beg for attention for a 1983 language; we attach to the hottest topic in systems programming (memory safety) with a claim nobody else can make ("we can prove it").
- Zero-install front door. The playground works in a browser, on a phone. The moment a language says "install GNAT first," 80% of curious people leave.
- Fixes the AI barrier. In 2026, people won't start a language their assistant can't help with. The MCP kit closes that gap directly.
MIT — see LICENSE. Contributions welcome; see
CONTRIBUTING.md.