Upload Code
Package Summary Specifications Assumptions Verification Results Our open standard Verify it yourself Install Docker Docker image

Formal Verification Certificate

ironkv — certified snapshot

This software package satisfies these specifications with these assumptions (see below). Specifically, everything shown with green text or background is auto-certified by VeriLib (and you can trivially re-verify it yourself), while what's shown with white background are unverified claims by the project team, included for pedagogy.

Certification date April 17, 2026
Package commit 08be20c
Functions Verified 212/212
Ethereum Proof Etherscan
Package Summary
GitHub VeriLib

Package Summary

This repository is a formal verification project for IronSHT, a distributed sharded hash table, ported from Microsoft's IronFleet (Dafny) into Verus, a verification tool for Rust that checks specifications and proofs via SMT solving. The original IronFleet system provides a verified distributed key-value service; this project re-implements and re-verifies the per-host protocol and implementation in Rust, proving that the executable code refines an abstract host state machine.

The verified code covers a sharded key-value protocol where hosts own ranges of keys, serve Get and Set requests, redirect clients to the correct owner, and transfer key ranges between hosts via Delegate and Shard operations. Verus proofs establish that every implementation step — including marshalling, network event abstraction, delegation map updates, and single-delivery message sequencing — satisfies the abstract host protocol specification. Each host step is shown to produce I/O that matches the trusted host_protocol_t::next transition relation over the abstract state.

This version targets the host-level verification from IronFleet. It does not replicate IronFleet's full distributed-system refinement layer (which proves that the composed hosts, in the context of a TLA-style network model, implement the high-level service spec), nor does it prove liveness or crash recovery. The focus is on implementation-level reasoning: that the Rust executable faithfully implements the per-host protocol.

Applications

  • Sharded hash tables distribute key-value storage across multiple servers, enabling horizontal scaling for workloads that exceed a single machine's capacity.
  • Verified protocol implementations provide assurance that operations like key migration (sharding/delegation) and client redirection behave correctly, preventing subtle bugs that can cause data loss or inconsistency in distributed deployments.
  • The per-host refinement proofs serve as a foundation for building fully verified distributed systems, where higher-level distributed reasoning (e.g., via TLA+ or similar frameworks) can compose with the verified host implementation.
Specifications

An easier way to view the specifications is to click on the corresponding functions in VeriLib.

Assumptions
Verus Verifier

We assume that the Verus verification system, including its standard library (vstd), correctly implements its verification logic and sound reasoning principles.

Z3 SMT Solver

Verus relies on the Z3 automated theorem prover for checking logical conditions. We assume that Z3 correctly implements SMT solving algorithms.

Rust Compiler

We assume that the Rust compiler correctly translates our verified code into machine instructions, and that it respects the semantics Verus reasons about.

Known Properties

Mathematical truths whose known proofs are not replicated within this project.

Dependencies

We assume correctness of the dependencies listed in the Cargo.toml file, primarily the Verus standard library (vstd).

Rust Features

Some functions are marked external_body with manually written postconditions because they use Rust features Verus doesn't support (iterators, HashMap) or interface with C# infrastructure (network I/O, buffer management). We assume these correctly implement their specifications and that HashMap's hash function is deterministic.

Hardware

We assume correct execution of machine code by the processor.

Network Model

We assume an asynchronous network where messages may be delayed but eventually delivered, with no Byzantine faults. The protocol implements single-delivery semantics via sequence numbers and acknowledgments, ensuring each message is delivered at most once.

Serialization Injectivity

We assume marshalling (serialization) is injective: distinct abstract values produce distinct byte sequences. This ensures that unmarshalling recovers the original value. The marshalling framework relies on size-prefixed encoding and type tags to achieve unambiguous parsing.

Key Ordering

Keys are represented as u64 values with a total ordering. We assume the comparison operations correctly implement mathematical ordering properties (reflexivity, antisymmetry, transitivity). Key ranges \[lo, hi) behave as mathematical half-open intervals.

Delegation Map Completeness

We assume the delegation map is always "complete": every key in the key space is owned by exactly one host at any point in time. The Shard and Delegate operations correctly transfer ownership of key ranges between hosts while maintaining this invariant.

Verification Results

Below are the formal verification results. Please check if the first test line says "VerificationSuccess": true.

