Repository navigation
Releases
Lume v1.1.0 — Formally Verified Systems, AI & Quantum Programming Language (Edition 2026)
Lume v1.1.0 — Edition 2026
Formally Verified Systems, Artificial Intelligence, Cyber-Physical & Quantum Programming Language
README.md · QUALIFICATION_DOSSIER.md (PASS) · Audit Report (PT-BR) · Official Wiki · Project Board (PROJECTS.md) · LumeLabs (LUMELABS.md) · Community (COMMUNITY.md) · Manual (EN) · Manual (PT-BR) · CHANGELOG.md
Executive Summary & Resumo Executivo (EN / PT-BR)
English — Institutional Overview
Lume (v1.1.0, Edition 2026) is a statically typed, formally verified systems, artificial intelligence, cyber-physical, and quantum programming language created by Ricardo Bueno (@OmegaSoftDLL). Engineered from first principles for both human systems engineers and autonomous AI agents, Lume enforces machine-checked mathematical correctness from source-level refinement contracts (requires, ensures, invariant, law, @bound, @no_alloc, @secret) all the way down to emitted native machine instructions.
Unlike conventional language toolchains that depend on external C/C++ compiler back ends, system assemblers, or unverified runtime helpers, Lume's production compiler, assembler, theorem prover, translation validator, MC/DC coverage analyzer, cryptographic stack, and developer tools are written 100% in Lume itself:
- Auditable Seed & Diverse Double-Compilation (DDC): Bootstrap originates from a minimal, frozen ~4.8k-LoC C11 interpreter and ELF64 emitter locked by
bootstrap/lume0/SEED_FREEZE.sha256. Following David A. Wheeler's Diverse Double-Compilation, building the self-hosted toolchain through independent C compilers (ccandclang) converges to the exact same bit-identical native compiler binary (0byte difference). - Zero-C Self-Hosted Steady State (
lumec == lumec2 == lumec3): Lume compiles, assembles, links, formats, tests, proves, and packages itself in~3.8 s(lumec-linux-x86_64SHA-2562a32911ee74c39b1…) with all external C compilers and system assemblers/linkers blocked (lume zero-c). - Clean-Room Mutual Assurance: No single component acts as an unexamined root of trust. Compiler proofs (
lcaas.src) are independently re-checked by a zero-compiler-import proof kernel (lcert.src); emittedx86-64,AArch64, andRISC-Vbinaries are symbolically validated against AST semantics (ltv.src,ltv_multiarch.src,ltv_rt.src);.smt2obligations are verifiedunsatby both a clean-room native solver (lsmt.src) andz3; structural Masking MC/DC is confirmed on real native binaries (lmcdc.src,0/9,618uncovered conditions); and critical control kernels run in2oo2Ddual-channel lockstep (lsafety_envelope.src) against a clean-roomRV32IMcompiler (lrv32_lowered.src) sharing0/3,169functions withlumec.
Português (PT-BR) — Resumo Executivo
A Lume (v1.1.0, Edição 2026) é uma linguagem de programação estaticamente tipada e formalmente verificada para sistemas críticos, inteligência artificial, controle ciberfísico e computação quântica, criada por Ricardo Bueno (@OmegaSoftDLL). Projetada desde os primeiros princípios para engenheiros de sistemas e agentes autônomos de IA, a Lume impõe correção matemática verificada por máquina desde contratos de refinamento no código-fonte até as instruções nativas emitidas em binário.
Toda a cadeia produtiva da Lume opera em regime 100% auto-hospedado Zero-C (lumec == lumec2 == lumec3 em ~3,8 s), ancorada por Diverse Double-Compilation (cc vs clang convergindo para o mesmo binário SHA-256 com 0 bytes de diferença) e verificação mútua clean-room: provador estático embarcado OmniProof-v4 (1.682 obrigações formais provadas em 16 baterias, 0 refutadas ou pendentes em runtime, 372 testes unitários e 122 domínios soberanos), validação simbólica de tradução binária (ltv em 694 funções + ltv_rt nos 18/18 helpers de runtime + checagem .smt2 unsat em lsmt e z3), cobertura estrutural Masking MC/DC com 0/9.618 condições descobertas, 118 kernels criptográficos constant-time [C0011] (TLS 1.3, X.509v3 Ed25519 e entropia NIST SP 800-90B), envelope de segurança 2oo2D clean-room RV32IM (87.224 falhas injetadas → 0 não detectadas), runtime de memória atômica em 4 níveis (31,8× mais rápido e 2.733× menos RAM), interoperabilidade poliglota Camaleão para 9 ecossistemas ([I0003]), dossiê de qualificação assinado (lume qualify PASS: 106/106 sondas e 21/21 gates) e compilação nativa direta para 27 arquiteturas.
What Ships in Lume v1.1.0 — Six Institutional Engineering Pillars
1. 100% Self-Hosted Zero-C Compiler, Assembler & Tooling (lumec == lumec2 == lumec3)
- Bit-Identical Triple-Bootstrap Fixpoint (
~3.8 s): Modular self-hosted compiler passes (compiler/stage1/lume/) compile tolumec1 == lumec2 == lumec3(0byte diff, SHA-2562a32911ee74c39b146cba4976ae12644725e8414d262a89847a5328ebfd386e6) with external C toolchains and linkers disabled (lume zero-c). - Byte-Verified Multi-Container Native Assembler (
lasm.src): Direct binary emission forELF64,PE32+,Mach-O 64,AVX2 VEX,AVX-512 EVEX, andDWARF v4debug tables (.debug_info,.debug_line,.symtab), differentially verified byte-for-byte against GNUasacross39,968generated instructions (1,467alternate-encoding disassembly-identical lines and176malformed lines rejected with[L0001]). - Manifest Integrity & Zero-Drift CLI Control Plane (
lume_driver.src,lcli.src):134SHA-256-locked manifest files (MANIFEST.sha256audited vialume self verify) and114table-driven CLI commands (226command and alias surfaces with0parity drift enforced bylume cli-parity). - Integrated Developer Protocol Suite & Bilingual Manuals (
linteractive.src,lmanual.src): Native JSON-RPC LSP (lume lsp --stdio), DAP (lume dap --stdiowithDWARF v4line mapping and deterministicstepBackreplay), MCP (lume mcp), interactive REPL (lume repl), canonical formatter (lume fmt), and built-in 10-chapterEN/PT-BRprogrammer's manuals (lume manual/lume manual --pt).
2. Multi-Theory Static Theorem Prover & Proof Kernel (OmniProof-v4)
- Embedded
OmniProof-v4Verification Suite (lume self-prove): Discharges1,682proven formal obligations across16proof batteries with0runtime-checked or refuted obligations,372unit tests, and122sovereign domains. - Multi-Theory Decision Procedures (
lcaas.src):QF_LIA: Exact rational/integer Fourier-Motzkin variable elimination, integer cutting planes, and independently checkable Farkas dual witnesses.QF_NIA: Non-linear polynomial Horner/Bernstein bounding envelopes and native quadratic square-completion.- **
QF_BV, Octagons, Separation Logic & WCE...
Lume v1.0.0 — Official Production-Ready Release (Edition 2026)
Lume v1.0.0 — Official Production-Ready Release (Edition 2026)
Lume is 100% complete, self-hosted, and formally verified across Phases 0–5, Inflection Stages A–D, and Waves 1–10.
Highlights
-
100% Self-Hosted Zero-C Steady State (
stage2 == stage3):lumec,lasm,lmod,lcaas,lcert,lfmt,ltest, andlume_drivercompile themselves bit-for-bit (0 diff) in ~3.8s (28.3x speedup). -
10/10 Developer Experience (DX):
- Nested layout-sensitive
match(let ... in match,if ... else match) + inline bracedmatch x { ... } - String interpolation
f"...{expr}..."and"${expr}" - Left-associative
|>pipe operator - Functional record updates
{ s with field: val } - Top-level
constdeclarations &let/vardestructuring for tupleslet (a, b) = ..., recordslet {x, y} = ..., and constructorslet Cons(h, t) = ...
- Nested layout-sensitive
-
Complete Mathematical Verification (
396/396obligations inlume self-prove):-
QF_LIAFourier-Motzkin with integer cutting-plane tightening (tighten_h) - Nonlinear
QF_NIAPositivstellensatz & shifted bilinear monotonicity(x - y) * (z - lb) >= 0 -
QF_BV, Separation Logic,[K0005]W^X DMA protection,[K0006]kernel stack bounds,[C0009]constant-time crypto guard, and standalonelcertproof verification (100% Lume Verified)
-
-
Sovereign Quantum Nexus Engine (
lume_quantum_nexus_engine.src):-
Silq-style linearQubittype checking ([Q0001]) & automatic$U^\dagger$ ancilla uncomputation ([Q0002],qfree) -
QuiZX/PyZXZX-Calculus spider fusion &$7\times$ $T$ -count reduction -
Google Stim$O(n^2)$ stabilizer tableau simulator (GHZ_8) - Rotated Surface Code
[[9, 1, 3]]topological QEC (27/27Pauli errors corrected) &Catalystexact parameter-shift VQE +.qbinhardware pulse synthesizer
-
-
27 Universal Targets & Store/Boot Packagers:
x86_64,aarch64,riscv64,wasm32, Windows PE64, macOS Mach-O (aarch64Apple Silicon &x86_64Intel), Android.apk, iOS.ipa, Bootable.iso, UEFI.efi, CUDA PTX 8.0, Vulkan SPIR-V 1.6, Verilog/VHDL RTL, OpenQASM 3.0, and Quaternary DNA. -
Built-In Bilingual Manual (
EN&PT-BR):lume manual/lume manual --pt/lume help.
SHA-256 Checksums (SHA256SUMS — All 6 Platforms)
47c831d7dbc1ca1dcfef775b2441bdf3be57c58e0c6d1d6f3ab91a4ae6006cd0 lume-v1.0.0-linux-x86_64.tar.gz
a719b97d79f3017a590a90db229f7bfe55a4b73f0ba35078697788e7e04a0387 lume-v1.0.0-linux-aarch64.tar.gz
07ea5258eb95492ba2b561e35d7a9523c55cfc6e654ecf82411ff3325763f4c3 lume-v1.0.0-linux-riscv64.tar.gz
2109ccaa06ee1ca758960929ea378d869e52b4b086072ced1c101f2c80eaf44c lume-v1.0.0-macos-aarch64.tar.gz
d98052d47d87195b4cf33acf5b91073dd5aeff7b2c9e6a36715c1726d2021b89 lume-v1.0.0-macos-x86_64.tar.gz
b8db1dfbe5496c64888b5284803eb70dd242d177a44b71a708cfd794bf707e3d lume-v1.0.0-windows-x86_64.tar.gz
47c831d7dbc1ca1dcfef775b2441bdf3be57c58e0c6d1d6f3ab91a4ae6006cd0 lume-v0.3.0-rc.3-linux-x86_64.tar.gz
2109ccaa06ee1ca758960929ea378d869e52b4b086072ced1c101f2c80eaf44c lume-v0.3.0-rc.3-macos-aarch64.tar.gz
d98052d47d87195b4cf33acf5b91073dd5aeff7b2c9e6a36715c1726d2021b89 lume-v0.3.0-rc.3-macos-x86_64.tar.gz
b8db1dfbe5496c64888b5284803eb70dd242d177a44b71a708cfd794bf707e3d lume-v0.3.0-rc.3-windows-x86_64.tar.gz
dd1cbec1a4bd70e2eeae88e93bbef28f955c3ae2921f7856f971935cac277077 lumec-linux-x86_64
60c561fe58854068567bc94f369424609d49255505e14fb9b5025a627b5b6381 lasm-linux-x86_64