-
rustls-platform-verifier
supports verifying TLS certificates in rustls with the operating system verifier
-
vstd
Verus Standard Library: Useful specifications and lemmas for verifying Rust code
-
kani-verifier
A bit-precise model checker for Rust
-
aws-smithy-checksums
Checksum calculation and verification callbacks
-
verus_builtin
Verus Builtins: Rust definitions for core constructs in Verus
-
gba-cli
CLI for GBA (Geektime Bootcamp Agent)
-
cargo-anneal
Formally verify that your safety comments are correct
-
contracts
Design-by-contract attributes
-
rebuilderd
independent build verification daemon
-
sigstore-verify
Sigstore signature verification
-
libcrux-ed25519
Formally verified ed25519 signature library
-
sequoia-sqv
OpenPGP signature verification program
-
cargo-veristat
Cargo subcommand for verifying BPF programs embedded in Rust binaries via veristat
-
captcha-rs
Generate verification images dynamically
-
libcprover_rust
Rust API for CBMC and assorted CProver tools
-
voa
Command line interface and library for interacting with the File Hierarchy for the Verification of OS Artifacts (VOA)
-
pearlite-syn
A syn parser for the Pearlite specification language in Creusot
-
dev-report
Structured, machine-readable reports for AI-assisted Rust development. Foundation schema of the dev-* verification suite.
-
triad-cli
Reference CLI for deterministic claim verification with triad
-
creusot-std
Standard library of Creusot: provides specification macros, contracts for Rust standard library and logic helpers
-
claimcheck
Verify AI agent claims from session transcripts
-
tla-connect
TLA+/Apalache integration for model-based testing
-
depyler
A Python-to-Rust transpiler focusing on energy-efficient, safe code generation with progressive verification
-
labscript
Prescription PDF generator with e-signature and QR verification
-
retrospector
Retro game ROM checksum verifier and metadata extractor
-
cargo-hermes
Formally verify that your safety comments are correct
-
ratify
signing and verifying files and directories
-
realitydefender
Reality Defender SDK for Rust - Tools for detecting deepfakes and manipulated media
-
nomograph-kit
Verified tool registry manager -- manages developer toolchains from git-based registries
-
fastbreak
A formal methods-inspired specification language combining Alloy, TLA+, Cucumber, and Design by Contract
-
passless-core
Core types and configuration for Passless
-
ferrify
governed Rust software-change platform with typed policy, bounded planning, and evidence-backed reporting
-
ans-verify
ANS Trust Verification library for the Agent Name Service
-
vest
DSL for specifying and generating fast, formally verified parsers and serializers
-
filepack
file verification utility
-
r2u2_core
R2U2: A stream-based runtime monitor in no_std
-
sourceright
Reference verification infrastructure for academic and legal citation workflows
-
provable-contracts
Papers to Math to Contracts in Code — YAML contract parsing, validation, scaffold generation, and Kani harness codegen for provable Rust kernels
-
oxirag
A four-layer RAG engine with SMT-based logic verification and knowledge graph support
-
pg_ecdsa_verify
A PostgreSQL extension for ECDSA signature verification
-
ritalin
Executive function for AI coding agents. Focus their intelligence, ground their work, stop the avoidable mistakes.
-
libverify-github
GitHub connector for libverify SDLC verification
-
legalis
Command-line interface for Legalis-RS
-
ravencheck
Decidable verification of Rust code using relational abstraction
-
voa-openpgp
using OpenPGP verifiers in VOA
-
wire-check
Verify newly added Rust code is actually integrated — dead code ratchet, cross-reference checks, and more
-
crev-data
Scalable, social, Code REView system that we desperately need - data types library
-
iso-probe
Runtime ISO discovery for rescue environments (loopback mount + GPT/ISO9660 + sha256/minisign sidecar verification)
-
entrouter-universal
Pipeline integrity guardian - what goes in, comes out identical
-
dev-fixtures
Repeatable test environments, sample data, and controlled inputs. Part of the dev-* verification suite.
-
bcl-secunit
secunit binary — agent helper for registry inspection, run orchestration, and capture
-
quint-connect
A model-based testing framework that connects Quint specifications with Rust applications
-
dev-coverage
Test coverage measurement and regression detection for Rust. Wraps cargo-llvm-cov. Part of the dev-* verification suite.
-
fastpasta
CLI for verifying or examining readout data from the ALICE detector
-
libverify-output
Output formatters (SARIF, JSON, Matrix, Vanta) for libverify verification results
-
tla-rs
IronFleet verified distributed systems framework
-
polysub
fast substitution of variables in polynomials
-
ssi-vc
Verifiable Credentials Data Model v1.1 for the
ssilibrary -
vertrule-schemas
Canonical schema types for the VertRule constitutional layer
-
hooksniff
Official Rust client for the HookSniff webhook delivery service
-
hibp-verifier
High-performance library for checking passwords against the Have I Been Pwned breach database using binary search on sha1t48 format
-
oxo-license
Generic dual-license runtime verification library for Traitome projects
-
r2u2_cli
R2U2 CLI: A stream-based runtime monitor command-line interface
-
mise-sigstore
Sigstore verification helpers for mise
-
xldenis/creusot
prove your code is correct in an automated fashion
-
traceforge
model checker for concurrent and distributed programs written in Rust
-
depyler-analysis
Analysis, type inference, and optimization passes for the Depyler transpiler
-
check_build
verify a VCF file against hg19 and hg38 references using a streaming, low-memory approach
-
sit-rs
Rust-native extraction for StuffIt Expander archive files
-
depyler-tooling
IDE, debugging, documentation, and tooling support for the Depyler transpiler
-
smc_scan
Statistical model checker for large concurrent systems
-
rumpsteak-lean-bridge
Lean verification bridge for Rumpsteak session types
-
philiprehberger-webhook-signature
HMAC-SHA256 webhook signing and verification for Rust
-
relentless-identity
Official Rust SDK for the Relentless Identity API — email Finder and Probe verification workflows
-
elicitation_kani
Kani model-checking proofs for elicitation contract types
-
coda-core
Core execution engine for CODA — orchestrates AI-driven feature development workflows
-
voa-config
configuration of technology backends in VOA
-
atrg-email
SMTP email and OTP verification for at-rust-go
-
authia
High-performance JWT verification library for Ed25519 using WebAssembly
-
alloyiser
Extract formal models from OpenAPI specs and database schemas, check invariants with Alloy
-
ruvix-proof
Proof engine with 3-tier routing for the RuVix Cognition Kernel (ADR-087)
-
open-agent-id
Rust SDK for Open Agent ID — sign, verify, and manage AI agent identities
-
taco-cli
The Threshold Automata for COnsensus Model Checker (TACO) is a tool to verify distributed algorithms that can be modeled using threshold automata
-
philharmonic-connector-service
Service framework for per-realm Philharmonic connector binaries: token verification, payload decryption, Implementation-trait registry and dispatch
-
depyler-lambda
AWS Lambda transpilation support for the Depyler Python-to-Rust transpiler
-
depyler-annotations
Annotation parsing and processing for Depyler
-
rtlola-interpreter
An interpreter for RTLola specifications
-
cognito-jwt-verify
JWT verification library for AWS Cognito tokens and any OIDC-compatible IDP
-
depyler-hir
High-level Intermediate Representation types for the Depyler transpiler
-
prismulti
A multi-threaded Rust implementation of a subset of the PRISM model checker
-
doc-drift
Catch when your markdown docs drift from your Rust source code
-
jwt-verify
JWT verification library for AWS Cognito tokens and any OIDC-compatible IDP
-
hessra-ffi
C FFI bindings for Hessra token verification and configuration
-
libverify-gitlab
GitLab connector for libverify SDLC verification
-
supersigil
CLI tool for spec-driven software development with AI agents
-
uor-prism
Prism standard library (wiki ADR-031): a façade re-exporting uor-foundation's substrate plus the Layer-3 sub-crates (prism-crypto, prism-numerics, prism-tensor, prism-fhe) that contribute…
-
aprender-contracts
Papers to Math to Contracts in Code — YAML contract parsing, validation, scaffold generation, and Kani harness codegen for provable Rust kernels
-
vera-effects
VERA (Verified Effect-Rule Architecture) — generic trace, rule output, and reaction types for building verifiable game loops where every state mutation is inspectable and testable
-
rtlola-cli
A CLI interface for the RTLola interpreter
-
ferrify-application
Ferrify orchestration for intake, planning, verification, and reporting
-
signedshot-validator
Validator for SignedShot media authenticity proofs
-
depyler-verify
Property verification and formal methods for Depyler transpilation
-
clerk-report
Verification of attested YAXI system versions
-
francis
Log-based hypothesis verifier. Declares ordered predictions about log events and verifies them against Loki within timeout windows.
-
otp_offline
offline verification of YubiKey OTPs
-
warp-types-smt
Phase-typed SMT solver for QF_EUF with compile-time phase ordering, built on warp-types-sat
-
why3
Why3 AST and pretty printers
-
doksnet
A CLI tool for documentation-code mapping verification using cryptographic hashes
-
supersigil-evidence
Language-agnostic evidence types for supersigil ecosystem plugins
-
amari-flynn
Probabilistic contracts and verification - named after Kevin Flynn's acceptance of spontaneous perfection
-
boltffi_verify
Static analysis and verification for BoltFFI generated bindings
-
releasor
A CLI that automates release tasks for Rust 🦀 projects, streamlining builds, .tar.gz packaging, and binary verification for a fast and consistent workflow
-
northroot-proof-engine
Core proof computation and validation library for PoSH (Proof of Shape) and PoX (Proof of Execution)
-
depyler-quality
Quality gates and metrics for Depyler
-
ruvector-verified-wasm
WASM bindings for ruvector-verified: proof-carrying vector operations in the browser
-
libverify-vanta
Vanta compliance platform adapter for libverify verification results
-
route_verification
Parse RPSL in the IRR to verify observed BGP routes
-
fdkey
verification primitives for MCP servers and HTTP backends — gate AI-agent access behind LLM-only puzzles
-
ferrify-infra
Ferrify runtime infrastructure for verification, sandboxing, and tool brokering
-
oxiz-proof
Proof generation and checking for OxiZ SMT solver
-
rustls-dangerous
A dangerous implementation of ServerCertVerifier for rustls that disables all certificate validation. WARNING: Development and testing only!
-
forever-ago
Nightly tar.gz backups of a directory with SHA-256 verification and retention pruning
-
flux-verify-api
Natural Language Verification API — prove or disprove claims with mathematical traces
-
oxiz-spacer
Property Directed Reachability (PDR/IC3) engine for OxiZ - Horn clause solving
-
taco-threshold-automaton
defining basic types for threshold automata and all of its building blocks. This crate is part of the TACO toolsuite.
-
supersigil-parser
Parsing pipeline for supersigil Markdown spec documents
-
bertie
Minimal TLS 1.3 implementation
-
trame
Formally verified partial value construction for facet
-
ed25519_heapless
Ed25519 signature verification, generic over bigint backends
-
vwh
Cryptographic accountability tool for verifying digital presence
-
vex-core
Core types for VEX: Agent, ContextPacket, MerkleNode, Evolution
-
logicpearl-verify
Solver-backed verification helpers for LogicPearl discovery and conformance
-
anodized-logic
embed non-trivial elements of logic into Rust code
-
kizzasi-logic
TensorLogic bridge for Kizzasi - constraint enforcement and safety guardrails
-
libcrux-rsa
Formally verified RSA signature library
-
moltbook-cli
CLI for Moltbook - the social network for AI agents
-
elicit_ui
Typestate-based verified UI system using AccessKit as universal IR
-
oximedia-archive
Media archive verification and long-term preservation system
-
redoubt-util
Memory utilities for verification and testing
-
licverify
Rust client for go-license verification system
-
did-you-actually-do-that
A verification framework for validating claimed AI actions against actual outcomes
-
warp-types-bmc
Phase-typed bounded model checker with compile-time depth tracking, built on warp-types-sat
-
aimds-core
Core types and abstractions for AI Manipulation Defense System (AIMDS)
-
cvlr-log
Logging in Certora Calltrace
-
depyler-mcp
Model Context Protocol integration for Depyler
-
cylinder
high-level cryptographic signing library
-
taco-model-checker
Model Checker interface and specification definitions for model checkers that are part of the TACO toolsuite
-
telltale-bridge
Lean verification bridge for Telltale session types
-
hush-cli
Command-line interface for clawdstrike
-
taco-smt-encoder
defining the SMT encodings of threshold automata components into SMT. This crate is part of the TACO toolsuite.
-
qssm-le
lattice engine facade (reference stub — not LaBRADOR)
-
pulith-verify
Content verification primitives for downloaded artifacts
-
proven
Safe, formally verified library for math, crypto, parsing, validation, and ML - Rust bindings
-
eth-id
Zero-Knowledge Document Verification CLI and Library
-
taco-parser
containing parsers to parse threshold automata and ELTL specifications from ByMC and TLA+ specification files. This crate is part of the TACO toolsuite.
-
taco-acs-model-checker
Model Checker constructing an abstract counter system to verify threshold automata. This model checker is part of the TACO toolsuite.
-
taco-interval-ta
allowing you to obtain a threshold automaton with an (symbolic) interval abstraction applied to it. This crate is part of the TACO toolsuite.
-
taco-bdd
A Binary Decision Diagram (BDD) crate that provides a unified interface for the CUDD and OxiDD BDD libraries. This crate is part of the TACO toolsuite.
-
taco-zcs-model-checker
Model Checker constructing an abstract counter system encoded into BDDs to verify threshold automata. This model checker is part of the TACO toolsuite.
-
logicpearl-render
Rendering helpers for LogicPearl artifacts and verification status
-
oxdl
Asynchronous downloader with progress bars and SHA256 verification
-
anodized-fmt
Formatter for #[spec] annotations in Anodized
-
kontroli
Type checking for the lambda-Pi calculus modulo rewriting
-
sigmate
A modern, developer-focused CLI for cryptographic file signing and verification
-
vex-protocol-cli
Command-line interface for VEX - verified AI agent tooling
-
supersigil-verify
Verification engine for supersigil spec documents
-
sql-composer-sqlx
sqlx integration for sql-composer: verify composed SQL against a database
-
taco-smt-model-checker
Model Checker encoding threshold automaton and a property into a single SMT query. This model checker is part of the TACO toolsuite.
-
rajac-verification
OpenJDK compatibility verification runner for rajac
-
pave
PAVED documentation tool - structured docs optimized for AI agents
-
torg-verify
Formal verification for TØR-G boolean circuits
-
checksums
making/verifying checksums of directory trees
-
supersigil-rust
Rust ecosystem plugin for the supersigil verification framework
-
taco-display-utils
A small helper crate for displaying iterators. This crate is part of the TACO toolsuite.
-
trame-runtime
Runtime traits and implementations for trame
-
rtlola-frontend
A frontend for the RTLola runtime verification framework
-
haima-outcome
Outcome-based pricing engine — automated verification, SLA monitoring, and billing orchestration
-
vcd_io
VCD IO utils
-
telltale-lean-bridge
Lean verification bridge for Telltale session types
-
idprova-verify
IDProva verification utilities — DAT and receipt log verification
-
oasert
verifying in-flight requests against a provided OpenAPI 3.1.x or 3.0.x specification
-
cvlr-fixed
Fixed point numbers over Certora native integers
-
veriwasm
A safety verifier for native-compiled WebAssembly code
-
smc_scan_jani
JANI frontend for the Scan model checker
-
smc_scan_promela
Promela frontend for the Scan model checker
-
depyler-analyzer
Static analysis and optimization engine for Depyler
-
flux-provenance
Merkle provenance service for fleet verification traces
-
supersigil-import
Import and convert external spec formats into supersigil documents
-
supersigil-lsp
Language Server Protocol implementation for supersigil spec documents
-
lexicon-gates
Verification gate runners and policy enforcement for lexicon
-
teepot-tee-quote-verification-rs
Fork of intel-tee-quote-verification-rs
-
oxalslien
ALIEN-inspired claim verification and finality probability simulator
-
aliyun-dypns
Rust SDK for Alibaba Cloud Phone Number Verification Service (DYPNS)
-
firebase-verifyid
Dead simple verification of firebase auth id tokens
-
rem-verification
Verification tool for the REM toolchain. Built to be implemented into the VSCode extension for REM. Relies on AENEAS and CoQ
-
ccheck
CLI that verifies the presence of commands inside containers
-
openhawk-verify
Agent claim verification engine — wraps claimcheck for OpenHawk sessions
-
route_verification_rib_stats
Parse RPSL in the IRR to verify observed BGP routes
-
contracts-try
Design-by-contract attributes
-
route_verification_irr
Parse RPSL in the IRR to verify observed BGP routes
-
cvlr-decimal
Decimal numbers over Certora native integers
-
route_verification_ir
Parse RPSL in the IRR to verify observed BGP routes
-
alice_protocol_reader
Reader library for reading raw binary data from the ALICE detector into a convenient structure for implementing analysis
-
cvlr-spec
Specification and Logic primitives for CVLR
-
ecdsa_verify
ECDSA signature verification
-
rtlola-hir
A high-level intermediate representation for RTLola specifications
-
stormdl-integrity
BLAKE3 incremental hashing and content verification
-
route_verification_lex
Parse RPSL in the IRR to verify observed BGP routes
-
verified-graphs
Graphs verified from first principles in Verus
-
route_verification_parse
Parse RPSL in the IRR to verify observed BGP routes
-
lincheck
A linearizability checker for concurrent data structures
-
cm-email-webhook-verification
SDK for verifying CM Email webhook signatures
-
multiple_choice
proc-macro library that verifies function results through multiple executions
-
leptix-otp-field
Leptix One-Time Password Field — a multi-segment input for OTP verification
-
nnv-rs
Verification and Statistics on Deep Neural Networks
-
lazarus-receipts
Lazarus Receipts SDK - Cryptographic receipt verification
-
route_verification_shared_struct
Parse RPSL in the IRR to verify observed BGP routes
-
faf-core
Fiduciary Agent Framework - Core protocol types and traits
-
stimmgabel
polyproto reference test implementation used for verifying other implementations of the protocol
-
route_verification_bgpmap
Parse RPSL in the IRR to verify observed BGP routes
-
smc_scan_scxml
SCXML frontend for the Scan model checker
-
auths-transparency
Append-only transparency log types, Merkle math, and tile storage for Auths
-
rtlola-parser
A parser for RTLola specifications
-
route_verification_io
Parse RPSL in the IRR to verify observed BGP routes
-
secunit-core
Registry, evidence, hashing, and verification primitives for secunit
-
route_verification_common_regex
Parse RPSL in the IRR to verify observed BGP routes
-
intel-tee-quote-verification-rs
Intel(R) TEE Quote Verification Rust Library
-
rtlola-streamir
A framework for the compilation of stream-based languages through an intermediate representation
-
route_verification_bgp
Parse RPSL in the IRR to verify observed BGP routes
-
vex-verify
Lightweight cryptographic verification engine for the VEX protocol
-
ssi-claims-core
Core types and traits for Verifiable Claims in the
ssilibrary -
ruma-zk-verifier
Lightweight verifier for matrix servers (crate or bin) and web clients (wasm)
-
cairn-drift
Staleness detection, drift verification, and contradiction finding
-
rtlola-io-plugins
Input and ouput plugins to be used in the various frontends of the interpreter
-
anodized-core
Core interoperability for the Anodized specification system
-
route_verification_as_path_regex
Parse RPSL in the IRR to verify observed BGP routes
-
recaptcha
response verification
-
qwed
Rust SDK for QWED Verification Protocol
Try searching with DuckDuckGo.