Manifest
{
  "VerificationSuccess": true,
  "atoms_note": "Verified keys: unified verification-status verified, error/failed (or similar), or proofs.verified; excludes unverified/trusted. Manifest counts: unified data — TBV = verified + error/errored; list = verified keys only. [worker] Counts recomputed from probe-verus extract on disk (status-only rules).",
  "branch": "main",
  "build_arg_commit": "08be20c3c35692138b495200ec50d1035666e3a5",
  "cargo_package": "",
  "cert_readme_badge_alt": "VeriLib Certified",
  "cert_readme_badge_image_url": "https://verilib.org/assets/img/verilib-certified-badge-wide.svg",
  "cert_readme_page_url": "https://verilib.org/cert/5167",
  "commit": "08be20c3c35692138b495200ec50d1035666e3a5",
  "commit_date_utc": "2026-02-20T15:45:13-08:00",
  "image": "cert-probe-docker",
  "image_build_date_utc": "2026-04-17T11:15:23Z",
  "probe_extract_completed_at_utc": "2026-04-17T11:15:23Z",
  "probe_verus_version": "6.9.1",
  "repo": "https://github.com/verus-lang/verified-ironkv.git",
  "source_tree_sha256": "d49a5e1fa0d09457ffb7636f24b7224016342be210d8a74b5a4dc3abf7ffa0c2",
  "to_be_verified": 212,
  "unified_extract_json_path": "/opt/cert-target-src/ironsht/.verilib/probes/verus_ironsht_0.1.0.json",
  "unified_extract_json_sha256": "7f00b77f7dfbc9362fbc0b576cd28f2ab538d4685e7c203705e07ae1b91eefd2",
  "verification_source": "unified_extract_json",
  "verified_functions": [
    "probe:ironsht/0.1.0/args_t/clone_arg()",
    "probe:ironsht/0.1.0/args_t/clone_vec_u8()",
    "probe:ironsht/0.1.0/choose_v/verus_extra/choose_smallest()",
    "probe:ironsht/0.1.0/cmessage_v/&CMessage#CMessage#clone_up_to_view()",
    "probe:ironsht/0.1.0/cmessage_v/&CMessage#CMessage<bool>#is_message_marshallable()",
    "probe:ironsht/0.1.0/cmessage_v/CMessage#view_equal_spec()",
    "probe:ironsht/0.1.0/cmessage_v/CMessage<&Option<Vec<u8>>>#clone_value()",
    "probe:ironsht/0.1.0/cmessage_v/clone_optional_value()",
    "probe:ironsht/0.1.0/cmessage_v/clone_up_to_view()",
    "probe:ironsht/0.1.0/cmessage_v/is_key_valid()",
    "probe:ironsht/0.1.0/cmessage_v/is_marshallable()",
    "probe:ironsht/0.1.0/cmessage_v/is_value_valid()",
    "probe:ironsht/0.1.0/cmessage_v/view_equal_spec()",
    "probe:ironsht/0.1.0/delegation_map_v/&DelegationMap<K>#DelegationMap#valid_implies_complete()",
    "probe:ironsht/0.1.0/delegation_map_v/&DelegationMap<K>#DelegationMap<&K>#get()",
    "probe:ironsht/0.1.0/delegation_map_v/&DelegationMap<K>#DelegationMap<&K>#get_internal()",
    "probe:ironsht/0.1.0/delegation_map_v/&DelegationMap<K>#DelegationMap<&KeyIterator<K>>#empty_key_range_is_consistent()",
    "probe:ironsht/0.1.0/delegation_map_v/&DelegationMap<K>#DelegationMap<&KeyIterator<K>>#range_consistent_impl()",
    "probe:ironsht/0.1.0/delegation_map_v/&DelegationMap<K>#DelegationMap<usize>#all_keys_agree()",
    "probe:ironsht/0.1.0/delegation_map_v/&DelegationMap<K>#DelegationMap<usize>#almost_all_keys_agree()",
    "probe:ironsht/0.1.0/delegation_map_v/&DelegationMap<SHTKey>#DelegationMap<&KeyIterator<AbstractKey>>#delegate_for_key_range_is_host_impl()",
    "probe:ironsht/0.1.0/delegation_map_v/&KeyIterator<K>#KeyIterator<&Self>#lt()",
    "probe:ironsht/0.1.0/delegation_map_v/&KeyIterator<K>#KeyIterator<K>#above()",
    "probe:ironsht/0.1.0/delegation_map_v/&KeyIterator<K>#KeyIterator<K>#get()",
    "probe:ironsht/0.1.0/delegation_map_v/&KeyIterator<K>#KeyIterator<bool>#is_end()",
    "probe:ironsht/0.1.0/delegation_map_v/&StrictlyOrderedMap<K>#StrictlyOrderedMap<&K>#find_key()",
    "probe:ironsht/0.1.0/delegation_map_v/&StrictlyOrderedMap<K>#StrictlyOrderedMap<&K>#get()",
    "probe:ironsht/0.1.0/delegation_map_v/&StrictlyOrderedMap<K>#StrictlyOrderedMap<&KeyIterator<K>>#greatest_lower_bound()",
    "probe:ironsht/0.1.0/delegation_map_v/&StrictlyOrderedMap<K>#StrictlyOrderedMap<&KeyIterator<K>>#greatest_lower_bound_index()",
    "probe:ironsht/0.1.0/delegation_map_v/&StrictlyOrderedMap<K>#StrictlyOrderedMap<usize>#keys_in_index_range_agree()",
    "probe:ironsht/0.1.0/delegation_map_v/&StrictlyOrderedMap<K>#StrictlyOrderedMap<usize>#values_agree()",
    "probe:ironsht/0.1.0/delegation_map_v/&StrictlyOrderedVec<K>#StrictlyOrderedVec<usize>#index()",
    "probe:ironsht/0.1.0/delegation_map_v/&StrictlyOrderedVec<K>#StrictlyOrderedVec<usize>#len()",
    "probe:ironsht/0.1.0/delegation_map_v/&mut/DelegationMap<K>#DelegationMap<&KeyIterator<K>>#set()",
    "probe:ironsht/0.1.0/delegation_map_v/&mut/StrictlyOrderedMap<K>#StrictlyOrderedMap<&KeyIterator<K>>#erase()",
    "probe:ironsht/0.1.0/delegation_map_v/&mut/StrictlyOrderedMap<K>#StrictlyOrderedMap<K>#set()",
    "probe:ironsht/0.1.0/delegation_map_v/&mut/StrictlyOrderedVec<K>#StrictlyOrderedVec<K>#insert()",
    "probe:ironsht/0.1.0/delegation_map_v/&mut/StrictlyOrderedVec<K>#StrictlyOrderedVec<usize>#erase()",
    "probe:ironsht/0.1.0/delegation_map_v/&mut/StrictlyOrderedVec<K>#StrictlyOrderedVec<usize>#remove()",
    "probe:ironsht/0.1.0/delegation_map_v/&mut/StrictlyOrderedVec<K>#StrictlyOrderedVec<usize>#set()",
    "probe:ironsht/0.1.0/delegation_map_v/DelegationMap<ID>#new()",
    "probe:ironsht/0.1.0/delegation_map_v/DelegationMap<K>#DelegationMap<&KeyIterator<K>>#extend_range_consistent()",
    "probe:ironsht/0.1.0/delegation_map_v/DelegationMap<K>#DelegationMap<&KeyIterator<K>>#not_range_consistent()",
    "probe:ironsht/0.1.0/delegation_map_v/DelegationMap<K>#DelegationMap<&KeyIterator<K>>#range_consistent_subset()",
    "probe:ironsht/0.1.0/delegation_map_v/DelegationMap<Self>#lemma_set_is_update()",
    "probe:ironsht/0.1.0/delegation_map_v/KeyIterator#end()",
    "probe:ironsht/0.1.0/delegation_map_v/KeyIterator<K>#new()",
    "probe:ironsht/0.1.0/delegation_map_v/Ordering#Ordering<bool>#is_eq()",
    "probe:ironsht/0.1.0/delegation_map_v/Ordering#Ordering<bool>#is_ge()",
    "probe:ironsht/0.1.0/delegation_map_v/Ordering#Ordering<bool>#is_gt()",
    "probe:ironsht/0.1.0/delegation_map_v/Ordering#Ordering<bool>#is_le()",
    "probe:ironsht/0.1.0/delegation_map_v/Ordering#Ordering<bool>#is_lt()",
    "probe:ironsht/0.1.0/delegation_map_v/Ordering#Ordering<bool>#is_ne()",
    "probe:ironsht/0.1.0/delegation_map_v/StrictlyOrderedMap#new()",
    "probe:ironsht/0.1.0/delegation_map_v/StrictlyOrderedMap<K>#StrictlyOrderedMap#mind_the_gap()",
    "probe:ironsht/0.1.0/delegation_map_v/StrictlyOrderedMap<K>#StrictlyOrderedMap<KeyIterator<K>>#choose_gap_violator()",
    "probe:ironsht/0.1.0/delegation_map_v/StrictlyOrderedMap<K>#StrictlyOrderedMap<KeyIterator<K>>#gap_means_empty()",
    "probe:ironsht/0.1.0/delegation_map_v/StrictlyOrderedVec#new()",
    "probe:ironsht/0.1.0/delegation_map_v/StrictlyOrderedVec<K>#StrictlyOrderedVec<Set<K>>#to_set()",
    "probe:ironsht/0.1.0/delegation_map_v/vec_erase()",
    "probe:ironsht/0.1.0/endpoint_hashmap_t/&HashMap<V>#HashMap<&EndPoint>#get()",
    "probe:ironsht/0.1.0/endpoint_hashmap_t/&HashMap<V>#HashMap<Vec<EndPoint>>#keys()",
    "probe:ironsht/0.1.0/endpoint_hashmap_t/&mut/HashMap<V>#HashMap<&EndPoint>#insert()",
    "probe:ironsht/0.1.0/endpoint_hashmap_t/&mut/HashMap<V>#HashMap<&EndPoint>#put()",
    "probe:ironsht/0.1.0/endpoint_hashmap_t/&mut/HashMap<V>#HashMap<&EndPoint>#swap()",
    "probe:ironsht/0.1.0/endpoint_hashmap_t/HashMap#new()",
    "probe:ironsht/0.1.0/hashmap_t/&CKeyHashMap#CKeyHashMap#clone_up_to_view()",
    "probe:ironsht/0.1.0/hashmap_t/&CKeyHashMap#CKeyHashMap<&CKey>#get()",
    "probe:ironsht/0.1.0/hashmap_t/&CKeyHashMap#CKeyHashMap<F>#filter()",
    "probe:ironsht/0.1.0/hashmap_t/&CKeyHashMap#CKeyHashMap<Vec<CKeyKV>>#to_vec()",
    "probe:ironsht/0.1.0/hashmap_t/&CKeyHashMap#CKeyHashMap<bool>#valid()",
    "probe:ironsht/0.1.0/hashmap_t/&mut/CKeyHashMap#CKeyHashMap<&CKey>#remove()",
    "probe:ironsht/0.1.0/hashmap_t/&mut/CKeyHashMap#CKeyHashMap<&KeyRange<CKey>>#bulk_remove()",
    "probe:ironsht/0.1.0/hashmap_t/&mut/CKeyHashMap#CKeyHashMap<&KeyRange<CKey>>#bulk_update()",
    "probe:ironsht/0.1.0/hashmap_t/&mut/CKeyHashMap#CKeyHashMap<CKey>#insert()",
    "probe:ironsht/0.1.0/hashmap_t/CKeyHashMap<CKeyHashMap>#new()",
    "probe:ironsht/0.1.0/hashmap_t/CKeyHashMap<Vec<CKeyKV>>#from_vec()",
    "probe:ironsht/0.1.0/hashmap_t/CKeyHashMap<Vec<CKeyKV>>#lemma_from_vec()",
    "probe:ironsht/0.1.0/hashmap_t/lemma_to_vec()",
    "probe:ironsht/0.1.0/hashmap_t/lemma_to_vec_view()",
    "probe:ironsht/0.1.0/host_impl_t/&mut/HostState#HostState<&NetClient>#next_impl()",
    "probe:ironsht/0.1.0/host_impl_t/HostState<&Args>#init_impl()",
    "probe:ironsht/0.1.0/host_impl_v/&HostState#HostState<&NetClient>#deliver_outbound_packets()",
    "probe:ironsht/0.1.0/host_impl_v/&HostState#HostState<&NetClient>#deliver_packet_seq()",
    "probe:ironsht/0.1.0/host_impl_v/&HostState#HostState<bool>#should_process_received_message_impl()",
    "probe:ironsht/0.1.0/host_impl_v/&mut/HostState#HostState<&NetClient>#host_next_receive_packet()",
    "probe:ironsht/0.1.0/host_impl_v/&mut/HostState#HostState<&NetClient>#host_noreceive_noclock_next()",
    "probe:ironsht/0.1.0/host_impl_v/&mut/HostState#HostState<&NetClient>#process_received_packet_next_impl()",
    "probe:ironsht/0.1.0/host_impl_v/&mut/HostState#HostState<&NetClient>#real_next_impl()",
    "probe:ironsht/0.1.0/host_impl_v/&mut/HostState#HostState<&NetClient>#receive_packet_next()",
    "probe:ironsht/0.1.0/host_impl_v/&mut/HostState#HostState<CPacket>#host_model_receive_packet()",
    "probe:ironsht/0.1.0/host_impl_v/&mut/HostState#HostState<Vec<CPacket>>#host_model_next_delegate()",
    "probe:ironsht/0.1.0/host_impl_v/&mut/HostState#HostState<Vec<CPacket>>#host_model_next_get_request()",
    "probe:ironsht/0.1.0/host_impl_v/&mut/HostState#HostState<Vec<CPacket>>#host_model_next_receive_message()",
    "probe:ironsht/0.1.0/host_impl_v/&mut/HostState#HostState<Vec<CPacket>>#host_model_next_set_request()",
    "probe:ironsht/0.1.0/host_impl_v/&mut/HostState#HostState<Vec<CPacket>>#host_model_next_shard()",
    "probe:ironsht/0.1.0/host_impl_v/HostState<&Arg>#parse_end_point()",
    "probe:ironsht/0.1.0/host_impl_v/HostState<&Args>#parse_end_points()",
    "probe:ironsht/0.1.0/host_impl_v/HostState<&Args>#real_init_impl()",
    "probe:ironsht/0.1.0/host_impl_v/HostState<CKeyHashMap>#effect_of_hashmap_bulk_update()",
    "probe:ironsht/0.1.0/host_impl_v/HostState<DelegationMap<CKey>>#effect_of_delegation_map_set()",
    "probe:ironsht/0.1.0/host_impl_v/HostState<EndPoint>#parse_command_line_configuration()",
    "probe:ironsht/0.1.0/host_impl_v/HostState<EventResults>#empty_event_results()",
    "probe:ironsht/0.1.0/host_impl_v/Parameters<Parameters>#static_params()",
    "probe:ironsht/0.1.0/host_impl_v/extract_range_impl()",
    "probe:ironsht/0.1.0/host_impl_v/make_empty_event_results()",
    "probe:ironsht/0.1.0/host_impl_v/make_send_only_event_results()",
    "probe:ironsht/0.1.0/host_protocol_t/workaround_dermarshal_not_invertible()",
    "probe:ironsht/0.1.0/io_t/&EndPoint#EndPoint<EndPoint>#clone_up_to_view()",
    "probe:ironsht/0.1.0/io_t/&EndPoint#EndPoint<bool>#valid_physical_address()",
    "probe:ironsht/0.1.0/io_t/&NetClient#NetClient<EndPoint>#get_my_end_point()",
    "probe:ironsht/0.1.0/io_t/&NetClient#NetClient<u64>#get_time_internal()",
    "probe:ironsht/0.1.0/io_t/&mut/NetClient#NetClient#reset()",
    "probe:ironsht/0.1.0/io_t/&mut/NetClient#NetClient<&EndPoint>#send()",
    "probe:ironsht/0.1.0/io_t/&mut/NetClient#NetClient<&EndPoint>#send_internal_wrapper()",
    "probe:ironsht/0.1.0/io_t/&mut/NetClient#NetClient<i32>#receive()",
    "probe:ironsht/0.1.0/io_t/&mut/NetClient#NetClient<u64>#get_time()",
    "probe:ironsht/0.1.0/io_t/NetClient<extern/\"C\"/fn(>#new()",
    "probe:ironsht/0.1.0/keys_t/&KeyRange<K>#KeyRange<&K>#contains_exec()",
    "probe:ironsht/0.1.0/keys_t/&SHTKey#SHTKey<SHTKey>#clone()",
    "probe:ironsht/0.1.0/keys_t/KeyTrait#cmp_properties()",
    "probe:ironsht/0.1.0/keys_t/KeyTrait#zero()",
    "probe:ironsht/0.1.0/keys_t/KeyTrait#zero_properties()",
    "probe:ironsht/0.1.0/keys_t/cmp()",
    "probe:ironsht/0.1.0/main_t/sht_main()",
    "probe:ironsht/0.1.0/marshal_ironsht_specific_v/EndPoint#view_equal_spec()",
    "probe:ironsht/0.1.0/marshal_ironsht_specific_v/SHTKey#view_equal_spec()",
    "probe:ironsht/0.1.0/marshal_ironsht_specific_v/ckeyhashmap_max_serialized_size_exec()",
    "probe:ironsht/0.1.0/marshal_ironsht_specific_v/lemma_is_marshalable_CKeyHashMap()",
    "probe:ironsht/0.1.0/marshal_ironsht_specific_v/sorted_keys()",
    "probe:ironsht/0.1.0/marshal_v/&Self#Marshalable<&Self>#lemma_same_views_serialize_the_same()",
    "probe:ironsht/0.1.0/marshal_v/&Self#Marshalable<&Self>#lemma_serialization_is_not_a_prefix_of()",
    "probe:ironsht/0.1.0/marshal_v/&Self#Marshalable<&Self>#lemma_serialize_injective()",
    "probe:ironsht/0.1.0/marshal_v/&Self#Marshalable<&Self>#lemma_view_equal_symmetric()",
    "probe:ironsht/0.1.0/marshal_v/&Self#Marshalable<&Vec<u8>>#serialize()",
    "probe:ironsht/0.1.0/marshal_v/&Self#Marshalable<bool>#_is_marshalable()",
    "probe:ironsht/0.1.0/marshal_v/&Self#Marshalable<usize>#serialized_size()",
    "probe:ironsht/0.1.0/marshal_v/Marshalable<usize>#deserialize()@49",
    "probe:ironsht/0.1.0/net_sht_v/receive_with_demarshal()",
    "probe:ironsht/0.1.0/net_sht_v/send_packet()",
    "probe:ironsht/0.1.0/net_sht_v/send_packet_seq()",
    "probe:ironsht/0.1.0/net_sht_v/sht_demarshall_data_method()",
    "probe:ironsht/0.1.0/net_sht_v/sht_marshal_data_injective()",
    "probe:ironsht/0.1.0/seq_is_unique_v/clone_end_point()",
    "probe:ironsht/0.1.0/seq_is_unique_v/clone_option_end_point()",
    "probe:ironsht/0.1.0/seq_is_unique_v/clone_option_vec_u8()",
    "probe:ironsht/0.1.0/seq_is_unique_v/do_end_points_match()",
    "probe:ironsht/0.1.0/seq_is_unique_v/do_vec_u8s_match()",
    "probe:ironsht/0.1.0/seq_is_unique_v/endpoints_contain()",
    "probe:ironsht/0.1.0/seq_is_unique_v/singleton_seq_to_set_is_singleton_set()",
    "probe:ironsht/0.1.0/seq_is_unique_v/test_unique()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_filter_skip_rejected()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_fold_left_append_merge()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_fold_left_on_equiv_seqs()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_if_everything_in_seq_satisfies_filter_then_filter_is_identity()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_if_nothing_in_seq_satisfies_filter_then_filter_result_is_empty()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_seq_add_subrange()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_seq_fold_left_append_len_int()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_seq_fold_left_append_len_int_le()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_seq_fold_left_append_right()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_seq_fold_left_merge_right_assoc()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_seq_fold_left_sum_le()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_seq_fold_left_sum_len_int_positive()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_seq_fold_left_sum_right()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/lemma_subrange_subrange()",
    "probe:ironsht/0.1.0/seq_lib_v/verus_extra/some_differing_index_for_unequal_seqs()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/flatten_sets_singleton_auto()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/flatten_sets_spec()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_flatten_set_seq_spec()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_flatten_sets_insert()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_flatten_sets_union()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_flatten_sets_union_auto()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_map_seq_singleton_auto()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_map_set_singleton_auto()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_map_values_singleton_auto()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_seq_map_equiv()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_seq_push_to_set()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_set_map_insert()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_to_set_distributes_over_addition()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_to_set_singleton_auto()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/lemma_to_set_union_auto()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/map_finite()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/map_fold_finite()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/map_fold_ok()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/map_set_finite_auto()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/seq_map_values_concat()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/seq_map_values_concat_auto()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/set_map_union()",
    "probe:ironsht/0.1.0/set_lib_ext_v/verus_extra/set_map_union_auto()",
    "probe:ironsht/0.1.0/single_delivery_model_v/&CSingleDelivery#CSingleDelivery<&CPacket>#maybe_ack_packet_impl()",
    "probe:ironsht/0.1.0/single_delivery_model_v/&CSingleDelivery#CSingleDelivery<&CPacket>#new_impl()",
    "probe:ironsht/0.1.0/single_delivery_model_v/&CSingleDelivery#CSingleDelivery<&EndPoint>#retransmit_un_acked_packets()",
    "probe:ironsht/0.1.0/single_delivery_model_v/&CSingleDelivery#CSingleDelivery<&EndPoint>#retransmit_un_acked_packets_for_dst()",
    "probe:ironsht/0.1.0/single_delivery_model_v/&mut/CSingleDelivery#CSingleDelivery<&CMessage>#send_single_cmessage()",
    "probe:ironsht/0.1.0/single_delivery_model_v/&mut/CSingleDelivery#CSingleDelivery<&CPacket>#receive_ack_impl()",
    "probe:ironsht/0.1.0/single_delivery_model_v/&mut/CSingleDelivery#CSingleDelivery<&CPacket>#receive_impl()",
    "probe:ironsht/0.1.0/single_delivery_model_v/&mut/CSingleDelivery#CSingleDelivery<&CPacket>#receive_real_packet_impl()",
    "probe:ironsht/0.1.0/single_delivery_model_v/same_view_same_marshalable()",
    "probe:ironsht/0.1.0/single_delivery_state_v/&CAckState#CAckState#clone_up_to_view()",
    "probe:ironsht/0.1.0/single_delivery_state_v/&CAckState#CAckState<AbstractEndPoint>#lemma_seqno_in_un_acked_list()",
    "probe:ironsht/0.1.0/single_delivery_state_v/&CSendState#CSendState<&EndPoint>#get()",
    "probe:ironsht/0.1.0/single_delivery_state_v/&CSingleDelivery#CSingleDelivery<AbstractEndPoint>#un_acked_messages_extend()",
    "probe:ironsht/0.1.0/single_delivery_state_v/&CTombstoneTable#CTombstoneTable<&EndPoint>#lookup()",
    "probe:ironsht/0.1.0/single_delivery_state_v/&SingleDelivery<Message>#SingleDelivery<AbstractEndPoint>#lemma_un_acked_messages_for_dests_empty()",
    "probe:ironsht/0.1.0/single_delivery_state_v/&mut/CAckState#CAckState<u64>#truncate()",
    "probe:ironsht/0.1.0/single_delivery_state_v/&mut/CSendState#CSendState<&EndPoint>#cack_state_swap()",
    "probe:ironsht/0.1.0/single_delivery_state_v/&mut/CSendState#CSendState<&EndPoint>#put()",
    "probe:ironsht/0.1.0/single_delivery_state_v/&mut/CTombstoneTable#CTombstoneTable<&EndPoint>#insert()",
    "probe:ironsht/0.1.0/single_delivery_state_v/CAckState<CAckState>#new()",
    "probe:ironsht/0.1.0/single_delivery_state_v/CAckState<int>#abstractify_distributes_over_skip()",
    "probe:ironsht/0.1.0/single_delivery_state_v/CSingleDelivery#empty()",
    "probe:ironsht/0.1.0/verus_extra/clone_v/clone()"
  ],
  "verified_functions_count": 212,
  "verified_functions_missing_atom_record": [],
  "verus_release_tag": "release/0.2026.01.14.88f7396"
}
Our open standard for verification certification

