Maat

Turing-complete programming language for writing zero-knowledge proofs

WARNING: This is a research project. It has not been audited and may contain bugs and security flaws. This implementation is NOT ready for production use.

Overview

Proof-Driven Development (PDD) is software development methodology that emphasizes formal verification and mathematical proofs to ensure the correctness and reliability of code. It is an extension of test-driven development (TDD), but instead of relying solely on tests, it uses formal methods to prove properties of the code.

Source files written in Maat use the .maat extension. Compiled bytecode files use the .mtc extension.

Getting Started

Prerequisites

• Rust 1.85 or later (with rustup)
• Cargo (comes with Rust)

Installation

Install the latest release directly from crates.io:

cargo install maat

Or build from source:

git clone https://github.com/maatlabs/maat.git
cd maat
cargo build --release

Note (source builds): When running from a source build instead of cargo install, substitute cargo run --release -- for maat in all commands below (e.g., cargo run --release -- run file.maat).

The maat Binary

Maat provides a single binary with seven subcommands:

Subcommand	Description
maat run <file.maat>	Compile and execute a .maat source file
maat build <file.maat> -o <output.mtc>	Compile a .maat file to .mtc bytecode
maat exec <file.mtc>	Execute a pre-compiled .mtc bytecode file
maat repl	Start an interactive REPL session
maat trace <file.maat> -o <output.csv>	Generate an execution trace (CSV) for ZK proof inspection
maat prove <file.maat> [options]	Generate a STARK proof of correct program execution
maat verify <proof.bin>	Verify a STARK proof file

To see version information:

maat --version

Running Source Files

Compile and execute a Maat source file in a single step:

maat run examples/hello_world.maat

Or use the build-then-execute workflow for faster repeated execution:

maat build examples/hello_world.maat -o hello_world.mtc
maat exec hello_world.mtc

Multi-Module Projects

Maat supports multi-file programs with mod, use, and pub. Imports are resolved relative to the entry file, and the compiler builds a dependency graph, type-checks each module, and produces a single linked bytecode output.

Given a project layout:

my_project/
  main.maat
  geometry.maat
  math.maat

main.maat:

mod geometry;
mod math;

use geometry::Point;
use math::add;

let p = Point { x: 3, y: 4 };
print(add(p.x, p.y));
print(p.sum());

geometry.maat:

pub struct Point {
    pub x: i64,
    pub y: i64,
}

impl Point {
    pub fn sum(self) -> i64 { self.x + self.y }
}

math.maat:

pub fn add(a: i64, b: i64) -> i64 { a + b }

fn internal_helper() -> i64 { 0 }

Run it:

maat run my_project/main.maat

Build it to a single .mtc:

maat build my_project/main.maat -o my_project.mtc
maat exec my_project.mtc

Key rules:

• mod foo; declares a dependency on foo.maat (or foo/mod.maat) relative to the declaring file
• use foo::bar; or use foo::{bar, baz}; imports specific public items -- no glob imports (use foo::*) for ZK auditability
• Items without pub are module-private and inaccessible to importers
• Circular module dependencies are detected and rejected at compile time
• pub use foo::bar; re-exports items through intermediate modules

A working multi-module example is included at examples/modules/.

Running the REPL

Start an interactive REPL session. The REPL compiles each line to bytecode and executes it on the VM:

maat repl

Example session:

>> 5 + 10;
15

>> let add = fn(x, y) { x + y };
>> add(2, 3);
5

>> let new_adder = fn(x) { fn(y) { x + y } };
>> let add_five = new_adder(5);
>> add_five(10);
15

>> let fibonacci = fn(x) {
..     if x == 0 {
..         0
..     } else if x == 1 {
..         return 1;
..     } else {
..         fibonacci(x - 1) + fibonacci(x - 2)
..     }
.. };
>> fibonacci(15);
610

