rust-lean

KO | EN

gitlite — search

#javascript #python #react #ai #go #android #machine-learning #deep-learning #windows #cli #kubernetes #vue #pytorch #mcp

(★ 11)

Verification of Rust code in Lean 4

rust-lean 최신버젼 다운로드

최종 버전 다운로드 (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

Rust verification in Lean 4
---------------------------------------

A collection of formal verification projects for zero-knowledge virtual machine components. Each subdirectory is a self-contained project where Rust code is translated to Lean 4 using [Hax](https://github.com/cryspen/hax) or [Aeneas](https://github.com/AeneasVerif/aeneas), and then formally verified.

## Projects

| Directory                                                            | Pipeline      | Description                                                                                           |
|----------------------------------------------------------------------|---------------|-------------------------------------------------------------------------------------------------------|
| [`hax-FRI/`](./hax-FRI/)                                             | Hax → Lean    | Verification of one-step FRI folding from [Plonky3](https://github.com/Plonky3/Plonky3)               |
| [`hax-horner/`](./hax-horner/)                                       | Hax → Lean    | Horner polynomial evaluation from Plonky3, with CompPoly spec and proofs                              |
| [`hax-merkle/`](./hax-merkle/)                                       | Hax → Lean    | Merkle root recomputation and inclusion verification from [RISC Zero](https://github.com/risc0/risc0) |
| [`hax-annotations-adc/`](./hax-annotations-adc/)                     | Hax → Lean    | 32-bit limb addition with carry (`adc`), verified via Hax annotations and `bv_decide`                 |
| [`aeneas-FRI/`](aeneas-FRI/)                                         | Aeneas → Lean | FRI folding functions (`fold_step`, `fold_arity`) translated via the Aeneas pipeline                  |
| [`Plonky3-Field-Arithmetic/Hax`](Plonky3-Field-Arithmetic/Hax)       | Hax → Lean    | Generation of Lean 4 code via Hax from Rust models of Plonky3's Mersenne31 and KoalaBear fields       |
| [`Plonky3-Field-Arithmetic/Aeneas`](Plonky3-Field-Arithmetic/Aeneas) | Aeneas → Lean | Verification of addition and multiplication functions of Rust models of Plonky3's Mersenne31          |

Each project has its own README with details on the verification target, pipeline specifics, and current status.

## Building

Each Lean project can be built independently with `lake build` from its respective directory. Rust crates can be built with `cargo build`. See individual project READMEs for specific instructions.

rust-lean

rust-lean 최신버젼 다운로드

오늘의 추천 프로젝트

Was this content helpful?

Recent Feedback

rust-lean

rust-lean 최신버젼 다운로드

오늘의 추천 프로젝트

Was this content helpful?

Recent Feedback

Download README