RIINA™

Programming language with a Coq-verified core model.

Formal claims, verification status, and gaps published openly.

Security properties in RIINA are tracked as a mix of machine-checked proofs, compiler checks, and explicitly documented gaps. The current verified state lives in RIINA_MASTER_PLAN.md Part 2.

Get Started in 10 Minutes | Writing Secure RIINA | Try the Playground | RIINA vs Rust | Website

  ██████╗ ██╗██╗███╗   ██╗ █████╗
  ██╔══██╗██║██║████╗  ██║██╔══██╗
  ██████╔╝██║██║██╔██╗ ██║███████║
  ██╔══██╗██║██║██║╚██╗██║██╔══██║
  ██║  ██║██║██║██║ ╚████║██║  ██║
  ╚═╝  ╚═╝╚═╝╚═╝╚═╝  ╚═══╝╚═╝  ╚═╝

  Rigorous Immutable Invariant, No Assumptions

Bahasa Melayu | 中文

Write with vibes. Ship with proofs.

---

AI-Native Language

RIINA is a programming language that combines formal verification work with AI-native tooling. The repository contains machine-checked proofs, active compiler checks, and explicitly documented verification gaps, and it is designed from the ground up for AI agents to read, write, and reason about. Code an agent writes is held to the same type and effect checks as any other code, for rules the compiler implements.

AI-Writability: a design goal, not a benchmarked score. Consistent Bahasa Melayu keywords, minimal syntax, strong types, and deterministic compilation are intended to make RIINA easy for AI agents to read and write. (Any single-number "writability score" is an internal self-assessment, not an externally validated metric.)

AI agents: See llms.txt for a machine-readable language reference.

For AI Agents

RIINA provides first-class support for AI-assisted development:

• Programmatic compilation: riinac check --json --stdin accepts source on stdin and returns structured JSON diagnostics
• Full machine reference: llms-full.txt is llms.txt plus the complete keyword, type, effect and security-level tables and the builtin reference, generated from the compiler's own tables
• Stdlib API reference: docs/api/STDLIB.md — every builtin and its type signature, generated from the compiler's own registry (drift-guarded by a test)
• Proof guide: docs/guide/PROOF_GUIDE.md — how to read, build, and extend the Coq lane
• Code patterns: 07_EXAMPLES/ contains 172 example programs across 20 category directories (security, effects, compliance, design patterns, FFI, and more)
• IDE integration: .cursorrules and .clinerules provide pre-configured rules for Cursor and Cline; .github/copilot-instructions.md provides GitHub Copilot context

---

What is RIINA?

RIINA is a programming language with a machine-checked Coq proof corpus and a security-oriented compiler. Coq is the only fully mechanized lane. The other prover lanes hold only small hand-written artifacts: a scoped SMT set of 37 Z3-checked properties, and single smoke specs for TLA+ and Alloy (F* and Isabelle are retired; Lean 4 is empty). The machine-generated mirrors of the Coq tree that used to fill them were archived out of main on 2026-10-20. Each lane has its own claim level in website/public/metrics.json; none is presented as independent verification of RIINA. The shipped compiler enforces core type/effect checks today; broader proof coverage and known gaps are tracked explicitly in RIINA_MASTER_PLAN.md Part 2.

Unlike CompCert or CakeML, the compiler riinac is not itself formally verified. What is proven in Coq is the language model: type safety, effect soundness against the declared effect, and, for the reference-free, recursion-free core, non-interference and termination (the table below and HEADLINE_THEOREMS.md). The compiler is tested against that model, not proven to implement it. An assured mode that runs the Coq-verified checker on every program is planned (REQ-100).

Most languages ask you to trust that your code is secure. RIINA asks you to verify it.