>> let map = fn(arr, f) {
..     let iter = fn(arr, acc) {
..         if arr.len() == 0 {
..             acc
..         } else {
..             iter(arr.split_first(), acc.push(f(arr.first().unwrap())))
..         }
..     };
..     iter(arr, [])
.. };
>> map([1, 2, 3, 4], fn(x) { x * x });
[1, 4, 9, 16]

>> let unless = macro(cond, cons, alt) {
..     quote(
..         if !(unquote(cond)) {
..             unquote(cons);
..         } else {
..             unquote(alt);
..         }
..     )
.. };
>> unless(10 > 5, "not greater", "greater");
greater

>> let double = macro(x) { quote(unquote(x) * 2) };
>> double(21);
42

Zero-Knowledge Proofs

Generate a STARK proof of correct program execution:

# Generate a proof (development mode, ~12 bits security)
maat prove examples/felt_arithmetic.maat

# Generate a proof with production security (~97 bits)
maat prove examples/felt_arithmetic.maat --production

# Specify output path and dump execution trace
maat prove examples/felt_arithmetic.maat -o felt_arithmetic.proof.bin -t trace.csv

Verify a proof:

maat verify examples/felt_arithmetic.proof.bin

The proof file embeds all public inputs (program hash, input values, output), so verification requires only the proof file itself.

Note: println! is for debugging only and does not affect the proof. The provable output is the program's return value.

Public inputs can be provided via command line or JSON file:

# Command-line inputs
maat prove program.maat --input "1,2,3"

# JSON file inputs
echo '[1, 2, 3]' > inputs.json
maat prove program.maat --inputs-file inputs.json

Current Limitations

The STARK proof system is functional for primitive-typed programs (i8..i64, u8..u64, usize, bool, Felt) and user-defined functions over those types, including parameters, return values, nested calls, and bounded recursion. The following remain planned for future releases:

• Composite-type tracing: Programs that use Vector<T>, Map<K, V>, Set<T>, str, struct, enum (including Option<T>, Result<T, E>), fixed-size arrays [T; N], or closures execute correctly under maat run but cannot yet be proven end-to-end. maat prove will emit a proof, but the verifier will reject it because the trace VM does not yet record every composite-type operation as constraint-satisfying rows.
• Ordering for u64/i64 and signed types: <, >, <=, >= are proven for u8/u16/u32/usize/char in v0.13.x; full-width 64-bit and signed ordering require a tighter range primitive and are deferred.
• STARK-to-SNARK wrapping: STARK proofs ship today; succinct on-chain verification via Groth16 over BN254 is planned.

Note that I/O side effects (println!) are not captured in the proof--the proof attests to correct computation of the return value.

Running Tests

Run the full test suite:

cargo test --workspace

Running Benchmarks

Maat includes a Criterion-based benchmark suite for the bytecode VM:

# Run all benchmarks
cargo bench -p maat_tests --bench benchmarks

# Run specific benchmarks
cargo bench -p maat_tests --bench benchmarks -- hello_world

# Save a baseline and compare after changes
cargo bench -p maat_tests --bench benchmarks -- --save-baseline before
# ... make changes ...
cargo bench -p maat_tests --bench benchmarks -- --baseline before

HTML reports are generated at target/criterion/report/index.html.

Fuzz Testing

Maat includes cargo-fuzz targets covering both the compiler pipeline and the proof system. Fuzz testing requires the nightly Rust toolchain.

# Install cargo-fuzz (one-time)
cargo install cargo-fuzz

# List available fuzz targets
cargo +nightly fuzz list

Compiler pipeline targets

libfuzzer starts from a single null byte and builds coverage-guided from there. Text and binary parsers are naturally explorable from minimal input, so no pre-generated seeds are required.

cargo +nightly fuzz run fuzz_lexer        -- -max_total_time=60
cargo +nightly fuzz run fuzz_parser       -- -max_total_time=60
cargo +nightly fuzz run fuzz_typechecker  -- -max_total_time=60
cargo +nightly fuzz run fuzz_compiler     -- -max_total_time=60
cargo +nightly fuzz run fuzz_deserializer -- -max_total_time=60

