soter/
lib.rs

1//! SMT-backed safety and policy assurance for Converge extensions.
2//!
3//! Soter produces searched evidence. It does not promote facts directly and it
4//! does not turn SMT results into formal proof claims.
5
6pub mod arbiter;
7pub mod backend;
8#[cfg(feature = "cvc5")]
9pub mod cvc5;
10pub mod formation;
11pub mod provenance;
12pub mod suggestor;
13pub mod types;
14
15pub use arbiter::{
16    ArbiterExpenseCommitInvariant, ArbiterExpensePolicyModel,
17    EXPENSE_NON_FINANCE_HIGH_VALUE_COMMIT_INVARIANT_ID,
18};
19pub use backend::{FakeSmtBackend, SmtBackend};
20#[cfg(feature = "cvc5")]
21pub use cvc5::Cvc5FfiBackend;
22pub use formation::{SoterCapability, formation_capabilities};
23pub use provenance::{SOTER_PROVENANCE, Soter};
24pub use suggestor::SmtSuggestor;
25pub use types::{SmtError, SmtEvidenceTier, SmtQuery, SmtReport, SmtStatus};
soter/lib.rs

soter/
lib.rs
