latticearc 0.6.2

Production-ready post-quantum cryptography. Hybrid ML-KEM+X25519 by default, all 4 NIST standards (FIPS 203–206), post-quantum TLS, and FIPS 140-3 backend — one crate, zero unsafe.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

//! Formal Verification for Prelude Utilities
//!
//! This module provides formal verification capabilities for critical utility functions.
//! Kani formal verification proofs are available in the LatticeArc crate.
//!
//! # Usage
//!
//! To run formal verification:
//! ```bash
//! cargo kani --package latticearc
//! ```
//!
//! # Requirements
//!
//! - Kani model checker must be installed: `cargo install kani-verifier`
//! - Only supported on Linux x86_64 and macOS aarch64

#![deny(unsafe_code)]
#![deny(missing_docs)]
#![deny(clippy::unwrap_used)]
#![deny(clippy::panic)]

/// Logs instructions for running formal verification.
///
/// This function provides guidance on using the Kani model checker
/// for formal verification of cryptographic operations.
///
/// # Example
///
/// ```rust
/// use latticearc::prelude::formal_verification::run_formal_verification;
///
/// run_formal_verification();
/// ```
pub fn run_formal_verification() {
    tracing::info!("Formal verification requires Kani model checker");
    tracing::info!("Install with: cargo install kani-verifier");
    tracing::info!("Run verification with: cargo kani --package latticearc");
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_run_formal_verification_succeeds() {
        // Verify the function executes without panic
        run_formal_verification();
    }
}