SearcharxivSearch

arXiv subjects

Julien Tesson

Publications and source records attributed to Julien Tesson.

5 recordsLinked to original sources

Canonical LST: A Protocol-Native Liquid Staking Solution for Tezos

Canonical LST (sTEZ) is an enshrined, protocol-native mechanism designed to mitigate the centralization risks associated with liquid staking intermediaries. Intended to complement direct staking rather than replace it, Canonical LST provides a neutral, public alternative managed directly by the Tezos protocol. It allows any tez holder to participate in aggregated staking without reliance on third-party operators. sTEZ follows an accrual-based design: all slashing events and rewards are reflected in the token's exchange rate to tez, keeping balances fungible while exposing holders to the precise economics of staking. This approach ensures that liquid staking functions as fundamental network infrastructure--with deterministic lifecycle rules, transparent on-chain data, and governance anchored in the amendment process--rather than as a discretionary commercial product. This white paper summarises the motivation for enshrining liquid staking, the core mechanics, exchange-rate model, regulatory touchpoints, risk posture, and forward-looking roadmap for Canonical LST.

cs.DC

Making Tezos smart contracts more reliable with Coq

Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. This article gives an overview of efforts using the Coq proof assistant to have stronger guarantees on Michelson smart contracts: the Mi-Cho-Coq framework, a Coq library defining formal semantics of Michelson, as well as an interpreter, a simple optimiser and a weakest-precondition calculus to reason about Michelson smart contracts; Albert, an intermediate language that abstracts Michelson stacks with a compiler written in Coq that targets Mi-Cho-Coq.

cs.PL

Albert, an intermediate smart-contract language for the Tezos blockchain

Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. In this article we present Albert, an intermediate language for Tezos smart contracts which abstracts Michelson stacks as linearly typed records. We also describe its compiler to Michelson, written in Coq, that targets Mi-Cho-Coq, a formal specification of Michelson implemented in Coq.

cs.PL

Introduction to the Tezos Blockchain

Tezos is an innovative blockchain that improves on several aspects compared to more established blockchains. It offers an original proof-of-stake consensus algorithm and can be used as a decentralized smart contract platform. It has the capacity to amend its own economic protocol through a voting mechanism and focuses on formal methods to improve safety.

cs.DC

Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts

Tezos is a blockchain launched in June 2018. It is written in OCaml and supports smart contracts. Its smart contract language is called Michelson and it has been designed with formal verification in mind. In this article, we present Mi-Cho-Coq, a Coq framework for verifying the functional correctness of Michelson smart contracts. As a case study, we detail the certification of a Multisig contract with the Mi-Cho-Coq framework.

cs.PL