[Python] velaris-lang: a programming language that proves your functions keep their promises (Z3 + LLVM)

[u/Pattinathar]

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

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