What RIINA has today	Current status
Type safety theorems	Machine-checked in Coq (type_safety is closed under the global context: no axioms, no premises); Rust checker active
Effect algebra and gate model	Machine-checked in Coq, kernel-closed: every perform site of a well-typed term lies within its effect bound, and every configuration reachable by evaluation stays within the declared effect (effect_sound_multi_step_declared, via preservation with ε' ⊑ ε). In the Coq model the typing bound orders effects by a single level (a total order); independently of that order, reachable_effects_from_program_text proves evaluation never produces an effect site absent from the program text and initial store. Compiler tracks and enforces declared effects
Information-flow / non-interference	Proven, kernel-closed, for the reference-free, recursion-free (fix-free) core (ref_free_noninterference): two runs that differ only in TSecret inputs return the same observable result. Enforced by tests beyond it: not yet proven with references or general recursion (REQ-89); the earlier full-calculus NI proofs remain archived. The compiler's IFC typing rules are tested, not proven, against the model
Declassification model	Machine-checked in Coq; shipped compiler/runtime alignment still in progress
Termination and reduction-count independence	Proven, kernel-closed, for the same core: every well-typed program terminates and is strongly normalizing with no premises (ref_free_well_typed_SN), and its reduction count in the model does not depend on secret inputs (ref_free_constant_time: reduction-count independence from secrets in the model, for the core fragment — not a wall-clock timing guarantee on hardware). With higher-order references the SN conclusion is false (Landin's knot, proven: well_typed_SN_conclusion_is_false), so the older well_typed_SN is vacuous and kept only as a recorded counterexample

These are real formal artifacts that compile today, but not every theorem is wired end-to-end into the shipped compiler yet.

---

Why RIINA?

If you write software where security matters, RIINA is for you.

• Building a payments system? RIINA gives you explicit secrets, effects, and auditable formal models.
• Building healthcare software? RIINA gives you language support for confidentiality-focused design and verification.
• Building infrastructure? RIINA gives you explicit effects, proof artifacts, and a narrow trusted surface.
• Building anything? RIINA is aimed at zero-trust software, but current compiler-enforced coverage is narrower than the full proof corpus.

RIINA doesn't care what industry you're in. If you care about getting security right, RIINA's core type and effect rules are proven in Coq for the language model; the compiler is tested against that model.

What makes RIINA different from every other language

Feature	RIINA	Rust	Haskell	Ada/SPARK
Memory safety	Formal model; compiler/runtime alignment in progress	Borrow checker (no proof)	GC	Proven (SPARK subset)
Information flow control	Formal model; compiler enforcement partial	None	None	None
Effect tracking	Implemented + formal model	None	Monads (no proof)	None
Type safety	Formalized in Coq; checker active	Tested	Tested	Proven (SPARK subset)
Zero external dependencies	Yes for the shipped compiler, crypto and stdlib (dev/CI tools are separate, see Install)	No	No	No
Formal proof corpus in repo	Yes — Coq (mechanized): 1,679 core Qed, 9,719 model Qed, 1,443 excluded Qed; see below	No	No	Partial
Session-typed actors	Yes (JALINAN: pelaku, lahir, hantar, terima)	No	No	No
Bahasa Melayu native syntax	Yes	No	No	No

---

Website: ib823.github.io/riina

---

Quick Start

Install

git clone https://github.com/ib823/riina.git
cd riina/03_PROTO
cargo build --release

The compiler binary is riinac. Native builds (riinac build) link with gcc or clang, invoked as cc, on Linux or macOS. On Windows, build inside WSL; MinGW support is planned. MSVC is not supported, because the emitted C uses POSIX headers, and riinac build says so when it finds only cl.

The shipped compiler has zero external runtime dependencies — everything is built from source. Development and CI use separate tools that are not part of it: the Rocq toolchain (proofs), cc and wasmtime (backend differential tests), z3 (the SMT set), fuzz harnesses, and NIST test vectors.

Alternative install methods:

# Docker (build from source)
docker build -t riina .
docker run --rm riina check myfile.rii

# Nix
nix run github:ib823/riina

# Portable installer (builds from source)
bash scripts/install.sh

For the pinned Isabelle/F* toolchains and TLA+/Alloy formal jars used by repo verification on a fresh clone:

bash scripts/provision-smoke-toolchains.sh

Hello World

Create hello.rii:

// Hello World in RIINA
// Keywords are in Bahasa Melayu (Malaysian Malay)
// (This example type-checks and runs on the shipped compiler.)

fungsi utama() -> Teks kesan Tulis {
    biar mesej = "Selamat datang ke RIINA!";
    cetak(mesej);          // 'cetak' prints; its effect is 'Tulis' (Write)
    mesej                  // trailing expression is the return value (no 'pulang;')
}

riinac check hello.rii    # Type-check and verify
riinac run hello.rii      # Run directly
riinac build hello.rii    # Compile to native binary via C

Security in Action

Every block in this section is checked by the test suite (03_PROTO/crates/riinac/tests/doc_snippets.rs). A secret can be hashed and kept, but the checker refuses to let it reach an output:

fungsi proses_pembayaran(kad: Rahsia<Teks>, jumlah: Nombor) -> Teks kesan Kripto {
    biar cap = cincang(kad);                      // OK: a hash of the secret stays secret
    biar resit = "Jumlah: " + ke_teks(jumlah);    // OK: the amount is public
    resit                                         // OK: only public data is returned
}

fungsi utama() -> Unit kesan Tulis {
    biar kad = sulit "4111 1111 1111 1111";
    cetakln(kad)                                  // COMPILE ERROR: a secret at a print sink
}

Returning kad as plain Teks is refused too (Annotation mismatch: expected String, found Secret(String)). The compiler enforces the information-flow rules it implements and is tested against the Coq model; PROPERTY_LEDGER.md lists what is proven, enforced and tested.

Effect System

A function declares its effects with kesan, and the checker rejects a body that does more:

fungsi baca_config(laluan: Teks) -> Tercemar<Teks, FileSystem> kesan SistemFail {
    fail_baca(laluan)                             // file contents are tainted at birth
}

fungsi kira_cukai(pendapatan: Nombor) -> Nombor kesan Bersih {
    pendapatan * 6 / 100                          // integer arithmetic; a float literal is error P0015
}

fungsi kira_cukai(pendapatan: Nombor) -> Nombor kesan Bersih {
    biar _ = fail_baca("cukai.txt");              // COMPILE ERROR: a pure function reads a file
    pendapatan * 6 / 100
}

---

Bahasa Melayu Syntax

RIINA uses Bahasa Melayu (Malaysian Malay) keywords — the first systems programming language with native Southeast Asian syntax.

RIINA	English	Example
fungsi	fn	fungsi tambah(x: Nombor) -> Nombor
biar	let	biar nama = "Ahmad";
kalau	if	kalau x > 0 { ... }
lain	else	lain { ... }
untuk	for	untuk x dalam senarai { ... }
selagi	while	selagi aktif { ... }
pulang	return	pulang hasil;
padan	match	padan nilai { ... }
rahsia	secret	biar kunci: Rahsia<Teks>
dedah	declassify	dedah(nilai)
kesan	effect	kesan Tulis
bersih	pure	kesan Bersih
betul / salah	true / false	Boolean values
ubah	mut	biar ubah x = 0;

You don't need to speak Malay to use RIINA. The keywords are consistent, short, and learnable in an afternoon. But if you do speak Malay, this is the first language that speaks your language.

---

What's Been Built

This is not a whitepaper. This is working software.

Formal Proofs — Current Verified State

Prover	What is actually proven	Notes
Rocq 9.1.1 (Primary)	1,679 core Qed (foundations, type system, properties, effects, termination and the compiler-linked crypto policy); 9,719 model Qed (domain, industry, compliance, crypto and runtime models — facts about their own definitions, not verified systems); 1,443 excluded Qed (vacuous patterns, examples, counterexamples or test files). 0 Admitted, 0 Axiom, 0 Abort	The only fully mechanized lane. 0 Axiom, 29 Parameters (trusted hardware interface; none of the capstone theorems depends on them) — a Parameter is logically equivalent to an axiom in Coq; see PROOF_STATUS.md
SMT / Z3	37 properties of the security lattice and effect join, checked for exact unsat counts by scripts/verify-smt.sh (Z3 4.8.12)	Mechanized at that scope only (REQ-67a, 02_FORMAL/smt/SCOPED_SET.txt)
TLA+ / Alloy	1 hand-written smoke spec each (5 TLC-checked theorems; 6 bounded-checked assertions)	Claim level generated until wired into CI
F*	1 smoke module with 3 trivial lemmas	Lane retired (REQ-67g)
Lean 4 / Isabelle	Nothing	The generated ports were archived (the Lean port at commit fd23fbdb8 had 12,576 declarations, of which 215 ever elaborated); Isabelle is retired. A hand-written Lean re-proof of the core (REQ-67b) has not started
Verus / Kani / TV	None	A few hand-written drafts, quarantined (quarantined: true in metrics.json)

Honest scope:

• Only the Coq active lane constitutes real machine-checked verification. It declares 0 Axiom, 29 Parameters (trusted hardware interface; none of the capstone theorems depends on them), proved jointly satisfiable in the build.
• The Lean, Isabelle, F*, TLA+, Alloy, SMT, Verus, Kani, and TV trees used to hold mirrors generated by scripts/generate-full-stack.py / generate-multiprover.py from the Coq tree. They inflated file and theorem counts but were stubbed (admit/placeholder tactics), so they were archived out of main on 2026-10-20 and are preserved in history at commit fd23fbdb8. Counts from different provers are never added together.
• Core Coq theorems cover foundations, type safety (closed), dynamic effect soundness against the declared effect, declassification lemmas, and — for the reference-free, fix-free core — strong normalization, non-interference and reduction-count independence from secrets in the model. Nine capstone theorems are kernel-attested closed under the global context (axiom-free): type_safety, progress, preservation, accepts_uses_only_current, effect_sound_multi_step_declared, reachable_effects_from_program_text, ref_free_well_typed_SN, ref_free_noninterference, ref_free_constant_time. The last three are fragment results: references and general recursion are not covered (REQ-89), and with higher-order references SN is provably false, so well_typed_SN (full calculus) is vacuous.
• Most domain Coq files are formal models/specifications checked against their own definitions, not verified systems and not compiler-enforced: scripts/detect-vacuous-proofs.py flags 1,318 vacuity patterns (theorems concluding True, reflexivity on hard-coded records, definitional tautologies), ratcheted so the number can only fall. The proofs it flags, plus listed test files, are the 1,443 excluded Qed above.
• See website/public/metrics.json for per-lane claim levels (the authoritative source of truth).

Ledgers (generated by scripts, checked in CI; do not edit by hand):

• HEADLINE_THEOREMS.md — the only theorems a public surface may cite as guarantees, with statement, fragment, kernel assumptions, witnesses and review status
• PROPERTY_LEDGER.md — every advertised property and its claim level (proven in the model, enforced by tests, modelled, planned)
• TRUSTED_BASE.md — everything a guarantee depends on that is not itself proven, with sizes
• PROOF_STATUS.md and AXIOMS.md — proof counts, Admitted/Axiom/Parameter sites
• docs/api/STDLIB.md — the builtin matrix

Compiler & Toolchain (Rust)

Metric	Value
Rust crates	18 in the compiler workspace (03_PROTO), plus the tooling workspace's own crates
Test count	3,661 tests in the compiler workspace, all passing (from website/public/metrics.json), plus the tooling workspace's own tests
External dependencies	0 third-party at runtime in the shipped compiler (dev/CI tools are separate, see Install)
Standard library builtins	374 registered (Malay and English names counted separately), 342 of them compile; see docs/api/STDLIB.md

Crates:

Crate	Purpose
riinac	Compiler driver — check, run, build, emit-c, emit-ir, emit-core, test, doc, fmt, lsp, mcp, repl, verify, pkg
riina-lexer	Tokenizer with 132 bilingual keywords
riina-parser	AST construction
riina-types	Type system definitions (45 types, 19 effects, 6 security levels)
riina-typechecker	Type inference and checking
riina-codegen	IR lowering, C/WASM/mobile code generation, interpreter, FFI
riina-wasm	WASM playground library (in-browser compiler via cdylib)
riina-fmt	Code formatter
riina-lsp	Language Server Protocol (VS Code integration)
riina-doc	HTML documentation generator
riina-pkg	Package manager (SemVer resolution, SHA-256 integrity, effect escalation checking)
riina-arena	Memory arena allocator
riina-span	Source location tracking
riina-symbols	String interning
riina-compliance	Industry compliance-profile checks and report generator (19 profiles, 606 heuristic rules in total): evidence toward a profile; not a conformity assessment or certification

Developer Tools

• VS Code extension — Syntax highlighting, 12 code snippets, LSP integration
• Formatter — riinac fmt for consistent code style
• Doc generator — riinac doc produces HTML documentation
• LSP server — Diagnostics, hover info, keyword completion
• Package manager — riinac pkg init/add/remove/lock/build/publish/list/tree/clean
• Verification gate — riinac verify --fast (zero-trust: runs tests, clippy, Coq audit)
• Docker image — Multi-stage build
• Nix flake — nix run github:ib823/riina or nix develop for full dev shell
• Release scripts — scripts/release.sh (one-command release: bump, tag, tarball, GitHub Release, deploy website), scripts/bump-version.sh, scripts/install.sh
• Website — 7-page site at ib823.github.io/riina: Home, Evidence, Language, Architecture, Compliance (9 industry sectors), Playground and Docs (with the release history); deployed via scripts/deploy-website.sh
• REPL — Interactive mode for experimentation

Example Programs

172 example .rii files across 20 category directories (security, effects, compliance, design patterns, FFI, AI context, JALINAN, showcase, and more).

Parser-support caveat (honest): Many of these examples use language forms the shipped compiler does not yet accept; 83 of the 172 currently pass riinac check (measured 2026-10-20). Until 2026-10-20, 14 more passed that used method-call syntax RIINA does not have (they stopped when field access on non-records became a type error), and 2 that used undeclared type names; 1 came back that day, when a variable named after a keyword became readable. They document the intended language surface. See 07_EXAMPLES/README.md for exactly which forms compile today and a list of the verified-working examples.

Cryptographic Tooling

The riina-core crate in 05_TOOLING/ contains the hand-written cryptographic primitives:

Experimental — not audited. RIINA's in-house cryptography (riina-core) is experimental and has not been audited. Do not use it to protect real secrets yet. No independent audit has been published.

• Symmetric / hashing: AES-256 and AES-256-GCM, SHA-256/384/512 (FIPS 180-4), SHA3-256/512 and SHAKE128/256 (FIPS 202), HMAC (RFC 2104/4231), HKDF (RFC 5869). ChaCha20-Poly1305 is a recognised algorithm name in the crypto-agility policy but is not implemented.
• Asymmetric: X25519 (RFC 7748) and Ed25519 (RFC 8032), checked against the RFC test vectors.
• Post-quantum: ML-KEM-768 and ML-DSA-65, tested byte-exact against NIST known-answer (ACVP) vectors and interoperable with OpenSSL; not validated (no CMVP/CAVP certificate). See reports/precrypto_audit_secondmodel.md — an in-house second-model review, not an independent audit.
• Zero external dependencies in the crypto library (riina-core) — everything auditable from source. (Some release/dev tools in 05_TOOLING do use third-party crates; see SECURITY.md.)
• No floating point, by design. A float literal is a compile error (P0015). Exact integer and fixed-point arithmetic keep programs within what the proofs model.

---

Repository Structure

riina/
├── 02_FORMAL/coq/         375 Coq proof files (335 active)
│   ├── foundations/        Core language semantics
│   ├── type_system/        Progress, Preservation, Type Safety
│   ├── properties/         Logical relations (NI building blocks), Declassification, Composition
│   ├── effects/            Effect algebra and gate proofs
│   ├── domains/            252 domain-specific model files (R-Z, Σ, compliance)
│   ├── termination/        Strong normalization, sized types
│   ├── compliance/         DO-178C, ISO-26262, Common Criteria models
│   └── Industries/         Regulatory/domain formal models
│
├── 02_FORMAL/smt/           Z3 scoped set (37 properties, checked by scripts/verify-smt.sh)
├── 02_FORMAL/tlaplus/       TLA+ hand-written specs (1 smoke spec TLC-checked)
│   └── ...                  (alloy, fstar, verus, kani, tv: hand-written drafts, quarantined or retired;
│                             lean is empty pending REQ-67b — see metrics.json)
│
├── 03_PROTO/               Rust compiler (18 crates, 3,661 tests, 0 third-party runtime deps)
│   └── crates/
│       ├── riinac/         Compiler driver (16 commands)
│       ├── riina-lexer/    Tokenizer
│       ├── riina-parser/   Parser
│       ├── riina-types/    Type system
│       ├── riina-typechecker/
│       ├── riina-codegen/  IR + C backend + interpreter
│       ├── riina-pkg/      Package manager
│       ├── riina-fmt/      Formatter
│       ├── riina-lsp/      Language server
│       ├── riina-doc/      Doc generator
│       ├── riina-arena/    Memory allocator
│       ├── riina-span/     Source spans
│       ├── riina-symbols/  String interning
│       └── riina-compliance/ Compliance-profile checks (evidence, not certification)
│
├── 04_SPECS/               Language specifications, compliance specs
├── 05_TOOLING/             Crypto primitives, build system (Rust)
├── 07_EXAMPLES/            172 example .rii files (83 pass `riinac check`)
├── docs/                   Enterprise docs, multilingual READMEs
├── VERSION                 Semver source of truth
├── CHANGELOG.md            Public-facing changelog
├── website/                7-page Vite/React website (Evidence, Language, Compliance, Playground, etc.)
├── scripts/                Build, install, release, deploy, sync scripts
└── riina-vscode/           VS Code extension

---

Research Scope

The research tracks in 01_RESEARCH/ that have a Coq counterpart are listed below. Every file in the active build compiles with 0 Admitted / 0 Axiom (the build has 29 Parameters, the trusted hardware interface; no capstone theorem depends on them). That is all "Modelled" below claims: the theorems are about each file's own definitions of the domain, not a verification of the named real-world system (the distribution file is a model of Raft/BFT/CRDT properties, not a verified distributed system), and they are not enforced by the compiler. Many are definitional — see the vacuity count above. Only the rows marked otherwise carry a stronger claim.

Track	Domain	Status
A	Core type system, non-interference	Type safety proven (closed); non-interference proven for the reference-free, recursion-free core (REQ-85); enforced by tests beyond it, not yet proven with references (REQ-89)
R	Certified compilation (translation validation)	Modelled
S	Hardware contracts (CPU side-channel models)	Modelled
T	Hermetic build (binary bootstrap verification)	Modelled
U	Runtime guardian (verified micro-hypervisor)	Modelled
V	Termination guarantees (strong normalization — reference-free, fix-free core; general recursion is type-safe but not normalizing, REQ-44)	Proven premise-free for that core (ref_free_well_typed_SN); false with higher-order references (Landin's knot, proven)
W	Verified memory (separation logic)	Modelled
X	Concurrency (session types, data-race freedom)	Modelled
Y	Verified standard library	Modelled
Z	Declassification policy (budgets, robust)	Modelled
Σ	Verified persistent storage	Modelled
—	Industry compliance (jurisdiction models)	Modelled
—	Domain security (timing, protocols, hardware, ...)	Modelled
Π	Verified performance (WCET, SIMD, lock-free)	Modelled
Δ	Verified distribution (Raft, BFT, CRDTs)	Modelled
Ω	Network defense (rate limiting, SYN cookies)	Modelled
Ψ	Operational security (Shamir, duress, dead man)	Modelled
L	FFI boundary safety, attack surface research	Modelled
—	Mobile OS security (subsystem models)	Modelled
—	Security foundations (boot, IOMMU, crypto)	Modelled
—	UI/UX accessibility and safety	Modelled
—	Capital markets (order matching, settlement)	Modelled
—	Physical systems security (sensors, timing)	Modelled

---

Current Status

Build: Passing. Verification: Coq 1,679 core Qed, 9,719 model Qed, 1,443 excluded Qed (vacuous, example, counterexample or test); 0 Admitted, 0 Axiom, 29 Parameters (trusted interface) — Coq is the only fully mechanized lane | 3661 Rust tests | other lanes: a scoped Z3 set and smoke artifacts (generated mirrors archived 2026-10-20; claim levels in metrics.json)

Area	Status
Core compiler	Lexer/parser/typechecker/codegen/interpreter build and pass 3,661 tests (plus the tooling workspace's own tests); the C/native backend is not formally verified — it is differential-tested against the interpreter; end-to-end security alignment still in progress
Standard library and tools	Implemented and test-covered
Formal verification	Coq active lane is the only real machine-checked verification (0 Admitted, 0 Axiom, 29 Parameters (trusted hardware interface; none of the capstone theorems depends on them)). Of the other lanes only the scoped SMT set (37 properties) is mechanized; the rest hold single smoke artifacts or nothing, and the generated mirrors were archived — see metrics.json. No independent audit published yet
WASM/mobile backends	Present as scaffolding, not full production backends
Example programs	Many .rii examples use a block-statement syntax the shipped parser does not yet accept; see 07_EXAMPLES/README.md for which forms currently compile

What's next

• Compiler alignment: Switch the shipped compiler path to the Coq-matching checker.
• Axiom status: Active Coq build has Axiom = 0 and Admitted = 0, but carries 29 Parameter declarations that are axioms in all but name (the trusted hardware interface; none of the capstone theorems depends on them). These are the de-facto trusted assumptions; see PROOF_STATUS.md.
• Prover-lane honesty (Gate D, REQ-29): The generated non-Coq mirrors were archived out of main on 2026-10-20. The next step is a hand-written Lean 4 re-proof of the core (REQ-67b), which has not started.
• Compliance system: --compliance exposes 19 profiles with 606 heuristic rules in total (riinac check --list-compliance). Their output is evidence toward a profile; not a conformity assessment or certification.

---

Security & Verification

RIINA uses compiler-integrated fast checks plus repository-level proof and audit flows. Not every formal verification lane runs inside riinac itself.

riinac verify --fast    # Tests + clippy (runs on every commit via pre-commit hook)
riinac verify --full    # + proof/tooling scans used by the repo hooks
riinac verify --coq     # The Coq lane alone, with the riinac-vs-Coq conformance gate (CI's coq job)
riinac verify --nightly # The Coq lane with that gate on at least 1,000,000 programs (nightly in CI)

Git hooks enforce verification automatically:

• Pre-commit: riinac verify --fast blocks commits with failing tests
• Pre-push: riinac verify --full + GPG signature check + secret detection + Trojan source scan

Install hooks: ./00_SETUP/scripts/install_hooks.sh

Deep verification (manual, 7 levels): bash 05_TOOLING/scripts/verify.sh [0-6]

Verification is enforced automatically via git hooks installed by ./00_SETUP/scripts/install_hooks.sh.

---

Contributing

License

RIINA is source-available, not open source, under the RIINA Proprietary License. In its own terms: programs you write in RIINA are your property, and you may use the compiler commercially and distribute the software you build with it. It does not allow modifying or redistributing the compiler itself.

Clarifications are drafted and waiting for counsel review: explicit permission to read, build and audit the source; an irrevocable runtime-library exception for the code the compiler embeds in your programs; continuity terms; and a trademark policy. They are not in force. Until they are adopted, LICENSE as written governs. This section summarises the licence; it is not legal advice.

Building from source

# Clone and set up
git clone https://github.com/ib823/riina.git
cd riina

# Verify environment
bash 00_SETUP/scripts/verify_setup.sh

# Build compiler
cd 03_PROTO && cargo build --release -p riinac && cd ..

# Run all tests
cd 03_PROTO && cargo test --all && cd ..

# Check a .rii file
./03_PROTO/target/release/riinac check 07_EXAMPLES/hello_dunia.rii

# Run the REPL
./03_PROTO/target/release/riinac repl

# Run the verification gate
./03_PROTO/target/release/riinac verify --fast

# Install git hooks (recommended for contributors)
./00_SETUP/scripts/install_hooks.sh

Read CONTRIBUTING.md for detailed development instructions and coding standards.

---

FAQ

Is RIINA production-ready? The compiler, proofs, and toolchain are functional, but the project is not finished. The repository has passed Phase 4 of the master plan. You can write, compile, and run RIINA programs today, but end-to-end alignment between the shipped compiler and the full proof corpus is still in progress. No independent audit has been published yet, and the in-house cryptography is experimental.

Do I need to know Bahasa Melayu? No. The keywords are short and consistent — fungsi (function), biar (let), kalau (if), pulang (return). You'll learn them in minutes. A cheatsheet is included.

Do I need to understand Coq or formal verification? No. You can use the language without reading the proofs. Some guarantees are enforced directly by the compiler today, while the broader proof corpus is there for auditability and future compiler alignment.

Why zero external dependencies? Trust. The shipped compiler, crypto library and standard library have no third-party runtime dependencies, so every line is auditable from source and there is no third-party crate to be hit by dependency confusion or a left-pad-style removal. Development and CI do use outside tools — the Rocq toolchain, cc, wasmtime, z3, fuzz harnesses and NIST test vectors — which are not part of the shipped compiler.

Why Bahasa Melayu? RIINA developed by Malaysians for the world. Programming languages have been English-only for 70 years. RIINA shows that formal verification and native-language syntax are not mutually exclusive. If a language can be proven correct, it can be proven correct in any language.

How does RIINA compare to SPARK/Ada? SPARK ships mature compile-time proof integration for a well-defined Ada subset. RIINA's research scope includes information flow, effects, and declassification, but the shipped compiler is not yet aligned with the full proof corpus. Today the comparison is strongest at the level of formal ambition and proof inventory, not end-to-end enforcement maturity.

---

RIINA — Rigorous Immutable Invariant, No Assumptions

Q.E.D. Aeternum.

---

_{RIINA™ is a trademark of The RIINA Authors. First use in commerce: February 2026. All rights reserved.}