The efficient SMT-based context-bounded model checker (ESBMC)
FailSafe: An autonomous fact-checking framework leveraging Multi-Agent LLMs and Structured Argumentation Graphs (SAG) to verify claims with deep-web retrieval and reasoning.
Artifact of the paper "Sound Verication of Security Protocols: From Design to Interoperable Implementations"
Tamarin Model & Verified Go Implementation of the WireGuard VPN Key Exchange Protocol
Artifact for "The Secrets Must Not Flow: Scaling Security Verification to Large Codebases" (S&P '26)
A different implementation of Decentralized Systems and Blockchain Technologies
Automated formal verification tool for vision classifiers using CLIP embeddings and MILP optimization. Converts OWL ontologies into ConSpec specifications and provides mathematical guarantees about model behavior in safety-critical AI systems.
Certus is a finetuned model that generates machine-checkable correctness certificates for Python functions, plus a checker that verifies them with counterexample search. 83% of certificates survive Hypothesis testing on unseen code.
Add a description, image, and links to the automated-verification topic page so that developers can more easily learn about it.
To associate your repository with the automated-verification topic, visit your repo's landing page and select "manage topics."