Velaris

Trust code you didn't write.

A language where the signature tells you everything — the types, the effects, whether it can fail, and promises mathematically proven before the program runs.

PyPI tests release license

Playground · Documentation · Library reference · Error index

fn discount(price: Int) -> Int
    requires price >= 0
    ensures result >= 0
{
    return price - 10
}

error[E700] promise cannot be kept: 'discount' ensures result >= 0
  proven without running the program: price = 5 gives result = -5

That ensures is not a comment or a runtime assert. The Z3 theorem prover verifies it for every possible input before execution — and refutes it with an exact counterexample when it lies.

Why Velaris

Guarantee What it means
Effects are visible uses io, net, fs — a function without uses net can never touch the network, transitively. Hidden behavior does not compile.
Promises are proven requires / ensures / loop invariant, verified by Z3 with modular call summaries — including records, maps, nested lists, quantified list properties, failure paths, and floats in genuine IEEE-754 (the prover refutes x + 0.1 + 0.1 == x + 0.2 with the exact double that breaks it).
Failure is unignorable -> Int or fail in the signature; callers must check or try. Forgetting the error path is a compile error — builtins included.
Fast where it's safe Pure functions over numbers, list reads, and text — including text built inside them — JIT to native code via LLVM (~10,000× on hot arithmetic, ~45× on text building), differential-tested against the interpreter. Native reads are bounds-guarded and text is built in a runtime-owned buffer, so results always match interpreted.

Why floats are proven in IEEE-754 rather than as real numbers, and what that costs: docs/floats.md.

Loops without written invariants are handled where the boring invariants suffice: the compiler proposes bounds on each counter and keeps the ones a loop step cannot break (see examples/inferred.vel). Anything richer — membership, sortedness — still needs an invariant line.

The prover never claims "proven without running" unless the counterexample is premise-complete — untranslatable assumptions abandon the proof to runtime checks rather than risk a false alarm. Soundness reports are treated as security issues.

Install

pip install velaris-lang
velaris doctor
velaris new hello && cd hello && velaris main.vel

Standalone executable (no Python required) — download for Windows / Linux / macOS from the latest release, then:

velaris doctor

With Python 3.10+:

pip install velaris-lang
velaris new hello && cd hello && velaris main.vel

Zero install — the playground runs the real compiler in your browser.

Optional extras for source installs: pip install ".[full]" adds z3-solver (compile-time proofs) and llvmlite (native speed); without them, promises are checked at runtime and everything runs interpreted — same language, honestly degraded.

Everyday ergonomics

keep_if(xs, fn(n: Int) -> Bool { return n % 2 == 0 })   // inline functions
format("hi {}, {} left", name, count)                    // text with holes
args()                                                   // command line
post(url, body) / fetch_status(url)                      // not just GET

Function values are lifted to real functions, so proofs and native compilation apply to them unchanged — and they can carry their own requires / ensures, proven like any other function's. They can't capture surrounding variables — the compiler tells you to pass them in instead.

Two real programs

examples/ledger.vel — an expense tracker: records, integer cents, file persistence, sorted reports. examples/wordcount.vel — text analysis: velaris examples/wordcount.vel <file> [n] counts word frequencies and prints a ranked histogram. examples/fetcher.vel — an HTTP tool: checks a status, then summarises a page, with every network call declared and every failure handled.

Libraries

velaris add https://example.com/geo.vel as geo   # vendored into lib/
velaris deps                                     # what you depend on
velaris verify                                   # unchanged since?

A library is compiled before it is accepted, recorded with its exact sha256 in velaris.toml, and kept in your repository where you can read it. No registry, no resolver, nothing fetched at build time.

Imports

import "lib/geo.vel" as geo      // named: geo.distance(a, b)
import "std.vel"                 // flat: sort(xs)

A named import prefixes that library's functions, so two libraries that both export distance can be used in the same file.

Tooling

velaris trace program.vel (watch every call as it happens) · velaris test program.vel (runs every test_* function written in Velaris) · velaris check program.vel (compile without running; several files at once, --json for tools) · velaris explain program.vel (a walkthrough of every function: effects, promises, and whether they are proven — explain <folder> maps a whole project) · velaris repl (definitions are proof-checked as you type them) · velaris fmt (canonical style, --check for CI) · velaris lsp (errors as you type in any LSP editor; a VS Code extension lives in editor/vscode) · velaris doctor · velaris new · --json errors for automation.

Standard library

Written in Velaris, in stdlib/std.vel — and it keeps its own promises: sort carries ensures is_sorted(result), max_of requires a nonempty list, and violating a library requires is a compile error at your call site. Full reference, generated from the real compiler.

Numbers

Whole numbers are 64-bit. Arithmetic that outgrows that range is an error, not a silent wrap — and the same error whether your code is interpreted or running as machine code. Floats are IEEE-754 doubles, proven as such.