Proof-system targets

fuzz_trace_recorder and fuzz_air_constraints ship with small authored seed files found in fuzz/corpus/. fuzz_proof_deserializer and fuzz_verifier additionally need real STARK proof bytes, so run corpus_gen once after a fresh clone (or after any proof-system change) to populate those corpora:

# Required after a fresh clone, or after any proof-system change.
cargo run --release -p maat_tests --bin corpus_gen

# Run proof-system fuzz targets
cargo +nightly fuzz run fuzz_proof_deserializer -- -max_total_time=60
cargo +nightly fuzz run fuzz_verifier           -- -max_total_time=60
cargo +nightly fuzz run fuzz_trace_recorder     -- -max_total_time=60
cargo +nightly fuzz run fuzz_air_constraints    -- -max_total_time=60

fuzz_proof_deserializer and fuzz_verifier verify that malformed byte streams are always rejected with a structured error and never cause a panic. fuzz_trace_recorder verifies that arbitrarily mutated source text never panics the compiler or prover pipeline. fuzz_air_constraints verifies the soundness property: any tampered execution trace must be rejected by the verifier.

Crash artifacts (if any) are saved to fuzz/artifacts/<target>/. Seed corpora live in fuzz/corpus/.

Property-Based Testing

Maat uses proptest for property-based testing. These tests verify invariants (round-trip correctness, execution determinism, type soundness) over thousands of randomly generated programs.

# Run all property tests
cargo test -p maat_tests --test properties

# Run a specific property test
cargo test -p maat_tests --test properties -- bytecode_roundtrip

Development

Code Formatting

Format code using nightly rustfmt:

cargo +nightly fmt

Linting

Run Clippy for linting (zero warnings policy):

cargo clippy --all-features --all-targets -- -D warnings

Building Documentation

Generate and view documentation:

cargo doc --all-features --no-deps --open

Architecture

Maat uses a multi-module compilation pipeline. Source files are parsed into per-module ASTs, organized into a dependency graph by maat_module, type-checked independently with cross-module visibility enforcement, compiled to bytecode by a shared maat_codegen compiler instance (which implicitly links all modules into a single instruction stream), and executed on the stack-based maat_vm. The maat_eval crate (the tree-walking evaluator) is reduced to a macro-expansion-only engine (define_macros/expand_macros). The STARK proof system begins with maat_trace, a trace-generating VM that records every instruction step into a 56-column algebraic witness matrix over the Goldilocks field (sub-selector witnesses for 16 opcode sub-classes, comparison and division auxiliaries, and a per-row encoded operand width); maat_air encodes the CPU semantics as 81 main + 20 auxiliary Winterfell transition constraints (output correctness for arithmetic/bitwise/ordering/equality, universal PC advance, unified memory permutation, range-check sub-AIR, and builtin-segment ABI), with static pub const transition-degree arrays (no per-trace FFT detection); maat_prover wires the AIR to Winterfell to produce and verify proofs.

The type checker infers types for each module using Hindley-Milner inference (Algorithm W), with imported bindings injected from dependency modules' public exports. Type annotations are optional--the inference engine deduces types from usage--but can be provided on let bindings, function parameters, and return types for documentation or to constrain polymorphism. Generic functions with parametric polymorphism are supported (fn identity<T>(x: T) -> T { x }). Tuples, char, Map<K, V>, Set<T>, Vector<T>, and fixed-size arrays [T; N] are all first-class types with full inference support. Felt (Goldilocks field element) is a first-class numeric type for zero-knowledge arithmetic.

Custom types follow Rust syntax: struct, enum (with unit, tuple, and struct variants), trait, and impl blocks (both inherent and trait impls). Pattern matching via match supports literal, identifier, tuple-struct, wildcard, and or-patterns. Methods are statically dispatched via compile-time type-directed dispatch. Option<T> and Result<T, E> are pre-registered as language-level enums with full method suites (map, and_then, unwrap_or, unwrap_or_else, ok, err, flatten, zip, map_err, or_else, etc.) and the ? operator for ergonomic error propagation. Range syntax (0..10 and 0..=10) produces first-class Range<T>/RangeInclusive<T> values generic over all integer types and integrates with for..in loops.

