mvl \ the maximum verifiable language

If it compiles, it's correct

The smallest language where the compiler verifies the most: eleven properties proven at compile time, in the smallest grammar that can carry them.

The LLM handles the syntax. The compiler handles the proof.

install \ 10 seconds

curl -fsSL https://mvl-lang.org/install.sh | sh

hello, verified world \ effects are never hidden

fn main() -> Unit ! Console {
    println("Hello, world!");
}

What the compiler proves.

Every program passes eleven verification checks before any code is emitted. Code that compiles is well-formed; tests handle whether it does the right thing.

# proves prevents

01 \ Type safety (ADTs) impossible states

02 \ Memory safety use-after-free, buffer overflow

03 \ Exhaustive matching unhandled cases

04 \ Null elimination null pointer dereference

05 \ Error visibility silent error swallowing

06 \ Ownership (linearity) double-free, resource leaks

07 \ Effect tracking hidden side effects

08 \ Termination infinite loops in total functions

09 \ Data race freedom concurrent access on shared state

10 \ Refinement types out-of-range values

11 \ Information flow secret and tainted data leaks

Try breaking it.

// the compiler proves 5 > 0 — no runtime check
fn double(x: Int where x > 0) -> Int where self > 0 {
    x * 2
}

fn main() -> Unit ! Console {
    let result: Int = double(5);
    println(result.to_string())
}

// double(-1) — compile error
error[REQ10]: refinement predicate violated
 --> example.mvl:6:23
  |
6 |     let result: Int = double(-1);
  |         ^^^^^^^^^^ argument violates refinement `self > 0`

why \

\Cybersecurity. AI-speed attacks need compile-time defenses. Injection, secret leakage, buffer overflow: code an attacker would exploit doesn't compile.
\Safety. Mission-critical systems require formal evidence. Every property proven at compile time is an audit artifact, generated automatically.

designed for ai generation \

\~10 statement forms, ~5 expression forms, ~3 declaration forms
\No macros, no inheritance, no exceptions, no null
\One way to do each thing — every dropped ambiguity is a property the compiler can now verify