formal-ai 0.23.0

Formal symbolic AI proof of concept with OpenAI-compatible APIs
Documentation

formal-ai

Formal AI is a Rust proof of concept for a symbolic, deterministic assistant that exposes OpenAI-shaped interfaces without neural-network inference.

The current prototype is intentionally small. It proves the surface area requested in issue #1:

  • library API for symbolic prompt handling
  • CLI chat command
  • HTTP API server with /v1/chat/completions and /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

cargo run -- chat --prompt "Hi"
cargo run -- chat --prompt "Write me hello world program in Rust" --format chat
cargo run -- dataset
cargo run -- serve --host 127.0.0.1 --port 8080
TELEGRAM_BOT_TOKEN=123:abc cargo run -- telegram                       # long polling (default)
cargo run -- telegram --mode webhook --host 127.0.0.1 --port 8080      # webhook server (opt-in)
rust-script scripts/download-datasets.rs
experiments/verify-hello-world-examples.sh

Example API call:

curl -s http://127.0.0.1:8080/v1/chat/completions \
  -H 'content-type: application/json' \
  -d '{"model":"formal-symbolic-poc","messages":[{"role":"user","content":"Hi"}]}'

Example Telegram webhook update:

curl -s http://127.0.0.1:8080/telegram/webhook \
  -H 'content-type: application/json' \
  -d '{"update_id":1,"message":{"message_id":7,"date":1,"chat":{"id":42,"type":"private"},"text":"Write me hello world program in Rust"}}'

Docker:

docker build -t formal-ai .
docker run --rm -p 8080:8080 formal-ai

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:

cargo run -- memory export --from memory.lino --path full.lino           # default: full bundle
cargo run -- memory export --from memory.lino --path events.lino --events-only  # legacy demo_memory
cargo run -- memory import --path full.lino --into memory.lino           # accepts either format
cargo run -- bundle export --path bundle.lino --memory memory.lino
cargo run -- bundle import --path bundle.lino --into memory.lino

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 tells users to wrap the export in a .zip (GitHub does not yet accept .lino attachments) and to redact sensitive content before attaching.

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)

export TELEGRAM_BOT_TOKEN=123:abc
cargo run -- telegram                                                   # polling by default
cargo run -- telegram --mode polling \
  --timeout 30 --limit 100 \
  --allowed-updates message,edited_message

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)

cargo run -- telegram --mode webhook --host 127.0.0.1 --port 8080
# or equivalently for backwards compatibility:
cargo run -- serve --host 127.0.0.1 --port 8080

Expose the server through HTTPS and register the endpoint with Telegram:

curl -s "https://api.telegram.org/bot${TELEGRAM_BOT_TOKEN}/setWebhook" \
  -d "url=https://example.com/telegram/webhook"

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 prototype 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 formal_ai::{create_chat_completion, ChatCompletionRequest, ChatMessage, MessageContent};

let request = ChatCompletionRequest {
    model: None,
    messages: vec![ChatMessage {
        role: String::from("user"),
        content: MessageContent::Text(String::from("Hi")),
    }],
    stream: false,
};

let completion = create_chat_completion(&request);
assert_eq!(
    completion.choices[0].message.content.plain_text(),
    "Hi, how may I help you?"
);

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
  • 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/.

rust-script scripts/download-datasets.rs
rust-script scripts/check-file-size.rs

The generator writes source, greeting, hello-world, and demo-dialog records. .lino files are kept below 1500 lines and validated by the unit tests.

Development

cargo fmt --all -- --check
cargo clippy --all-targets --all-features
cargo test --all-features --verbose
cargo test --doc --verbose
rust-script scripts/check-file-size.rs

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.