Stability

Semantic versioning: breaking changes only at major versions (v2.0 migrated the fallible builtins, compiler-guided). CI tests every push on Linux and Windows, Python 3.10 and 3.12, with and without the optional dependencies. Errors are stable, numbered, and fully documented.

Contributing

The entire implementation is one readable file, velaris.py, in pipeline order — lexer to LSP. Start with CONTRIBUTING.md; 52 example programs in examples/ each carry an expected verdict (half are designed to be rejected — each rejection demonstrates a guarantee).

License

MIT © Gowri Shankar

Project links

Data verified by PyPI on Aug 18, 2026
Data provided by the project maintainers, verified at the time the release was uploaded to PyPI.

Key dates

PyPI data
Data sourced directly from PyPI's database.
  • Released:
Newer release available (2.59.0)

1 maintainer

PyPI data
Data sourced directly from PyPI's database.
Avatar for khaga from gravatar.com khaga

Credits

Author: Gowri Shankar

GitHub Statistics

Data verified by PyPI on Aug 18, 2026
The GitHub source repository was provided by the project maintainers and verified by PyPI at the time of upload. Stars, forks, and open issues/PRs are derived from that repository and have not been independently verified.

License

MIT License

Requires

Python >=3.10

Provides Extra

full

Tags

compiler contracts effects language verification z3

Report project as malware

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

velaris_lang-2.24.0.tar.gz (228.5 kB view details)

Uploaded Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

velaris_lang-2.24.0-py3-none-any.whl (58.4 kB view details)

Uploaded Python 3

File details

Details for the file velaris_lang-2.24.0.tar.gz.

File metadata

  • Download URL: velaris_lang-2.24.0.tar.gz
  • Upload date:
  • Size: 228.5 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/7.0.0 CPython/3.13.14

File hashes

Hashes for velaris_lang-2.24.0.tar.gz
Algorithm Hash digest
SHA256 2e84faf662d88cd60fbaee1bfa018bcb6c994557643725cee7fdff26d9d9ae78
MD5 edd77748b2b4466b11e5865275fa9dee
BLAKE2b-256 29d25152dc1d02c35ed639de2b4dca149353bbf33c8c31de79ff4231ef0b4c3b

See more details on using hashes here.

Provenance

The following attestation bundles were made for velaris_lang-2.24.0.tar.gz:

Publisher: release.yml on gowrishankar-infra/velaris-lang

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file velaris_lang-2.24.0-py3-none-any.whl.

File metadata

  • Download URL: velaris_lang-2.24.0-py3-none-any.whl
  • Upload date:
  • Size: 58.4 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/7.0.0 CPython/3.13.14

File hashes

Hashes for velaris_lang-2.24.0-py3-none-any.whl
Algorithm Hash digest
SHA256 c6e2e3d3675162a04e9b78d32d0ba52b5e9dfb2ce06eb5525f72c1c5ee6e5aa0
MD5 1f5624078b07df0e89cfb82052fbe1be
BLAKE2b-256 a1b0ab1a98a5b87757ac59a868ed5ee96721729e91d0e3e42dc1bb37aab0010c

See more details on using hashes here.

Provenance

The following attestation bundles were made for velaris_lang-2.24.0-py3-none-any.whl:

Publisher: release.yml on gowrishankar-infra/velaris-lang

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Release history Release notifications | RSS feed

2.59.0

2 files

2.58.0

2 files

2.57.0

2 files

2.56.0

2 files

2.55.0

2 files

2.54.0

2 files

2.53.1

2 files

2.53.0

2 files

2.51.0

2 files

2.50.0

2 files

2.49.0

2 files

2.48.0

2 files

2.47.0

2 files

2.46.0

2 files

2.45.0

2 files

2.44.0

2 files

2.43.0

2 files

2.42.0

2 files

2.41.2

2 files

2.41.1

2 files

2.40.1

2 files

2.40.0

2 files

2.39.1

2 files

2.39.0

2 files

2.38.0

2 files

2.37.0

2 files

2.36.4

2 files

2.36.3

2 files

2.36.2

2 files

2.36.1

2 files

2.36.0

2 files

2.34.0

2 files

2.33.0

2 files

2.32.0

2 files

2.31.0

2 files

2.29.0

2 files

2.28.0

2 files

2.27.0

2 files

2.26.0

2 files

2.25.0

2 files

2.24.1

2 files

This release

2.24.0 This release

2 files

2.23.0

2 files

2.22.1

2 files

2.22.0

2 files

2.21.0

2 files

2.20.0

2 files

2.19.0

2 files

2.18.2

2 files

Anthropic, PBC Visionary sponsor Bloomberg Visionary sponsor Hudson River Trading Visionary sponsor Meta Visionary sponsor NVIDIA Visionary sponsor Microsoft Sustainability sponsor Depot Continuous Integration AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page