Viper Project

All

86 repositories

gobra-libs
Public
Standard library for the Gobra verifier for Go. Contains definitions and lemmas useful for verifying large projects.
Python
•
MIT License
•2•2•5•2•Updated Feb 22, 2026Feb 22, 2026
gobra-ide
Public
VSCode Plugin for Gobra
TypeScript
•
Other
•4•11•4•1•Updated Feb 22, 2026Feb 22, 2026
tutorial
Public
This repo contains the sources of the official Viper tutorial. Feel free to submit your fixes and additions via pull requests. Please report technical issues vi…
documentation verification formal-methods
JavaScript
•5•0•3•1•Updated Feb 20, 2026Feb 20, 2026
viperserver
Public
HTTP server that manages verification requests to different tools from the Viper tool stack.
verification viper
Scala
•
Other
•16•15•3•6•Updated Feb 20, 2026Feb 20, 2026
gobra
Public
Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
go golang verification
Scala
•
Other
•37•148•152•18•Updated Feb 19, 2026Feb 19, 2026
viper-ide
Public
This is the main repository for the Viper IDE extension for VS Code.
verification viper vscode-extension
TypeScript
•
Mozilla Public License 2.0
•11•12•11•7•Updated Feb 19, 2026Feb 19, 2026
carbon
Public
Verification-condition-generation-based verifier for the Viper intermediate verification language.
verification viper verification-condition-generation
Scala
•
Mozilla Public License 2.0
•23•35•149•10•Updated Feb 19, 2026Feb 19, 2026
silver
Public
Definition of the Viper intermediate verification language.
programming-language verification viper
Scala
•
Mozilla Public License 2.0
•48•95•103•18•Updated Feb 19, 2026Feb 19, 2026
silicon
Public
Symbolic-execution-based verifier for the Viper intermediate verification language.
verification symbolic-execution viper
Scala
•
Mozilla Public License 2.0
•36•127•111•12•Updated Feb 19, 2026Feb 19, 2026
gobra-action
Public
Github Action to verify Go code with Gobra directly in a CI workflow
go golang actions verification formal-verification github-actions
Shell
•
Mozilla Public License 2.0
•3•2•4•2•Updated Feb 17, 2026Feb 17, 2026
vs-verification-toolbox
Public
Useful component to build VS Code extensions for verifiers.
TypeScript
•
Mozilla Public License 2.0
•2•5•0•1•Updated Feb 15, 2026Feb 15, 2026
VerifiedSCION
Public
Verifying the SCION architecture using Gobra
Go
•
Apache License 2.0
•5•11•9•8•Updated Feb 9, 2026Feb 9, 2026
prusti-dev
Public
A static verifier for Rust, based on the Viper verification infrastructure.
rust verification viper formal-verification
Rust
•
Other
•123•1.7k•265•28•Updated Feb 2, 2026Feb 2, 2026
locate-java-home
Public
Locates JAVA_HOME on any platform, and can differentiate between different versions.
TypeScript
•
Other
•9•3•0•3•Updated Feb 2, 2026Feb 2, 2026
check-license-header
Public
GitHub action to check whether all files have a specified copyright license header
TypeScript
•
Other
•2•6•2•1•Updated Feb 1, 2026Feb 1, 2026
prusti-assistant
Public
VS Code extension to verify Rust programs with the Prusti verifier.
rust verification vscode-extension diagnostics prusti
TypeScript
•
MIT License
•9•24•10•6•Updated Feb 1, 2026Feb 1, 2026
create-nightly-release
Public
GitHub action to create a new pre-release and delete old pre-releases created by this action
TypeScript
•
Other
•1•10•0•2•Updated Feb 1, 2026Feb 1, 2026
gobra-book
Public
JavaScript
•3•4•2•0•Updated Jan 25, 2026Jan 25, 2026
silver-sif-extension
Public archive
Extension of the Viper language with modular product programs and information flow specifications
Scala
•
Mozilla Public License 2.0
•1•3•0•1•Updated Jan 23, 2026Jan 23, 2026
ReusableProtocolVerificationLibrary
Public
Go
•0•3•0•0•Updated Jan 14, 2026Jan 14, 2026
diodon-artifact
Public
Artifact for "The Secrets Must Not Flow: Scaling Security Verification to Large Codebases" (S&P '26)
static-analysis implementation tamarin separation-logic protocol-verification symbolic-security automated-verification gobra
Go
•
Apache License 2.0
•0•3•0•2•Updated Jan 1, 2026Jan 1, 2026
smt-scope
Public
SMTscope automatically analyses and visualises SMT solver execution traces.
profiler z3 instantiation smt axiom quantifiers e-matching
Rust
•
Apache License 2.0
•5•58•7•1•Updated Dec 10, 2025Dec 10, 2025
protocol-verification-refinement
Public
Artifact of the paper "Sound Verication of Security Protocols: From Design to Interoperable Implementations"
implementation tamarin separation-logic protocol-verification symbolic-security automated-verification
Haskell
•
Mozilla Public License 2.0
•0•6•0•1•Updated Dec 2, 2025Dec 2, 2025
silicon-fork-peibensteine
Public
Symbolic-execution-based verifier for the Viper intermediate verification language.
Scala
•
Mozilla Public License 2.0
•36•0•0•0•Updated Nov 4, 2025Nov 4, 2025
carbon-fork-peibensteine
Public
Verification-condition-generation-based verifier for the Viper intermediate verification language.
Scala
•
Mozilla Public License 2.0
•23•0•0•0•Updated Nov 4, 2025Nov 4, 2025
silver-fork-peibensteine
Public
Definition of the Viper intermediate verification language.
Scala
•
Mozilla Public License 2.0
•48•0•0•0•Updated Jul 8, 2025Jul 8, 2025
vpr-mode
Public
Viper mode for emacs
Emacs Lisp
•
Mozilla Public License 2.0
•2•2•0•0•Updated Jun 12, 2025Jun 12, 2025
silver-oxide
Public
A Rust parser for Viper
Rust
•
Mozilla Public License 2.0
•0•3•0•0•Updated Apr 14, 2025Apr 14, 2025
gobra-playground
Public
Go
•
Mozilla Public License 2.0
•1•0•0•0•Updated Mar 30, 2025Mar 30, 2025
program-proofs-viper
Public
Examples and exercises from the book Program Proofs translated Viper.
0•1•0•0•Updated Mar 19, 2025Mar 19, 2025