formal-ai
Formal AI is a Rust implementation of a symbolic, deterministic assistant that exposes OpenAI-shaped interfaces without neural-network inference.
The current implementation covers the surface area requested in issue #1:
- library API for symbolic prompt handling
- CLI chat command
- HTTP API server with
/v1/chat/completionsand/v1/responses - Telegram bot CLI with long polling by default and an opt-in webhook server, configured through
lino-arguments - human-readable Links Notation knowledge and dataset export through
lino-objects-codec - Docker-ready microservice
- GitHub Pages markdown chat demo backed by a Rust-generated WebAssembly worker
Project direction is tracked in VISION.md, GOALS.md, and NON-GOALS.md. The issue #12 synthesis is in docs/case-studies/issue-12/README.md.
Quick Start
TELEGRAM_BOT_TOKEN=123:abc
Example API call:
Example Telegram webhook update:
Docker:
The static demo lives in src/web/index.html. Serve it from a local web server or GitHub Pages so the WebAssembly worker can be fetched by the browser. The demo starts with a user greeting, renders markdown in messages, previews markdown input, and includes a randomized dialog mode for hello-world prompts across several programming languages.
Full-memory export and import
Every interface produces the same self-contained Links Notation document by default. In the browser, the Export memory topbar button writes formal-ai-memory.lino as a complete formal_ai_bundle — the entire seed (rules, concepts, tools, multilingual responses), UI preferences, environment metadata, and the full append-only event log — so a single click is enough to reconstitute the session. Import memory auto-detects bundle vs legacy demo_memory files and surfaces migration suggestions when the imported seed version differs from the running app's. The CLI matches:
The Rust library re-exports the same helpers — export_memory_full, import_memory_full, suggest_memory_migrations, BundleInfo, ParsedBundle — so embedders writing their own surface get the same defaults. The prefilled Report issue link records the dialog as a single compact U:/A: code block and points to docs/upload-memory.md for attaching the full memory export (GitHub Gist or .zip workflow, plus redaction reminders) instead of repeating those instructions inline.
Telegram Bot
The formal-ai telegram subcommand defaults to long polling and keeps the webhook server available as an opt-in mode. The CLI is configured through lino-arguments (a clap-compatible derive), so every flag also reads from the matching environment variable and from .lenv/.env files in the working directory.
Long polling (default)
The polling client shells out to curl, calls Telegram's getUpdates, advances the offset after each batch, and replies through sendMessage with HTML formatting. The same FormalAiEngine used by the library, HTTP API, and web demo is reused, so polling answers match the other surfaces.
Webhook (opt-in)
# or equivalently for backwards compatibility:
Expose the server through HTTPS and register the endpoint with Telegram:
The webhook accepts Telegram message, edited_message, channel_post, and edited_channel_post updates. It returns a direct Telegram sendMessage response for both private chats and group/channel chat IDs, using Telegram HTML formatting so code blocks survive the chat surface. This implementation does not store a bot token or perform outbound Telegram API calls from the webhook path; large file attachments require an outbound bot-client layer.
Rust Library
use ;
let request = ChatCompletionRequest ;
let completion = create_chat_completion;
assert_eq!;
Current Symbolic Behavior
The engine normalizes a prompt, selects a deterministic symbolic rule, and returns the rule output with evidence link identifiers and indented Links Notation. Seed rules currently cover:
- greetings:
Hi,Hello,Hey - hello world requests for Rust, Python, JavaScript, TypeScript, Go, and C
- calculator-parsable math, unit, currency, percentage, and datetime prompts through
link-calculator, with the local arithmetic evaluator retained for unsupported word-operator and binary-modulo syntax - URL requests such as
fetch example.comandСделай запрос к google.com; the browser demo tries CORSfetch()first and falls back to an embedded iframe - explicit web-search prompts such as
Search the web for Nikola TeslaandНайди в интернете Никола Тесла; the browser demo uses the CORS-enabled Wikipedia search endpoint and returns ranked links - unknown prompts, which return an explicit learnable-rule fallback
Hello-world answers include execution metadata. Rust, Python, JavaScript, Go, and C examples are compiled or syntax-checked and run by the issue-8 local verification harness with captured output. TypeScript is returned with an explicit warning because tsc is not configured in the current repository runtime.
No GPU, neural network, remote model, or random sampling is used.
Dataset Seeds
Issue #1 source indexes and seed prompts are stored as indented Links Notation in data/.
The generator writes source, greeting, hello-world, and demo-dialog records. .lino files are kept below 1500 lines and validated by the unit tests.
Hive Mind Dataset Mining
Issue #115 adds an operator script for mining GitHub evidence from
link-assistant/hive-mind pull requests, issues, reviews, diffs, and Actions
logs into a case-study dataset. Keep this outside the seed tool registry; it is
a repository maintenance command, not an in-agent reasoning tool.
The script wraps formal-ai github-logs plan|collect with the focused Hive
Mind defaults used by docs/case-studies/issue-115/.
Development
See REQUIREMENTS.md for the cumulative requirement matrix (now alongside VISION.md) and docs/case-studies/issue-1/README.md for the collected research and implementation plan.