The first verified standard library for game development. Every shader, every texture, every physics formula — with a mathematical proof.

Plus the math, signal-processing, control, biology, ballistics, and ML kernels that built the rest of the Monogate stack. Every module compiles to GDScript, GLSL, HLSL, C, Python, and Lean (and ~30 other backends via Forge); every @verify contract has a Lean proof obligation against MachLib.

pip install eml-stdlib
eml-compile eml_stdlib/gaming/shading/pbr_specular.eml --target glsl

And get a verified PBR specular shader.

At a glance

• 185 modules across 22 categories
• 550 functions total
• 476 carry an @verify(lean, …) contract (86%)
• Every function declares its Pfaffian chain order in the type

Used by

Four Godot 4 prototypes are live consumers of the kernels here. Each one is a working application of a different stdlib slice; together they cover most of what game engines actually do at runtime.

The 10 kernels in biology/abilities/ were promoted up from apex-predator's local eml/abilities/ directory in v0.4.0. The local copies remain in that repo because scripts/build_stdlib.py reads from them as the source-of-truth; deleting them locally would break the stdlib build.

Use

After pip install, import the location of the .eml source files into your Forge project:

from eml_stdlib import path_to
math_dir = path_to('math')           # Path to math/ subdir
sigmoid  = path_to('math/sigmoid.eml')  # Specific module

Inside an EML source file, reference modules with use:

use stdlib::math::sigmoid;
use stdlib::ml::attention;
use stdlib::circuits::rc_filter;

Directory map

math/ — 20 modules / 67 fns / 63 verified

Math primitives — transcendentals, special functions, identities.

signal/ — 10 modules / 20 fns / 20 verified

DSP — filters, FFT, windows, matched-filter.

control/ — 13 modules / 41 fns / 22 verified

Control — PID, Kalman, LQR, hysteresis, deadband.

physics/ — 9 modules / 30 fns / 28 verified

Physics — wave propagation, oscillators, blackbody, fluid flow.

circuits/ — 8 modules / 37 fns / 26 verified

Analog circuits — RC, voltage divider, CMOS, MOSFET, PLL, LDO, buck.

sensors/ — 6 modules / 24 fns / 23 verified

Sensors — Hall effect, thermistor, RTD, accelerometer, strain gauge.

biology/ — 12 modules / 18 fns / 15 verified

Biology — vision, olfaction, magnetoreception, ion channels.

biology/abilities/ — 10 modules / 30 fns / 30 verified

Biology / abilities — creature combat, movement, and cover: elastic energy, locomotion, chromatophore camouflage, toxin pharmacokinetics, ballistic armor, bioelectric discharge, texture matching, sprint metabolism, muscle power, bite force.

carriers/ — 12 modules / 40 fns / 24 verified

Wave carriers — photonic, magnonic, phononic, ferronic.

quantum/ — 7 modules / 23 fns / 14 verified

Quantum gates — Hadamard, Pauli, phase, CNOT, Grover oracle.

ml/ — 9 modules / 34 fns / 32 verified

Machine learning — activations, attention, RoPE, layernorm, loss.

ballistics/ — 9 modules / 40 fns / 40 verified

Exterior ballistics — drag, gravity, wind, Coriolis, spin drift, air density, muzzle velocity, time of flight.

gaming/noise/ — 9 modules / 25 fns / 18 verified

Procedural noise — Perlin (2D/3D), Simplex, Voronoi, Worley, value noise, FBM, turbulence.

gaming/textures/ — 8 modules / 12 fns / 12 verified

Procedural textures — wood, marble, brick, checkerboard, rust, water surface, caustics, fire.

gaming/shading/ — 6 modules / 18 fns / 18 verified

Shading models — Lambertian + half-Lambert, Cook-Torrance GGX/Smith, Schlick Fresnel, toon, matcap, Burley SSS.

gaming/lighting/ — 6 modules / 12 fns / 12 verified

Lighting — point + spot + area, ambient occlusion, exponential and squared-exponential fog.

gaming/terrain/ — 5 modules / 12 fns / 12 verified

Terrain — FBM heightmaps, thermal + hydraulic erosion, biome classification, cliff detection.

gaming/animation/ — 6 modules / 14 fns / 14 verified

Animation — quadratic + cubic ease-in/out, smoothstep + smootherstep, damped springs, bounce, 2-bone IK.

gaming/particles/ — 5 modules / 11 fns / 11 verified

Particles — radial emitter, exponential drag, gravity, lifetime fade, size-over-life.

gaming/camera/ — 4 modules / 11 fns / 11 verified

Camera — perspective FOV matrix, orbit (spherical), damped-noise shake, depth-of-field circle of confusion.

gaming/audio/ — 4 modules / 10 fns / 10 verified

Audio — distance attenuation (linear/inverse/inverse-square), Doppler shift, feedback delay reverb, 1-pole low-pass.

gaming/physics/ — 7 modules / 21 fns / 21 verified

Physics — semi-implicit Euler rigid-body 2D, AABB + circle collision, restitution-aware impulse resolve, Verlet, spring-damper, Archimedes buoyancy.

Vocabulary

Chain order — the Pfaffian chain order, an upper bound on how many transcendental compositions deep a function reaches. Order 0 = pure polynomial / rational. Order 1 = single transcendental wrapping a polynomial argument (e.g. exp, sin, ln). Order 2 = two transcendentals composed (e.g. tanh = sinh/cosh). Forge uses chain order to bound termination, place transcendentals on FPGA / GPU, and select the right Lean tactic.

@verify(lean, theorem = …) — the function carries a Lean proof obligation. The Forge Lean backend emits the obligation; closing it against MachLib is what makes the function verified.

Origin: new — written for this stdlib. Otherwise the column shows the path under ~/monogate/ from which the module was copied (originals stay where they are; the stdlib is the curated home).

License

MIT — see LICENSE.