GitHub

FORMA 0.2 · Working language prototype

A programming language for code you need to trust—especially when AI writes it.

FORMA is a working discussion starter about agentic engineering: what should move into the language and compiler when agents can generate more code than people can review line by line?

The 0.2 principle

One set of semantics feeds checking, interpretation, native compilation, editor tooling, and verification. A tool never gets to invent a more convenient version of the language.

Try Forma 0.2 See the architecture View source

Prototype status: the 0.2 semantic foundation is implemented. Backend coverage and formal verification remain profile-bounded and explicitly reported.

Affine by defaultNon-Copy values move or drop exactly once.
Type-wide invariantsState validity is checked wherever owned or exclusively borrowed values become observable.
Four support profilesCore, Hosted, Native, and Experimental make boundaries visible.
One compiler sessionCLI and semantic tooling reuse the same resolved program.

Why Forma

Faster code generation needs stronger semantic feedback

More generated code is only useful if teams can understand its authority, ownership, compatibility, and evidence without reconstructing those facts by hand.

01 · Syntax

Constrain what can be generated

The compiler exports EBNF and JSON grammar from the same structured grammar model used to keep parser, formatter, keywords, and editor metadata aligned.

02 · Semantics

Reject invalid ownership early

Typed MIR records Copy and Move explicitly. Non-lexical loans, partial moves, and deterministic drop glue are checked before optimization or backend selection.

03 · Evidence

Say what verification established

TESTED is never presented as PROVED. Exhaustive finite checks, counterexamples, unknown obligations, and skipped work remain distinct in human and JSON reports.

The Agentic Engineering Proposal

Give the agent feedback. Keep authority and judgment explicit.

Forma separates three roles: the human or policy owner states intent and accepts risk, the agent generates and repairs, and the compiler enforces semantics while reporting bounded evidence.

  1. 01State intent

    A person supplies behavior, constraints, acceptable authority, and the evidence required.

  2. 02Generate

    The agent writes invariants, contracts, and code using compiler-known grammar and APIs.

  3. 03Repair

    Structured diagnostics expose syntax, type, ownership, invariant, effect, and profile failures.

  4. 04Grant authority

    Capabilities are chosen for one execution; generated code receives no ambient trust.

  5. 05Produce evidence

    Tests, exhaustive checks, proofs, counterexamples, and unknowns remain distinct.

  6. 06Review and decide

    People review intent, authority, compatibility, evidence, and the highest-risk code.

Questions, not conclusions

What should we measure?

  • Can agents specify contracts more reliably than implementations?
  • Do type-wide invariants make multi-step agent repairs safer and easier to review?
  • Do structured semantic repair loops outperform compiler prose?
  • Does affine ownership improve generation without making applications awkward?
  • Can review packets improve human accuracy and reduce review time?
  • Which results should block delivery when verification remains UNKNOWN?
Read the complete thesis

The 0.2 Foundation

One semantic spine, several trustworthy consumers

Every path starts with the same source model and passes through ownership before it reaches execution, tooling, or verification.

01Lossless sourceCST + formatter
02Resolved programnames, types, traits, effects
03Typed MIRplaces, Copy, Move, control flow
04Ownership gatesloans, initialization, drops
05Consumersinterpreter, LLVM, LSP, verifier

Ownership

Visible at function boundaries

f consume(items: Vec[Item])
f inspect(ref items: Vec[Item])
f update(ref mut items: Vec[Item])

Owned parameters move non-Copy arguments. Shared and exclusive loans are explicit; lifetime parameters are inferred.

Authority

Effects describe; capabilities grant

$ forma run app.forma --allow-read
$ forma run app.forma --allow-network
$ forma verify app.forma --level formal

File, network, process, environment, and unsafe operations are gated centrally. Formal verification reports unsupported effects as UNKNOWN.

Concurrency

Structured and ownership-aware

task = sp compute(payload)
result = aw task
# sending through a channel moves the value

Task captures move, references cannot cross task boundaries, and compiler-known Send/Sync rules protect shared state.

Packages

Deterministic local foundations

[package]
name = "demo"

[deps]
math = { path = "../math" }

forma.toml, generated lockfiles, importer-relative modules, pub visibility, and local path dependencies ship now. Registry and Git sources come later.

