u/Pattinathar

The idea: I wanted a language where you can trust a function just by reading its first line. So the signature says what effects it uses (a function without "uses net" can't touch the network), whether it can fail (ignoring that doesn't compile), and any promises it makes about its result.

Those promises get checked by the Z3 theorem prover before the program runs. If your code breaks one, it tells you the exact input that breaks it: error[E700] promise cannot be kept: 'discount' ensures result >= 0 proven without running the program: price = 5 gives result = -5

The part I'm most pleased with is the float handling. It proves in real IEEE-754 rather than pretending floats are perfect decimals, so it refuses to certify x + 0.1 + 0.1 == x + 0.2 and hands you the exact number where it breaks. A lot of tools would just "prove" that and be wrong.

Playground, runs in your browser, nothing to install:

https://gowrishankar-infra.github.io/velaris-lang/playground.html

Repo: https://github.com/gowrishankar-infra/velaris-lang

Built with a lot of AI help over 40+ releases. It's got a REPL, editor support, a standard library written in itself, CI, and one-file downloads for Windows/Mac/Linux. Happy to answer anything. Thank you

The idea: I wanted a language where you can trust a function just by reading its first line. So the signature says what effects it uses (a function without "uses net" can't touch the network), whether it can fail (ignoring that doesn't compile), and any promises it makes about its result.

Those promises get checked by the Z3 theorem prover before the program runs. If your code breaks one, it tells you the exact input that breaks it: error[E700] promise cannot be kept: 'discount' ensures result >= 0 proven without running the program: price = 5 gives result = -5

The part I'm most pleased with is the float handling. It proves in real IEEE-754 rather than pretending floats are perfect decimals, so it refuses to certify x + 0.1 + 0.1 == x + 0.2 and hands you the exact number where it breaks. A lot of tools would just "prove" that and be wrong.

Playground, runs in your browser, nothing to install:

https://gowrishankar-infra.github.io/velaris-lang/playground.html

Repo: https://github.com/gowrishankar-infra/velaris-lang

Built with a lot of AI help over 40+ releases. It's got a REPL, editor support, a standard library written in itself, CI, and one-file downloads for Windows/Mac/Linux. Happy to answer anything. Thank you

Signatures declare effects (a function without "uses net" can't touch the network), failure (ignoring it doesn't compile), and contracts that Z3 proves before the program runs — with the exact counterexample when they don't hold. Float proofs use real IEEE-754, so it refuses to "prove" x + 0.1 + 0.1 == x + 0.2.

Try it in your browser, nothing to install:

https://gowrishankar-infra.github.io/velaris-lang/playground.html

MIT, AI-assisted build (disclosed in the README). Thank you

I built a language where the signature carries the guarantees, and I wanted to share the implementation choices since this crowd cares about the how.

Pipeline: lexer → parser → loader → effect checker → type checker → Z3 proof pass → LLVM JIT (llvmlite) → interpreter, all in one file in pipeline order.

Three things that might interest you:

1. The proof pass explores paths symbolically and checks requires/ensures/loop invariants in Z3, with modular call summaries (a callee's contract is assumed at the call site rather than inlining its body). Lists use the theory of arrays, records get per-field symbolic values, and all_of/any_of become real quantifiers with the predicate body inlined under the For All.

2. Floats are proven in Z3's genuine IEEE-754 theory, not modelled as reals — so the prover refutes x + 0.1 + 0.1 == x + 0.2 and returns the exact double. FP queries get a bigger solver budget (30s vs 3s) since bit-blasting is slow; integer proofs stay instant.

3. The JIT covers pure Int/Float/Bool functions with typed codegen. Division and modulo are deliberately left interpreted in both modes —native fdiv by zero gives infinity while the language promises a clean error, and I'd rather lose the optimization than have the two engines disagree. Every native change ships with a differential test: same program, both engines, diff must be empty.

One soundness lesson: when I added quantifiers, the first test run produced a false counterexample. Turned out untranslatable `requires` premises had been silently dropped since an early version — harmless for "proven" claims, but capable of manufacturing false alarms. Now an untranslatable premise aborts the proof entirely and falls back to runtime checks.

Repo: https://github.com/gowrishankar-infra/velaris-lang

Playground (Pyodide, real compiler in-browser):

https://gowrishankar-infra.github.io/velaris-lang/playground.html

Disclosure: built pair-programming with an AI across 40+ releases; design decisions mine, commit history is the honest record. Beginner here, so tear the implementation apart — especially the prover.

I started this knowing basically nothing about compilers. The idea I couldn't let go of: with so much code being AI-generated now, I wanted a language where you can trust a function just by reading its signature.

So in Velaris, the signature says everything. What effects it uses (a function without "uses net" literally cannot touch the network). Whether it can fail (and ignoring failure doesn't compile). And promises like "ensures result >= 0" that get proven by Z3 BEFORE the program runs. If your code breaks a promise, you get the exact input that breaks it: error[E700] promise cannot be kept: 'discount' ensures result >= 0 proven without running: price = 5 gives result = -5

My favourite part: float promises are proven in actual IEEE-754, so it refuses to "prove" x + 0.1 + 0.1 == x + 0.2, and hands you the exact double where it breaks. Most tools pretend floats are perfect reals. Mine doesn't.

Playground (runs the real compiler in your browser, nothing to install):

https://gowrishankar-infra.github.io/velaris-lang/playground.html

Repo: https://github.com/gowrishankar-infra/velaris-lang

Being upfront: the implementation is one big readable Python file, so it's not fast (pure numeric functions do JIT to native via LLVM though). No lambdas yet. Loop invariants are written by hand, not inferred. And I built this pair-programming heavily with AI — the design decisions were mine, argued over 40+ releases, and the commit history is the honest record of both of us making mistakes.

I'm a beginner who got obsessed. Tear it apart if you can make the prover say "proven" about something false, I treat that as a security bug and I want to know. Thank you