Build Secure Smart Contracts, the Pythonic Way.

Vyper is a smart contract language with a relentless focus on security, simplicity, and readability. It empowers developers to write clean, auditable, and gas-efficient code for the EVM, without common pitfalls.

Security by Design

Write safer code, naturally. Vyper eliminates entire classes of vulnerabilities by design. With built-in overflow checking, reentrancy guards, and bounds checking, you can focus on your logic, not on avoiding language-level traps.

Uncompromising Readability

If you know Python, you're ready to build with Vyper. Its clean, minimal syntax results in code that's easy to read, review, and audit. Less ambiguity means less risk and faster development cycles.

Peak Performance, No Assembly

Get gas performance that rivals low-level code, without sacrificing clarity. Vyper's powerful compiler produces highly optimized bytecode from high-level Pythonic code, so you don't have to compromise.

Discover the Vyper Advantage

Vyper's design philosophy isn't just theoretical. See how its focus on clarity, security, and efficiency translates into simpler, safer, and more performant code in practice.

This simple safe remote purchase contract is not only concise in Vyper, its intent is clear at a glance! By removing modifiers and other complex patterns, Vyper makes code harder to misunderstand.

The Vyper Way

@external
def purchase():
    assert msg.value == 2 * self.value
    assert self.state == State.LOCKED
    
    self.state = State.INACTIVE
    self.buyer = msg.sender
    self.value = msg.value

A Solidity Contrast

modifier condition(bool condition_) {
    require(condition_);
    _;
}
modifier onlyBuyer() { ... }
modifier inState(State state_) { ... }

function purchase() external payable
    inState(State.Locked)
    condition(msg.value == (2 * value))
{
    state = State.Inactive;
    buyer = payable(msg.sender);
    value = msg.value;
}

Less code. Less gas. Less risk. Stop compromising.

Deep Verification

Vyper's design makes deep verification practical on a production smart contract language. It narrows the verification gap by formally connecting high-level security properties through source semantics, compiler correctness, and the EVM execution model.

Vyper Semantics

A public, machine-checked formal semantics for Vyper in HOL4. It defines what Vyper code means and is the foundation for proving properties about real contracts and libraries.

Compiler Verification

Proving the Vyper compiler preserves meaning from source code to EVM bytecode. Work on this is in progress; once complete, source-level proofs carry through to deployed bytecode.

EVM Semantics

A formal EVM model in HOL4, validated against the Ethereum Execution Spec Tests (EEST), with a small residual gap to live network behavior.

Explore vyper-hol on GitHub

Battle-Tested by Industry Leaders

“Vyper makes complex codebases much easier to reason about. Teams that are looking for languages that are safer-by-design should heavily consider using Vyper.”

“Thanks to Vyper, Sugar has become one of the finest examples of onchain products, serving some of the largest protocols and communities on the Superchain.”