Monogate Forge

Forge is the EML language and compiler. Write a math kernel once, compile it to 36 backends — all of them emitting locally from the CLI, no license and no account — with chain-order analysis, and contracts (requires, ensures, refinement types) that the Lean, Coq and Isabelle targets state as theorems wherever a function declares them. Whether another target checks a contract at run time depends on the target, and several emit nothing: see the per-target table. The catalog spans software, GPU shaders, compiler IRs, FPGA RTL, manufacturing artifacts, formal-verification proofs, safety-critical avionics, gaming and EVM. The tables below list every one, and what each needs in your source to fire.

Quick start

pip install monogate-forge

Create hello.eml:

module hello;

fn pid(error: Real, integral: Real, derivative: Real) -> Real
    where chain_order <= 0
    requires (-1.0 <= error && error <= 1.0)
    ensures  (-1.5 * 1.0 <= result && result <= 1.5 * 1.0)
{
    let kp = 1.0;
    let ki = 0.2;
    let kd = 0.3;
    kp * error + ki * integral + kd * derivative
}

Compile to every target at once:

eml-compile hello.eml --target all -o build/

You now have build/hello.c, build/hello.rs, build/hello.py, build/hello.lean, build/hello.v, build/hello.hlsl, build/hello.metal, build/hello.swift, … one file per target. Pick a single target instead:

eml-compile hello.eml --target rust -o hello.rs
eml-compile hello.eml --target c    -o hello.c
eml-compile hello.eml --target lean -o Hello.lean

A snippet of hello.rs:

use monogate_sys::*;

/// pid
/// Pfaffian chain count (eml-cost pfaffian_r): 0     Cost class: p0-d2-w0-c0
/// EML depth:   2  Symbolic band: LOW (from pfaffian_r only)
/// Numerical:   cancellation exposure NONE  (no mixed-sign subtraction)
/// source obligations for pid: {O1}
///   O1 [a99a5a5c258f] -> PRESERVED (equivalent)  assert! before the tail expression
///        build: unconditional -- assert! is kept in release builds -- only debug_assert! is compiled out
/// Dynamics:    0 osc, 0 decay  (predicted_r=0)
/// FPGA est:   2 MAC, 0 exp, 0 ln, 0 trig -> 4 cy @ 32-bit
pub fn pid(error: f64, integral: f64, derivative: f64) -> f64 {
    assert!((((-1.0) <= error) && (error <= 1.0)), "pid: requires ((((-1.0) <= error) && (error <= 1.0)))");
    let kp: f64 = 1.0;
    let ki: f64 = 0.2;
    let kd: f64 = 0.3;
    let result = (((kp * error) + (ki * integral)) + (kd * derivative));
    assert!(((((-1.5) * 1.0) <= result) && (result <= (1.5 * 1.0))), "pid: ensures violated");
    result
}

Every emitted function carries its EML profile (eml-cost's pfaffian_r, cost class, EML depth, symbolic band, cancellation exposure, FPGA cycle estimate) and its obligation map in the doc-comment header, so a reviewer can see the analysis without leaving the file. The requires and ensures contracts from the EML source become runtime assert!s, which release builds keep. tests/test_doc_emission_samples.py holds this snippet to what the Rust backend prints for the hello.eml above.

Five-minute tour: docs/quickstart.md. Full tutorial: monogate.dev/learn/eml/intro.

What you get

36 targets. All local. All free. Every backend in the tables below emits from eml-compile on your machine — there is no Free/Pro split, no license token, and no hosted step in the path. What a target needs is not a tier but an annotation: the RTL family wants a @target(fpga, ...) function, the circuit family wants @spice_* components, and the proof family wants a @verify(lean, ...) block. Ask for a target the source has nothing to feed and the compiler says so instead of emitting a stub. The Requires column below records exactly that. Per-target notes — flag, file extension, what the output is for — are in docs/backends.md.

What each target's toolchain accepts

Emitting is not compiling, and compiling is not synthesizing. This table is what was measured, not what is supported:

Measured by the corpus gate over every tracked .eml file (350): each file is emitted for each target and read by that target's own toolchain (compiled, linked, run or validated: see tools/scripts/corpus_checks/). Emits is how many files the target produced an artifact for; the rest it refused with a stated reason (a missing @target(fpga), @spice_* or @verify annotation is a refusal). Accepted is how many of those the toolchain accepted; Broken were rejected. Broken files are listed by name in tools/corpus_compile_baseline.json, each target's list may only shrink, and each broken target carries an owner and an expiry date there.

Contract-stopped files emitted and ran, but every probe input fired one of the kernel's own contract checks, so the body past it never ran: not a failure, and not a full run either.

Whether every target computes the same number

Accepting an artifact is not computing the right value. Every wrong number found in the week before the differential gate existed compiled, linted or synthesized cleanly. This table is what one kernel's own functions actually returned, target against target, bit for bit:

Measured by the differential gate (tools/scripts/differential.py) over every tracked .eml file (350): 1037 of 1110 functions are in round-1 scope (Real/f64 arguments, a Real/f64 or tuple return, no state, no extern), each is called with up to 48 generated inputs -- contract boundaries and one ulp either side, IEEE specials, seeded draws -- and every result is compared with the c artifact's by bits: 47849 calls per target. Agree means identical bits on every call (a NaN is one value; both sides firing the same contract counts). Every other function is listed by name in tools/differential_baseline.json, which may only shrink.

Counts are FUNCTIONS, not calls. Signed zero, Ulp and Contract unchecked are tolerated classes, not defects: signed zero is equal except the sign of a zero; ulp is within 4 ulps, and the function reaches a libm call (glibc's exp/log/pow are not correctly rounded, and a target with its own libm is no less right); contract unchecked is the reference's contract fired and the target returned the body's value, on a target docs/verify-guide.md records as checking no contract.

Contract unchecked is why llvm and wasm agree on a minority of functions, and it is not a failure rate. docs/verify-guide.md's contract table records both targets as checking neither requires nor ensures (LLVM IR lowers a requires to an llvm.assume, a promise to the optimizer, and drops ensures; WebAssembly is built from that IR), so where the reference refuses an input they return the value the body computed. That comparison did not happen; it is disclosed, recorded and shrink-only, and no value difference hides behind it -- their Wrong and Contract differs columns are the same 0 as any agreeing target's.

Not covered. 73 of 1110 functions are outside round-1 scope and are refused with a stated reason per function in the baseline (state across calls, a Vec/Mat/Int parameter, an extern the host supplies), never counted as agreement. Refused above is a module that target's own toolchain would not emit or build at all. Every other target Forge has (lean, zkproof, verilog, systemverilog, vhdl, chisel, hlsl, glsl, glsles, wgsl, metal, autosar, aadl, ros2, coq, isabelle, solidity, spice, kicad, jlcpcb) executes nothing here: they are compared by the corpus gate's own checkers, which ask whether the toolchain ACCEPTS the artifact -- a different question, and the one the table above this answers.

Software (general-purpose)

Compiler IRs

GPU shaders

Hardware (FPGA / ASIC)

Manufacturing / circuits

Formal verification

Safety-critical

Gaming

Blockchain

Zero-knowledge

Every target above is free and emits locally. The Free/Pro split that earlier releases shipped is retired: ALL_TIERS_FREE in tools/license/verifier.py is True, so load_license reads nothing, target_allowed passes everything, and no token is checked on any path. The signing machinery stays in the tree because deleting it would be a bigger change than parking it, not because it gates anything. If a target refuses to emit, the reason is in the Requires column — a missing annotation in your source, which the error message names.

VS Code extension

Monogate Forge on the VS Code Marketplace

ext install Monogate.monogate-forge-vscode

LSP features:

• Chain-order on hover — every function shows its profiled chain order, cost class, and node count.
• Completions — keywords (fn, let, where, requires, ensures, module, use), builtins (exp, ln, sin, cos, sqrt, tanh, pow, clamp, eml, …), stdlib modules.
• Diagnostics — type errors, unbound identifiers, chain-order violations, contract failures.
• FPGA status bar — for any function annotated @target(fpga), the status bar shows estimated LUT / DSP / latency for the selected device.
• Format on save — canonical layout via eml-fmt.

Marketplace listing: Monogate.monogate-forge-vscode.

Why Forge

Industrial automation today is stuck on ladder logic — Boolean rungs from the 1960s that can't express transcendental functions, can't prove correctness, can't optimize node count, and treat PID loops as black boxes. Structured Text is marginally better but still opaque. MATLAB/Simulink + HDL Coder will get you to FPGA, but the math hides inside vendor library calls and you have no formal proof of precision.

EML makes every mathematical operation visible and measurable. Every expression is an EML tree and every function carries a chain order. A contract a function declares is stated as a Lean theorem unless translation loses it, which the obligation map reports as LOST. Whether that theorem is then proved is a separate question, answered by #print axioms. The same source compiles to your laptop, your microcontroller, your FPGA, your Solidity contract, and your formal proof. The FPGA targets compute in Q-format fixed point, so they do not agree bit for bit with the IEEE-754 software targets.

Documentation

• Quickstart — pip install to first compile in 5 minutes.
• Language reference — every keyword, builtin, type, and annotation.
• Backends — every compilation target with its CLI flag, file extension, and what it needs in your source.
• Verify guide — @verify, requires/ensures, Lean output, MachLib integration.
• FPGA guide — @target(fpga), LUT/DSP estimates, precision selection, vendor support.

External:

• monogate.dev/learn/eml/intro — guided beginner tutorial.
• monogate.dev/learn/eml/engineering — intermediate engineering course (chain orders, contracts, FPGA targeting, Lean verification).
• monogateforge.com/get-started — install the CLI.
• monogate.org — research papers and theory.
• machlib.org — formal library of mathematical kernels with Lean proofs.
• arXiv preprint — the EML cost conjecture and Pfaffian profile.

Contributing

See CONTRIBUTING.md. Bug reports and feature requests via GitHub issues.

License

Compiler is MIT (see LICENSE). Specific algorithmic methods covered by patents — open implementation, but commercial re-implementations may need a license. See patents/index.md.

Built by Mosa Creates LLC.