Skip to content

unsoundsystem/rlsf-verified

BranchesTags

Repository files navigation

Formally verified real-time allocator written in Rust (wip)

Formal verification of rlsf crate using Verus .

Specification & Proof status

function porting specification proof

insert_free_block_ptr_aligned

search_suitable_free_block_list_for_allocation

✓

✓

map_floor

✓

✓

✓

map_ceil

✓

✓

allocate

✓

✓

deallocate

✓

link list manipulation

✓

✓

✓

Verification

To verify the whole codebase:

VERUS_SINGULAR_PATH=/usr/bin/Singular $VERUS_ROOT/source/target-verus/release/verus  --crate-type=lib src/lib.rs --expand-errors --verify-root --triggers-mode silent

About

No description, website, or topics provided.

Resources

Readme
Activity

Stars

2 stars

Watchers

2 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages