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.
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.
- Rust 1.85 or later (with
rustup) - Cargo (comes with Rust)
Install the latest release directly from crates.io:
cargo install maatOr build from source:
git clone https://github.com/maatlabs/maat.git
cd maat
cargo build --releaseNote (source builds): When running from a source build instead of
cargo install, substitutecargo run --release --formaatin all commands below (e.g.,cargo run --release -- run file.maat).
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 --versionCompile and execute a Maat source file in a single step:
maat run examples/fib.maatOr use the build-then-execute workflow for faster repeated execution:
maat build examples/fib.maat -o fib.mtc
maat exec fib.mtcSee examples/README.md for the full set of provable example programs and how to run, prove, and verify each one.
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.maatmain.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.maatBuild it to a single .mtc:
maat build my_project/main.maat -o my_project.mtc
maat exec my_project.mtcKey rules:
mod foo;declares a dependency onfoo.maat(orfoo/mod.maat) relative to the declaring fileuse foo::bar;oruse foo::{bar, baz};imports specific public items -- no glob imports (use foo::*) for ZK auditability- Items without
pubare 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
Start an interactive REPL session. The REPL compiles each line to bytecode and executes it on the VM:
maat replExample 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);
42Generate a STARK proof of correct program execution:
# Generate a proof (development mode, ~12 bits security)
maat prove examples/fib.maat
# Generate a proof with production security (~97 bits)
maat prove examples/fib.maat --production
# Dump execution trace alongside the default-named proof
maat prove examples/fib.maat -t trace.csvVerify a proof (the default output path is the source file with its extension swapped to .proof.bin):
maat verify examples/fib.proof.binThe 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 and private inputs bind to the fn main signature: pub parameters flow through the boundary-constrained public-memory accumulator, bare parameters bind to a prover-supplied witness cell with no public commitment. Supply them via command line or JSON file:
# Command-line inputs
maat prove program.maat --input "1,2,3" --private-input "4,5"
# JSON file inputs
echo '[1, 2, 3]' > inputs.json
echo '[4, 5]' > private.json
maat prove program.maat --inputs-file inputs.json --private-inputs-file private.jsonSee examples/README.md for the full set of provable example programs, their fn main signatures, and input values for each one.
By default maat verify <proof.bin> reads the public values (inputs, output, program hash) from inside the proof envelope and accepts whatever the prover committed to. The Fiat-Shamir transcript and the boundary-constrained public-memory accumulator make those embedded values cryptographically binding---a prover cannot lie about them---nevertheless, the verifier needs a CLI knob to pin what the proof must say. There's an outer assertion layer for exactly that purpose.
The simplest flow ships the proof and a JSON public-I/O bundle from the prover to the verifier; the verifier then asserts both are consistent with each other and with its own expectation:
# Prover side: emit the bundle alongside the proof.
maat prove examples/vdf.maat --input 3 --write-public-io vdf.pubio.json
# Verifier side: assert the proof commits to exactly these public values.
maat verify examples/vdf.proof.bin --public-io vdf.pubio.json --expect-program examples/vdf.maatThe bundle is decimal-string typed (Goldilocks Felt reaches 2^64 - 2^32 + 1, beyond what JSON numbers round-trip losslessly) and uses #[serde(deny_unknown_fields)] so schema drift surfaces at parse time:
{
"inputs": ["3"],
"output": "11509554200763765976",
"program_hash": "0x0f9692dbb14bc0020bb23b06c59595626de2d16a8d7ddb94b11ebcb2d4a70c0f"
}For finer-grained assertions, the verifier accepts --input, --expect-output, --expect-program <path.maat> (compile + hash), and --expect-program-hash <hex> (pin a known image hash without recompilation) individually. The prove side mirrors the symmetry: --expect-output runs the prover-side assertion after tracing but before the expensive proof step, and --public-io <path.json> loads inputs, private inputs, and an expected output from one bundle. --write-public-io deliberately omits private_inputs---private witnesses are uncommitted by design. The cryptographic verify runs first so a forged proof fails with the existing diagnostic; assertion mismatches are only reported on proofs that are otherwise valid, with structured error: ... lines.
The STARK proof system is functional for primitive-typed programs (i8..i64, u8..u64, usize, bool, Felt), fixed-size arrays [T; N] over primitive T, Vector<T> for primitive T (segment-backed, with builtin-allocated cells covered by the memory permutation argument), closures (segment-backed captures, tamper-detected via aux constraint 1), and user-defined functions over those types--including parameters, return values, nested calls, bounded recursion, Option<T> / Result<T, E> pattern matching, and #[bounded(N)] loops. <, >, <=, >= are proven for every integer width up through u64/i64/usize/isize. All examples/*.maat programs prove and verify end-to-end under development_options. The following remain planned for future releases:
- Segment-backed migration for remaining composites:
Map<K, V>,Set<T>,str,struct, andenumcontinue to execute via inlineValuevariants. Their inline forms prove and verify cleanly for current programs (their cells never enter the heap), but the cells are not yet covered by the AIR's memory permutation argument. Segment-backed migration is deferred until a real consumer (recursive proofs, STARK-to-SNARK wrapping, in-AIR composite-cell content) demonstrates that AIR-level cell coverage is load-bearing. - 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.
Run the full test suite:
cargo test --workspaceMaat includes a Criterion-based benchmark suite for the bytecode VM:
# Run all benchmarks
cargo bench -p maat_tests --bench benchmarks
# Run specific benchmarks (e.g. the Rescue hash-chain workload)
cargo bench -p maat_tests --bench benchmarks -- rescue
# 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 beforeHTML reports are generated at target/criterion/report/index.html.
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 listlibfuzzer 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=60fuzz_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=60fuzz_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/.
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_roundtripFormat code using nightly rustfmt:
cargo +nightly fmtRun Clippy for linting (zero warnings policy):
cargo clippy --all-features --all-targets -- -D warningsGenerate and view documentation:
cargo doc --all-features --no-deps --openMaat 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); heap accesses go through per-instance memory segments via MemorySegmentManager, and a relocation pass between trace finalization and proof generation flattens those segments into the single AIR address space, fills sparse-segment holes, and appends the public-memory accumulator's dummy rows. 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, public-memory accumulator over the multi-cell output segment, 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 | 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, …) |
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.
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.
All 18 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.
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 |
Maat is currently at version 0.18.0. The compiler frontend, type system, module system, bytecode VM, and CLI toolchain are functional and tested. The ZK backend proves and verifies a top-level fn main(<params>) -> T entry point with public (pub) parameters bound cell-by-cell into the public-memory accumulator and private (bare) parameters bound to an uncommitted prover-supplied witness, plus user-defined function calls with parameters, return values, nested calls, bounded recursion, arithmetic, bitwise operations (AND / OR / XOR / SHL / SHR over a chunked-LogUp argument), ordering comparisons across every integer width up through u64/i64/usize/isize, fixed-size arrays [T; N] (including nested [[T; N]; M]) over primitive T, segment-backed Vector<T>, segment-backed closure captures, and Rescue-Prime hashing (hash::rescue_2 / rescue_4 / rescue_8). The verifier-side public-I/O bundle (maat verify --public-io / --input / --expect-output / --expect-program{,-hash}) adds an assertion layer over the cryptographic verify. All examples/*.maat programs prove and verify end-to-end. See the current limitations for gaps deferred to future releases.
Early adopters should be aware that Maat 0.18.0 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.
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.