Verification Without Inflated Claims

Choose the level of evidence the function can support

test

Generated contract tests

Reproducible samples with bounded execution and seed control.

TESTED
exhaustive

Finite-domain enumeration

Every supported input tuple is checked up to a declared domain limit.

EXHAUSTIVE
formal · experimental

SMT-backed proof attempt

Acyclic scalar logic, tuples, named structs, projected updates, and struct invariants can be proved. Unsupported obligations stay visible.

PROVED UNKNOWN

Forma has exercised this path against real Z3: valid structural and invariant obligations prove, while invalid invariant construction produces a solver counterexample. Generated examples never produce a proof claim.

Compatibility You Can Inspect

Profiles replace vague “supported” claims

Compiler results include per-function backend support, propagated through direct calls. A Core-looking wrapper cannot hide a Hosted-only operation.

Core

Portable semantics

Affine ownership, scalar values, tuples, fixed arrays, structs, enums, calls, matches, and loops.

Hosted

Managed runtime

Dynamic collections, strings, files, databases, networking, processes, tasks, channels, and mutexes.

Native

Runtime-backed native

Currently selected strings, math, memory, and collection facilities.

Experimental

Explicitly evolving

Whole-program LLVM parity, SMT verification, and user-defined destructor bodies.

Browser Code Tour

Explore compiler-checked examples

This browser tool is a reader and lightweight heuristic inspector—not a compiler. Use the shown CLI command for authoritative diagnostics and execution.

Estimated tokens

0

Canonical shorthand

0

Heuristic notices

0

Non-empty lines

0

Local heuristic check

    Example diagnostic shape

    
          
    Expected output
    Choose an example, then show its expected output.
    
        
    
      
    
    
    

    
    
      
    
        
    
          
    Honest Project Status
    
          
    Implemented foundation, explicit boundaries
    
        
    
        
    FORMA is a serious prototype, not a production-stable ecosystem. The list below separates implemented 0.2 foundations, experimental surfaces, and deliberate next steps.
    
      
    
      
    
        
        
        
        
      
    
      
    
    
    

    
    
      
    
        
    Evaluate the Prototype
    
        
    What Forma is—and what it is not yet
    
      
    
      
    
        
    Evaluate it for
    • Research into AI-oriented language design
    • Ownership semantics without written lifetimes
    • Contract and verification UX experiments
    • Capability-aware hosted applications
    • Compiler and semantic-tooling exploration
    
        
    Do not assume yet
    • Stable 1.0 compatibility
    • Full LLVM parity across Hosted features
    • Formal proofs for arbitrary programs
    • A public package registry
    • OS isolation as the primary sandbox
    
      
    
    
    

    
    
      
    
        
    Learn, Evaluate, Contribute
    A real language project needs more than a landing page
    
        
    Start with a checked program, inspect the semantic boundaries, then challenge the proposal with experiments, counterexamples, or implementation work.
    
      
    
      
    
        
    Start
    Install and take the tour
    Build the 0.2 compiler from source, run a small program, and learn the ownership model progressively.
    Getting started →
    
        
    Build
    Use the language guide
    Syntax, ownership, effects, concurrency, contracts, profiles, packages, CLI, and compiler-checked examples.
    Language guide →
    
        
    Understand
    Inspect the architecture
    Follow the shared semantic spine from source through typed MIR, ownership gates, tools, and backends.
    Architecture →
    
        
    Integrate
    Use generated metadata
    Agents and editors can consume the grammar, keyword catalog, and builtin ownership/effect registry.
    Repository docs →
    
        
    Track
    Read status and changes
    Version history, support profiles, implementation status, and deliberate next steps are documented separately.
    Changelog →
    
        
    Challenge
    Join the discussion
    Bring soundness cases, workflow experiments, misleading evidence, capability concerns, or better language-design arguments.
    Contributing →
    
      
    
    
    

    
    
      
    Start with the evidence
    
      
    Read the profile. Run the compiler. Inspect the report.
    
      
    The fastest way to understand Forma is to try a small program and watch ownership, effects, and verification become explicit.
    
      
    
        Get started
        Read the architecture
        Open GitHub