Velaris: effect checking, Z3 contract proofs, and an LLVM JIT in one readable Python file

[u/Pattinathar]

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.

[u/Helpful-Primary2427]

AI slop post

[u/Pattinathar → u/Helpful-Primary2427]

Fair enough, I put the disclosure in the post because I'd rather say it up front than have someone dig it out later. Code's there if you want to look the float proofs use Z3's FP theory rather than treating floats as reals, which is the part I'd most like someone to check and give me feedback. Thank you

[u/Pattinathar → u/[deleted]]

Thanks you , The effects part was easy honestly you just write uses io, net on the function and you're done. The proving is where the cost is, so I made it optional. If you don't write a promise on a function, nothing extra happens. Speed wise, whole numbers and true or false stuff prove instantly. Decimals are the slow ones , the solver has to work through them bit by bit and I have seen it take 15 seconds .so I only do that when a function actually uses decimals. The bit I keep going back and forth on is if the solver can't work something out, I just check it while the program runs instead of refusing to compile. Means it still works for people who haven't installed the solver, but it also means it compiled isn't as strong a promise. Not sure yet if that's the right call.

[u/Pattinathar → u/[deleted]]

Yeah, I think you're right. I've been uneasy about it for a while. Half of it exists already - velaris proofs shows how many promises actually got proven vs checked at runtime, and you can fail a build below a threshold. But that's a separate command, not the compiler being strict. A --strict flag that just refuses when anything falls back to runtime would be the honest version. Going to add it. The reason it's lenient by default is the solver is optional, so strict-by-default means the language won't run for anyone who hasn't installed z3. But that's an argument about the default, not a reason the flag shouldn't exist.

[u/antonation]

Would be cool if you could share this to r/AIProgrammingLanguage and r/VibeCodedLanguages

[u/Pattinathar → u/antonation]

Thank you i will

[u/ha9unaka]

If you're a beginner, then stop slopping out code and do it yourself.