Errors are reported with precise file:line:col locations using source maps and ariadne diagnostics. Compiled bytecode can be serialized to .mtc files and deserialized for later execution, enabling the build/exec workflow.

Crate Organization

Crate	Description
maat	The CLI for commands such as build, trace, repl, prove, and verify
maat_span	Source location tracking and span management
maat_errors	Unified error handling with Result type alias
maat_lexer	logos compile-time DFA tokenizer
maat_ast	Abstract Syntax Tree definitions and transformations
maat_parser	winnow combinator-based parser
maat_eval	Macro expansion engine (quote/unquote)
maat_runtime	Value system, built-in functions, and compiled types
maat_types	Hindley-Milner type inference (Algorithm W)
maat_field	Goldilocks field element (Felt) arithmetic
maat_bytecode	Instruction set encoding/decoding and serialization (50 opcodes)
maat_trace	Trace-generating VM producing a 56-column algebraic execution trace for ZK proving
maat_air	CPU constraint system (AIR): 101 polynomial constraints (81 main + 20 aux) with static declared transition degrees
maat_prover	STARK prover and verifier: generates and validates cryptographic proofs of execution
maat_codegen	AST-to-bytecode compiler with scope analysis
maat_module	Module resolution, dependency graph, and multi-module pipeline
maat_vm	Stack-based virtual machine
maat_stdlib	Embedded standard library sources (std::math, std::vec, …)

Contributing

Thank you for your interest in contributing to this project! All contributions large and small are actively accepted. To get started, please read the contribution guidelines. A good place to start would be Good First Issues.

License

Licensed under either of Apache License, Version 2.0 or MIT license at your option.

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in this codebase by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.

Security

All 17 crates enforce #![forbid(unsafe_code)]. The compiler and VM have been hardened against adversarial input with resource limits, checked arithmetic, and safe type conversions. Field element arithmetic uses the Winterfell library's constant-time implementations. See SECURITY.md for the full threat model.

Roadmap

Maat's development follows a phased milestone plan.

Milestone	Focus	Status
1	Rust-native, ZK-correct-by-design, working compiler	Complete
2	STARK-based ZK backend (proof generation and verification)	In Progress
3	Advanced type system (linear types, effect system) and self-hosting	Planned

Status

Maat is currently at version 0.13.1 (ZK proof system foundation for primitive-typed programs). The compiler frontend, type system, module system, bytecode VM, and CLI toolchain are functional and tested. The ZK backend proves and verifies user-defined function calls with parameters, return values, nested calls, bounded recursion, arithmetic, bitwise operations, and unsigned ordering comparisons. See the current limitations for gaps deferred to future releases.

Disclaimer

Early adopters should be aware that Maat 0.13.1 is a step toward Maat 1.0, for which a formal audit process is expected. In the meantime, we invite you to explore and experiment with Maat, but we do not recommend using it to build mission-critical systems.

Acknowledgments

Maat's early architecture (v0.1--v0.4) was inspired by Thorsten Ball's Writing An Interpreter In Go, The Lost Chapter: A Macro System for Monkey, and Writing A Compiler In Go. The lexer structure, Pratt parser skeleton, tree-walking evaluator, macro system, and initial bytecode VM design trace back to these books, translated from Go to Rust.

Since then, Maat has diverged substantially. The language now features Hindley-Milner type inference, Rust-native custom types (structs, enums, traits, impl blocks, pattern matching), a multi-file module system with visibility enforcement, a ZK-first design that rejects floating-point and implicit truthiness, built-in Option<T> and Result<T, E>, source-location diagnostics, bytecode serialization, and a CLI toolchain--none of which originate from the source material.

---