Home

Design and project goals: Goals

Design/Implementation

Three kinds of code: specification, proof, and executable

Equality and references support and encoding

Current Work Items (as of July 2, 2021)

Language Design

Google Doc

Ideas with Macros

Idiomatic Syntax

Distinct Mathematical Universe

Parser References

Structuring Proofs

Debugger Use Cases

State Machine (Refinement)

Early Mockup

Mypyvy-inspired and Rust-inspired Mockup

Refinement via Rust Traits

Concurrency

RWLock.dfy

rwlock_unverified.rs

rwlock_verified.rs

concurrency.rs

Related work

Automatic Rust verification tools as of 2021

Rust Verification Workshop