Skip to content
/ lampe Public

Extracting the semantics of Noir to Lean for formal verification

Notifications You must be signed in to change notification settings

reilabs/lampe

This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Repository files navigation

Lampe

Lampe (/lɑ̃p/), a light to illuminate the darkness

This project contains a model of Noir's semantics in the Lean programming language and theorem prover. The aim is to support the formal verification of both the Noir language semantics and the properties of programs written in Noir.

Building

In order to build this you will need to clone the Reilabs fork of the Noir repo next to the clone of this repo. In other words, if you have this repository at reilabs/lampe, then that fork needs to be at reilabs/noir. You will also need to check out the lampe branch in the noir repo. This will allow the Rust project to build.

The Lean project should build on its own.