Skip to content

reilabs/lampe

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.

Testing

To run rust tests you need to bump stack size. Use command:

RUST_MIN_STACK=16777216 cargo test

About

Extracting the semantics of Noir to Lean for formal verification

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Contributors 5