We have designed our VeriLib verification certificates to meet three goals:

  • Transparency: Easy to see precisely what has been verified about what code with what tooling & assumptions
  • Reproducibility: Easy for user to automatically reproduce all certified claims, so no need to trust the issuer of the certificate
  • Usability: Quick and easy to build the desired level of trust:
    • Busy users can choose trust crowdsourcing: simply trusting software with the green checkmark, knowing that if it were fraudulent, someone else would probably have tried to reproduce it, failed, sounded the alarm, and permanently destroyed VeriLib’s credibility.
    • More hardcore users can automatically repeat and inspect the entire verification process on their own machine.

Here is how this works in detail. The green checkmark displayed (at the top of certificate pages such as this one) is not static, but dynamically generated if and only if three hashes stored on the Ethereum blockchain satisfy these properties:

a) The GitHub repo hash matches that of the linked repo (certifying that we’re verifying the right code)

b) The DockerHub container hash matches that of the linked container (certifying that we’re using the right verification tooling)

c) The manifest hash matches that of the displayed manifest (certifying that we’re showing the right verification result)

d) That the manifest shows VerificationSuccess = true

Blockchain commit time — (on-chain timestamp: Ethereum proof)
GitHub / repo hash 08be20c3c35692138b495200ec50d1035666e3a5 (browse tree)
DockerHub / container hash sha256:0583382b6122245cfd7e033f288c30d85fdf8f1933aed48829d85cbecec110fa
Manifest hash 778626bf863e58737a016e180bb10f560528090938aa8c6d1c9b475a96e2bc15 (SHA-256 of published JSON file)

