Aufbau

Aufbau is an experimental Metamath Zero (MM0/MMB) verifier and proof compiler written in Zig. The compiler translates MM0 source and Aufbau proof scripts to MMB; the verifier checks the resulting MM0/MMB pair.

Try the web demo.

Build

Aufbau requires Zig 0.15.2.

git clone --recurse-submodules https://github.com/gleachkr/Aufbau.git
cd aufbau
zig build -Doptimize=ReleaseFast

The native binaries are written to zig-out/bin/:

• abc — proof compiler and language server
• mm0-zig — MMB verifier

Usage

Compile a proof:

abc compile INPUT.mm0 INPUT.auf OUTPUT.mmb

Verify it:

mm0-zig OUTPUT.mmb < INPUT.mm0

JavaScript packages

WebAssembly and browser packages are published on npm:

• @aufbau/compiler
• @aufbau/verifier
• @aufbau/lsp
• @aufbau/editor

Each package README contains a minimal usage example.

User Documentation

A manual with some interactive examples is available at https://grahamlk.me/Aufbau/manual

Developer Documentation

• CHANGELOG.md — release history and unreleased changes
• ARCHITECTURE.md — structure and trust boundary
• docs/proof.md — Aufbau proof-script format
• docs/rewrite_system.md — rewrite metadata
• docs/transparent_defs.md — transparent defs
• docs/view_recover.md — view and recovery metadata
• docs/fresh_binders.md — fresh binders
• docs/holes.md — proof-side holes

The canonical MM0 and MMB specifications are maintained by the Metamath Zero project.

Test

zig build test -Doptimize=ReleaseFast

Full integration coverage also requires Node, npm, mm0-rs, mm0-c, and initialized repository submodules.

Status

Aufbau is pre-1.0 software. The verifier is usable, and the compiler supports its documented proof format, but APIs and proof syntax may still change.

Licensed under the Apache License 2.0.