Metadata-Version: 2.4
Name: monogate-forge
Version: 0.18.0
Summary: EML language and compiler for verified mathematical computation across 36 targets: software, GPU shaders, hardware (FPGA/ASIC, SPICE, KiCad, and JLCPCB), formal verification, and safety-critical systems.
Author: Mosa Creates LLC
Author-email: "Arturo R. Almaguer" <contact@monogate.dev>
Maintainer-email: "Arturo R. Almaguer" <contact@monogate.dev>
License: MIT
Project-URL: Homepage, https://monogateforge.com
Project-URL: Documentation, https://monogate.dev/learn/eml/intro
Project-URL: VS Code Extension, https://marketplace.visualstudio.com/items?itemName=Monogate.monogate-forge-vscode
Project-URL: Research, https://monogate.org
Project-URL: MachLib, https://machlib.org
Keywords: compiler,programming-language,formal-verification,lean,fpga,hdl,verilog,vhdl,safety-critical,embedded,math,shader,hlsl,metal,wgsl,eml
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Compilers
Classifier: Topic :: Software Development :: Code Generators
Classifier: Topic :: Software Development :: Embedded Systems
Classifier: Typing :: Typed
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: eml-cost>=0.19.0
Requires-Dist: cryptography>=42
Requires-Dist: numpy>=2.0
Provides-Extra: dev
Requires-Dist: pytest>=8; extra == "dev"
Requires-Dist: pytest-cov>=5; extra == "dev"
Requires-Dist: mpmath>=1.3; extra == "dev"
Requires-Dist: pytest-xdist>=3.5; extra == "dev"
Requires-Dist: ruff>=0.5; extra == "dev"
Requires-Dist: mypy>=1.10; extra == "dev"
Requires-Dist: pyyaml>=6; extra == "dev"
Provides-Extra: lsp
Requires-Dist: pygls>=2.0; extra == "lsp"
Requires-Dist: lsprotocol>=2024.0.0b1; extra == "lsp"
Dynamic: license-file

# Monogate Forge