Running the Verify it yourself script (instructions below) checks that applying the verification tooling (b) to the code (a) reproduces the manifest (c).

To save you time, VeriLib has already auto-run this same script, which produces both pedagogical output to the terminal and the result summary file manifest.json.

We encourage you to not only run this tooling, but also inspect it for correctness. You can build trust in this certificate page by checking the text in green against the manifest, and by noting that the manifest lists as successfully verified all functions in the Specifications section.

Verify it yourself

You do not need to clone any repository. Download the small bash script below using wget or curl. Running it pulls the prebuilt image from Docker Hub and writes the same manifests and lists this page publishes. A full run can take a long time and use significant disk space—plan for that before you start.

  1. Get the script with wget (saves as verify.sh in the current directory):
    wget -O verify.sh https://verilib.org/cert/5167/verify-script

    Same URL with curl: curl -fsSL -o verify.sh https://verilib.org/cert/5167/verify-script

  2. bash verify.sh --cert-verify-url 'https://verilib.org' 'verilib/repo-5167@sha256:0583382b6122245cfd7e033f288c30d85fdf8f1933aed48829d85cbecec110fa' 'VERIFICATION_RESULTS'

Once you have finished running the script, the file VERIFICATION_RESULTS/manifest.json should match what is shown in the Results section above (downloadable here).

