Vel

A language for verified low-level software.

It dreams to be something like Rust with logic
― a language that empowers people to build verified low-level software.

Name

The name Vel stands for various concepts.

Vel is a language for verified low-level software.

Vel commits to the velocity of both development and runtime.

Vel wants to be smooth and relaxing like velvet.

Type system

Vel features a dependent ownership type system.

It enables reasoning about runtime objects using some propositions.
Some propositions are copyable (like Rust's Copy), but others are not ― as we are in separation logic!

We can also use Rust-like borrows for sharing, very unlike traditional separation logic.

Architecture

• vel: Vel's language engine, written in Rust.
• vel-vscode: VS Code extension for Vel.