94.8%
of AI-to-Rust failures are compile errors—mostly unresolved imports and dependencies
AI-native systems programming
AI writes code faster than you can review it. We are building a language and tools to fix that.
FORMA is a systems language designed for AI code generation. Memory-safe without lifetime annotations. Grammar-constrained to prevent invalid syntax. And the first language with built-in tools to explain and verify what AI-generated code actually does—so you can trust it without reading every line.
This began as a simple experiment into the competency of Claude Code. As coding quickly shifts to generative AI, there are simple trust and quality concerns that we can engineer out. This project is a discussion starter about how to adapt to this future.
A Parallel Worth Watching
AI acceleration took a major step when the stack evolved from general-purpose compute to custom hardware and silicon. FORMA is starting the conversation that a language-layer equivalent may be necessary for generative coding: purpose-built syntax, constraints, and verification for AI-authored software.
~35%
fewer tokens than equivalent Rust—lower inference costs at scale
316+
built-in functions—no external dependencies for common tasks
51
development sprints of research-driven iteration
The Trust Problem
You're generating thousands of lines of code you can't fully review
AI coding assistants are transforming development. But they create a new problem: code you didn't write that you're responsible for.
The Volume Problem
AI generates code faster than humans can review. A single prompt can produce hundreds of lines. Multiply that across a team, and you have a codebase growing faster than anyone can audit.
The Complexity Problem
Systems code is the hardest to verify. Memory management, concurrency, error handling—the things that cause production failures are exactly what's hardest to review at a glance.
The Liability Problem
When AI-generated code fails in production, it's your responsibility. "The AI wrote it" isn't a defense. You need a way to verify correctness before you ship.
The FORMA Approach: Trust Through Verification
Instead of asking you to review every line, FORMA gives you tools to verify what the code promises.
Contracts specify behavior. forma explain translates them to English. forma verify tests them automatically.
You review the specification, not the implementation.
The Verification Toolchain
Tools that make AI-generated code trustworthy
FORMA isn't just a language—it's a complete toolchain for generating, constraining, and verifying AI-authored code.
forma explain
Understand what code promises without reading it
Translates function contracts into plain English. See what the AI claims the code does—preconditions, postconditions, invariants—in human language.
$ forma explain sort.forma --format human
┌─ verified_sort(items: [Int]) -> [Int]
│ Requires:
│ - items is not empty
│ Guarantees:
│ - [@sorted] for every i in 0..result.len() - 1,
│ result[i] is at most result[i + 1]
│ - [@permutation] permutation(items, result)
└─JSON output available for CI integration and automated review pipelines.
forma verify --report
Prove contracts hold with generated test cases
Automatically generates inputs, runs them against contracts, and produces a trust report. PASS/WARN/SKIP/FAIL status for every function. Deterministic with seed control.
$ forma verify src/ --report --format human
FORMA Verification Report
src/sort.forma
✓ PASS verified_sort contracts:3 examples:20/20
✓ PASS binary_search contracts:2 examples:20/20
⚠ SKIP merge contracts:0
Summary
Functions: 3
Verified: 2, Skipped: 1, Failures: 0
Examples passed: 40/40Capabilities revoked by default—safe to run in CI without side effects.
Grammar Export
Constrain generation to valid syntax
Export FORMA's grammar as EBNF or JSON. Feed it to constrained decoding pipelines (llama.cpp, Outlines, etc.) to guarantee the AI only produces syntactically valid code.
$ forma grammar --format json > forma.json
# Use with constrained decoding to eliminate syntax errorsJSON Diagnostics
Machine-readable errors for self-correction loops
Compiler errors in structured JSON with location, severity, code, and suggestions. Feed them back to the AI for automatic repair without human intervention.
$ forma check --error-format json broken.forma
{"success":false,"errors":[{
"file":"broken.forma","line":5,"column":12,
"severity":"error","code":"TYPE",
"message":"type mismatch: expected Int, found Str"
}]}Contract Patterns
Express invariants concisely
35 built-in contract patterns: @sorted, @nonempty, @permutation, @bounded, @even, @subset, @prefix, @pure, and more. Plus forall, exists, and old() for custom specifications.
@nonempty(items)
@sorted(result)
@permutation(items, result)
f verified_sort(items: [Int]) -> [Int]Type Queries
Context-aware completions for AI prompts
Query types at any position. Get completions with full signatures. Provide context to AI systems for more accurate generation in complex codebases.
$ forma typeof app.forma --position 12:8
$ forma complete app.forma --position 12:8The AI-Assisted Development Workflow
1
Constrain
Export grammar, feed to AI. Generation is syntactically valid by construction.
→
2
Generate
AI writes code with contracts specifying behavior.
→
3
Explain
Review contracts in English. Understand promises without reading implementation.
→
4
Verify
Run verification report. Get PASS/FAIL for every contract.
→
5
Ship
Trust the code because you verified the specification.
The Language
Systems programming without the AI failure modes
FORMA is memory-safe, statically typed, and compiles to native code. It's designed so AI can generate it reliably.
No Lifetime Annotations
Second-class references give you memory safety without explicit lifetimes. The #1 source of AI-generated Rust failures—eliminated by design.
Token Efficient
Short keywords (f, s, e, m, wh), type shortcuts (T?, T!E), minimal punctuation. ~35% fewer tokens than Rust for equivalent programs.
Batteries Included
316+ built-in functions: HTTP, TCP/TLS, SQLite, compression, JSON, regex, async/await, higher-order collections. No package ecosystem to navigate—AI can use the stdlib directly.
Capability Security
File, network, and process access are gated by flags (--allow-read, --allow-network). Safe sandboxing for AI-generated code execution.
Quick Syntax Overview
# Functions use 'f', return type after ->
f factorial(n: Int) -> Int
if n <= 1 then 1
else n * factorial(n - 1)
# Contracts specify behavior
@pre(n >= 0, "n must be non-negative")
@post(result >= 1, "factorial is always positive")
f verified_factorial(n: Int) -> Int
if n <= 1 then 1 else n * verified_factorial(n - 1)
# Async with 'as', spawn with 'sp', await with 'aw'
as f fetch_all(urls: [Str]) -> [Str]
tasks := map(urls, |url: Str| sp http_get(url))
map(tasks, |t: Future| aw t)Interactive
Live FORMA Playground
Load working examples, inspect token metrics, and see structured diagnostics.
Estimated Tokens
0
Shorthand Hits
0
Syntax Warnings
0
Rust-Equivalent Tokens
0
Heuristic Diagnostics
Structured JSON Diagnostic
Expected Output
Load or write a program, then click "Simulate Run".
Project Status
What's Shipped, What's Next
FORMA is in active development. The core language and verification toolchain are functional. Here's where we are and where we're going.
The Path to Formal Verification
Today, FORMA verifies contracts at runtime with generated test cases. The foundation is in place for the next level: static verification that proves correctness without execution.
What's Built
- Clean MIR with CFG structure ideal for analysis
- Contract expressions with quantifiers and old()
- 35 named patterns with formal semantics
- Deterministic verification with seed control
What's Coming
- SMT solver integration (Z3) for bounded verification
- Exportable verification conditions for external provers
- Coverage-guided fuzzing with contract feedback
- Refinement types for compile-time contract checking
The Vision
A language where AI generates code with contracts, and the compiler proves those contracts hold—not by testing, but by mathematical verification. Critical systems code that's correct by construction.
Positioning
FORMA vs. Alternatives
Several languages are exploring AI-first design. Here's how FORMA compares.
| Capability | FORMA | Rust | Mojo | Python |
|---|---|---|---|---|
| Memory safe | ✓ | ✓ | ✓ | ✗ |
| No lifetime annotations | ✓ | ✗ | ✓ | N/A |
| Grammar export for constrained decoding | ✓ | ✗ | ✗ | ✗ |
| JSON diagnostics for self-correction | ✓ | Partial | ✗ | ✗ |
| Contract explanation (explain command) | ✓ | ✗ | ✗ | ✗ |
| Automated verification reports | ✓ | ✗ | ✗ | ✗ |
| Capability-based sandboxing | ✓ | ✗ | ✗ | ✗ |
| Native compilation | ✓ (LLVM) | ✓ | ✓ | ✗ |
Other AI-first languages exist. FORMA's differentiator is the complete verification toolchain: grammar export, structured diagnostics, contract explanation, and automated verification reports—all designed to work together for trustworthy AI-assisted development.
Ready to try FORMA?
Clone the repo, build with Cargo, and run your first verified program in minutes.