Install Docker

You need a working Docker install before you can pull the certificate image or run the verification script. For the canonical, up-to-date steps (including licensing and system requirements), use Docker’s official guide: Get Docker.

  • macOS: Install Docker Desktop for Mac (Apple Silicon or Intel per your Mac). Open the app from Applications, complete onboarding, and wait until Docker reports “running”. Detailed steps: Install Docker Desktop on Mac.
  • Windows: Install Docker Desktop for Windows. Use WSL 2 backend when prompted. After install, start Docker Desktop and wait until it is ready. Detailed steps: Install Docker Desktop on Windows.
  • Linux: Install Docker Engine (and optionally Docker Compose plugin) for your distribution—do not rely on a random apt package without checking Docker’s repo instructions. Detailed steps: Install Docker Engine (choose your distro: Ubuntu, Debian, Fedora, etc.).

Smoke test: In a terminal, run docker version. You should see both Client and Server sections. If you see docker: command not found, the CLI is not on your PATH yet—restart the terminal or finish Docker Desktop’s setup.

Reproducible Docker image (open source)

Latest certificate: v1 — /cert/5167 and /cert/5167?p=1&c=v1 pin the image below.

The Docker image verilib/repo-5167@sha256:0583382b6122245cfd7e033f288c30d85fdf8f1933aed48829d85cbecec110fa on Docker Hub matches this certificate’s published dockerHubImageDigest / manifest image. Use Verify it yourself to pull and run—no clone required.