[![PyPI](https://img.shields.io/pypi/v/monogate-forge.svg)](https://pypi.org/project/monogate-forge/)
[![License: MIT](https://img.shields.io/badge/license-MIT-blue.svg)](LICENSE)
[![Python](https://img.shields.io/pypi/pyversions/monogate-forge.svg)](https://pypi.org/project/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](docs/verify-guide.md#what-backends-respect-contracts). 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

```bash
pip install monogate-forge
```

Create `hello.eml`:

```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:

```bash
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:

```bash
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`:

```rust
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`](docs/quickstart.md). Full tutorial: [monogate.dev/learn/eml/intro](https://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](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:

<!-- corpus-status:begin -->
Measured by the corpus gate over every tracked `.eml` file (357). **Out of scope** counts the files a target has nothing to compile in, by that target's own applicability rule (`tools/target_model/targets.py`): an HDL target needs an `@target(fpga)` function, a proof target an `@verify(lean)` block, a circuit target a `spice_*` annotation, and AUTOSAR, ROS 2, zkproof and AADL a function with a body. Each such file is one the gate recorded the target refusing for exactly that reason, checked file by file. The rest are **Applicable**: for each, the target's backend **Refused** it with a stated reason, or emitted an artifact that the target's own toolchain (compiled, linked, run or validated: see `tools/scripts/corpus_checks/`) **Accepted** or rejected (**Failed**). Failed files are listed by name in `tools/corpus_compile_baseline.json`, each target's list may only shrink, and each failing gating target carries an owner and an expiry date there.

Every row satisfies two equations, asserted when this table is rendered: **corpus = out of scope + applicable**, and **applicable = accepted + refused + failed** (+ unknown where no checker runs). The Corpus column is printed on every row so the denominator is never shown without it. Until 2026-10-04 this table counted a file with nothing to compile as a refusal; no numerator changed, only applicability is now explicit (`evidence/README.md`). **Contract-stopped is a SUBSET of accepted, not a further column** -- those files emitted and ran, so they are accepted, and every probe input then fired one of the kernel's own contract checks. Adding it to the others over-counts, and `corpus_compile.py`'s own summary uses the other convention (its `pass` column EXCLUDES them), which is how `300 + 10` came to look like a missing 44 on matlab. **What "accepted" means differs by target** and the column says so -- on the shader targets it means the toolchain compiled and LINKED the artifact, never that it ran or that a value matched. The value axis is the differential, which covers 16 targets and none of the shaders.

| Target | Checked | Corpus | Out of scope | Applicable | Accepted | Refused | Failed | Contract-stopped | Accepted means | Not measured |
|---|---|---|---|---|---|---|---|---|---|---|
| c | every push | 357 | 0 | 357 | 357 of 357 | 0 | 0 | 0 | compiled, linked and RUN | — |
| cpp | nightly | 357 | 0 | 357 | 352 of 357 | 5 | 0 | 0 | compiled, linked and RUN | execution |
| rust | every push | 357 | 0 | 357 | 352 of 357 | 5 | 0 | 0 | compiled and RUN | execution |
| python | nightly | 357 | 0 | 357 | 352 of 357 | 5 | 0 | 43 | imported and RUN | — |
| go | nightly | 357 | 0 | 357 | 352 of 357 | 5 | 0 | 0 | built and RUN | execution |
| java | nightly | 357 | 0 | 357 | 352 of 357 | 5 | 0 | 0 | compiled and RUN | execution |
| kotlin | nightly | 357 | 0 | 357 | 352 of 357 | 5 | 0 | 0 | compiled and RUN | execution |
| csharp | nightly | 357 | 0 | 357 | 352 of 357 | 5 | 0 | 0 | built and RUN | execution |
| javascript | nightly | 357 | 0 | 357 | 347 of 357 | 10 | 0 | 43 | imported and RUN | — |
| wasm | nightly | 357 | 0 | 357 | 347 of 357 | 10 | 0 | 0 | built from the IR and RUN | execution |
| matlab | nightly | 357 | 0 | 357 | 335 of 357 | 22 | 0 | 42 | RUN under octave | — |
| lean | nightly | 357 | 75 | 282 | 279 of 282 | 0 | 3 (owner agent-maestro, expires 2026-10-16) | 0 | compiled by lake (a sorry theorem still compiles; discharge is a separate census) | proofs: a sorry theorem compiles (tools/scripts/lean_discharge_census.py counts discharge) |
| zkproof | nightly | 357 | 2 | 355 | 34 of 355 | 321 | 0 | 0 | a circuit was built | — |
| verilog | every push | 357 | 143 | 214 | 119 of 214 | 95 | 0 | 0 | linted by Verilator (synthesis is separate and not gated) | synthesis is not gated (yosys synthesized every linted design on 2026-09-16, about an hour); simulation against C only for the demo kernels |
| systemverilog | nightly, advisory (not gating) | 357 | 143 | 214 | 44 of 214 | 107 | 63 | 0 | linted by Verilator | synthesis and simulation (Verilator lint only) |
| vhdl | nightly | 357 | 143 | 214 | 113 of 214 | 101 | 0 | 0 | analysed and elaborated by GHDL | synthesis and simulation (GHDL analysis and elaboration only) |
| chisel | nightly, advisory (not gating) | 357 | 143 | 214 | 17 of 214 | 77 | 120 | 0 | compiled and elaborated to CHIRRTL | synthesis (compiled and elaborated to CHIRRTL only) |
| llvm | nightly | 357 | 0 | 357 | 347 of 357 | 10 | 0 | 0 | assembled by llc and RUN | execution |
| hlsl | nightly | 357 | 0 | 357 | 331 of 357 | 26 | 0 | 0 | compiled AND LINKED by glslang, not DXC -- never run, no value compared | not run on a GPU (glslang, not DXC) |
| glsl | nightly | 357 | 0 | 357 | 331 of 357 | 26 | 0 | 0 | compiled AND LINKED by glslang -- never run, no value compared | not run on a GPU |
| glsles | nightly | 357 | 0 | 357 | 331 of 357 | 26 | 0 | 0 | compiled AND LINKED by glslang -- never run, no value compared | not run on a GPU |
| wgsl | nightly | 357 | 0 | 357 | 337 of 357 | 20 | 0 | 0 | validated by naga -- never run, no value compared | not run on a GPU |
| metal | not covered: Apple's Metal shader compiler (`xcrun metal`) ships only for macOS and Windows; no Linux build exists, none is on this box, and compiling MSL as C++ would not apply Metal's rules | 357 | 0 | 357 | unknown | — | — | — | — | everything |
| swift | nightly | 357 | 0 | 357 | 352 of 357 | 5 | 0 | 0 | compiled and RUN | execution |
| ada | nightly | 357 | 0 | 357 | 346 of 357 | 11 | 0 | 0 | compiled by GNAT and RUN | execution |
| autosar | nightly | 357 | 2 | 355 | 351 of 355 | 4 | 0 | 0 | compiled and linked | AUTOSAR XSD conformance and an RTE generator run |
| aadl | not covered: no AADL front end is installed: osate, ocarina and aadl-inspector are all absent from PATH (measured 2026-09-16), and the target's output is AADL text that only such a tool can name-resolve and legality-check. OSATE is an Eclipse RCP download and Ocarina builds from source with GNAT; neither is here. | 357 | 2 | 355 | unknown | — | — | — | — | everything |
| ros2 | nightly | 357 | 2 | 355 | 346 of 355 | 9 | 0 | 0 | compiled and linked | real rclcpp (compiled against a stub of the API it uses) |
| coq | nightly | 357 | 75 | 282 | 282 of 282 | 0 | 0 | 0 | checked by coqc (an Admitted obligation still compiles) | proofs: an Admitted theorem compiles |
| isabelle | nightly | 357 | 75 | 282 | 281 of 282 | 0 | 1 (owner agent-maestro, expires 2026-10-24) | 0 | checked by Isabelle (it REFUSES sorry unless quick_and_dirty) | proofs: a sorry theorem compiles |
| solidity | nightly | 357 | 0 | 357 | 347 of 357 | 10 | 0 | 0 | compiled by solc (never executed) | execution on an EVM (compiled only) |
| luau | nightly | 357 | 0 | 357 | 347 of 357 | 10 | 0 | 43 | RUN | — |
| gdscript | nightly | 357 | 0 | 357 | 345 of 357 | 12 | 0 | 0 | RUN under Godot | execution (Godot --check-only) |
| spice | nightly | 357 | 350 | 7 | 7 of 7 | 0 | 0 | 0 | parsed by ngspice | the circuit's behaviour against the kernel |
| kicad | not covered: kicad-cli here is 7.0.11 and the backend emits KiCad 8 (version 20231120): measured 2026-09-16, `kicad-cli sch export netlist` refuses all 7 emitted corpus schematics unmodified with `Failed to load schematic file` (rc 3). A dialect shim (software/backends/tests/test_kicad_schematic_actually_loads.py) loads 6 of 7, but that checks a transformation, not the artifact; examples/maglev/driver.eml fails even shimmed, cause undetermined without KiCad 8. | 357 | 350 | 7 | unknown | — | — | — | — | everything |
| jlcpcb | nightly | 357 | 350 | 7 | 7 of 7 | 0 | 0 | 0 | mapped | manufacturability at the fab |

**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.
<!-- corpus-status:end -->

### 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:

<!-- differential-status:begin -->
Measured by the differential gate (`tools/scripts/differential.py`) over every tracked `.eml` file (357): **1068 of 1145** 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**: 49337 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.

| Target | Agree | Signed zero | Ulp | Wrong | Contract differs | Contract unchecked | Target error | Refused | Burn-down |
|---|---|---|---|---|---|---|---|---|---|
| ada | 1052 of 1064 | 0 | 10 | 0 | 2 | 0 | 0 | 4 | owner agent-maestro, expires 2026-10-17 |
| c | 1068 of 1068 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | — |
| cpp | 1058 of 1068 | 0 | 9 | 0 | 1 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| csharp | 1049 of 1068 | 0 | 18 | 0 | 1 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| gdscript | 1025 of 1062 | 0 | 32 | 5 | 3 | 0 | 0 | 6 | owner agent-maestro, expires 2026-10-17 |
| go | 811 of 1068 | 0 | 250 | 42 | 6 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| java | 867 of 1068 | 0 | 191 | 12 | 4 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| javascript | 886 of 1068 | 0 | 173 | 9 | 4 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| kotlin | 865 of 1068 | 0 | 193 | 14 | 5 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| llvm | 344 of 1068 | 0 | 0 | 0 | 0 | **724** (disclosed) | 0 | 0 | — |
| luau | 1044 of 1066 | 0 | 21 | 0 | 1 | 0 | 0 | 2 | owner agent-maestro, expires 2026-10-17 |
| matlab | 1056 of 1066 | 0 | 9 | 0 | 1 | 0 | 0 | 2 | owner agent-maestro, expires 2026-10-17 |
| python | 1050 of 1068 | 0 | 18 | 0 | 0 | 0 | 0 | 0 | — |
| rust | 916 of 1068 | 0 | 144 | 7 | 3 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| swift | 1058 of 1068 | 0 | 9 | 0 | 1 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| wasm | 344 of 1068 | 0 | 0 | 0 | 0 | **724** (disclosed) | 0 | 0 | — |

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.** 77 of 1145 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.
<!-- differential-status:end -->

### Software (general-purpose)
| Target | Flag | Requires |
|---|---|---|
| C99 | `--target c` | — |
| C++17 | `--target cpp` | — |
| Rust | `--target rust` | — |
| Python 3 | `--target python` | — |
| Go | `--target go` | — |
| Java | `--target java` | — |
| Kotlin | `--target kotlin` | — |
| C# | `--target csharp` | — |
| JavaScript | `--target javascript` | — |
| MATLAB | `--target matlab` | — |
| Swift | `--target swift` | — |

### Compiler IRs
| Target | Flag | Requires |
|---|---|---|
| WebAssembly | `--target wasm` | — |
| LLVM IR | `--target llvm` | — |

### GPU shaders
| Target | Flag | Requires |
|---|---|---|
| HLSL (DirectX) | `--target hlsl` | — |
| GLSL (desktop) | `--target glsl` | — |
| GLSL ES | `--target glsles` | — |
| WGSL (WebGPU) | `--target wgsl` | — |
| Metal (Apple) | `--target metal` | — |

### Hardware (FPGA / ASIC)
| Target | Flag | Requires |
|---|---|---|
| Verilog | `--target verilog` | `@target(fpga)` fn |
| SystemVerilog | `--target systemverilog` | `@target(fpga)` fn |
| VHDL | `--target vhdl` | `@target(fpga)` fn |
| Chisel / FIRRTL | `--target chisel` | `@target(fpga)` fn |

### Manufacturing / circuits
| Target | Flag | Requires |
|---|---|---|
| spice | `--target spice` | `@spice_*` components |
| kicad | `--target kicad` | `@spice_*` components |
| jlcpcb | `--target jlcpcb` | `@spice_*` components |

### Formal verification
| Target | Flag | Requires |
|---|---|---|
| Lean 4 | `--target lean` | `@verify(lean)` block |
| Coq | `--target coq` | `@verify(lean)` block |
| Isabelle/HOL | `--target isabelle` | `@verify(lean)` block |

### Safety-critical
| Target | Flag | Requires |
|---|---|---|
| Ada/SPARK | `--target ada` | — |
| AUTOSAR C | `--target autosar` | — |
| AADL | `--target aadl` | — |
| ROS 2 / C++ | `--target ros2` | — |

### Gaming
| Target | Flag | Requires |
|---|---|---|
| Luau (Roblox) | `--target luau` | — |
| GDScript (Godot) | `--target gdscript` | — |

### Blockchain
| Target | Flag | Requires |
|---|---|---|
| Solidity (PRBMath SD59x18) | `--target solidity` | — |

### Zero-knowledge
| Target | Flag | Requires |
|---|---|---|
| Plonky2 ZK circuits (research) | `--target zkproof` | — |

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**](https://marketplace.visualstudio.com/items?itemName=Monogate.monogate-forge-vscode)

```
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](https://marketplace.visualstudio.com/items?itemName=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](docs/quickstart.md) — pip install to first compile in 5 minutes.
- [Language reference](docs/language-reference.md) — every keyword, builtin, type, and annotation.
- [Backends](docs/backends.md) — every compilation target with its CLI flag, file extension, and what it needs in your source.
- [Verify guide](docs/verify-guide.md) — `@verify`, `requires`/`ensures`, Lean output, MachLib integration.
- [FPGA guide](docs/fpga-guide.md) — `@target(fpga)`, LUT/DSP estimates, precision selection, vendor support.

External:

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

---

## Contributing

See [`CONTRIBUTING.md`](CONTRIBUTING.md). Bug reports and feature requests via GitHub issues.

## License

Compiler is MIT (see [`LICENSE`](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](https://monogateforge.com).
