Skip to content

@viperproject Viper Project

Change the repository type filter

All

    Repositories list

    82 repositories

    • gobra-ide

      Public
      VSCode Plugin for Gobra
      TypeScript
      •
      Other
      •3•10•3•0•Updated Apr 7, 2025Apr 7, 2025

    • viperserver

      Public
      HTTP server that manages verification requests to different tools from the Viper tool stack.
      verificationviper
      Scala
      •
      Other
      •17•10•3•7•Updated Apr 7, 2025Apr 7, 2025

    • gobra-book

      Public
      JavaScript
      •1•2•1•0•Updated Apr 7, 2025Apr 7, 2025

    • viper-ide

      Public
      This is the main repository for the Viper IDE extension for VS Code.
      verificationvipervscode-extension
      TypeScript
      •
      Mozilla Public License 2.0
      •11•10•15•12•Updated Apr 7, 2025Apr 7, 2025

    • pcg

      Public
      Rust
      •5•2•7•2•Updated Apr 7, 2025Apr 7, 2025

    • silicon

      Public
      Symbolic-execution-based verifier for the Viper intermediate verification language.
      verificationsymbolic-executionviper
      Scala
      •
      Mozilla Public License 2.0
      •37•97•114•11•Updated Apr 4, 2025Apr 4, 2025

    • carbon

      Public
      Verification-condition-generation-based verifier for the Viper intermediate verification language.
      verificationviperverification-condition-generation
      Scala
      •
      Mozilla Public License 2.0
      •23•30•143•7•Updated Apr 4, 2025Apr 4, 2025

    • silver

      Public
      Definition of the Viper intermediate verification language.
      programming-languageverificationviper
      Scala
      •
      Mozilla Public License 2.0
      •47•83•99•18•Updated Apr 4, 2025Apr 4, 2025

    • silver-sif-extension

      Public
      Extension of the Viper language with modular product programs and information flow specifications
      Scala
      •
      Mozilla Public License 2.0
      •1•2•0•1•Updated Apr 4, 2025Apr 4, 2025

    • ReusableProtocolVerificationLibrary

      Public
      Go
      •0•2•0•0•Updated Apr 3, 2025Apr 3, 2025

    • gobra

      Public
      Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
      gogolangverification
      Scala
      •
      Other
      •32•124•128•13•Updated Apr 3, 2025Apr 3, 2025

    • check-license-header

      Public
      GitHub action to check whether all files have a specified copyright license header
      TypeScript
      •
      Other
      •2•6•2•0•Updated Apr 2, 2025Apr 2, 2025

    • 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•0•Updated Apr 1, 2025Apr 1, 2025

    • vs-verification-toolbox

      Public
      Useful component to build VS Code extensions for verifiers.
      TypeScript
      •
      Mozilla Public License 2.0
      •2•5•0•0•Updated Apr 1, 2025Apr 1, 2025

    • locate-java-home

      Public
      Locates JAVA_HOME on any platform, and can differentiate between different versions.
      TypeScript
      •
      Other
      •9•3•0•0•Updated Apr 1, 2025Apr 1, 2025

    • prusti-assistant

      Public
      VS Code extension to verify Rust programs with the Prusti verifier.
      verificationvscode-extensiondiagnosticsprustirust
      TypeScript
      •
      MIT License
      •10•23•9•5•Updated Apr 1, 2025Apr 1, 2025

    • vpr-mode

      Public
      Viper mode for emacs
      Emacs Lisp
      •
      Mozilla Public License 2.0
      •1•2•0•0•Updated Mar 31, 2025Mar 31, 2025

    • VerifiedSCION

      Public
      Verifying the SCION architecture using Gobra
      Go
      •
      Apache License 2.0
      •4•11•8•9•Updated Mar 25, 2025Mar 25, 2025

    • prusti-dev

      Public
      A static verifier for Rust, based on the Viper verification infrastructure.
      verificationviperformal-verificationrust
      Rust
      •
      Other
      •110•1.6k•252•27•Updated Mar 21, 2025Mar 21, 2025

    • smt-scope

      Public
      SMTscope automatically analyses and visualises SMT solver execution traces.
      profilerz3instantiationsmtaxiomquantifierse-matching
      Rust
      •
      Apache License 2.0
      •4•32•6•1•Updated Mar 20, 2025Mar 20, 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

    • tutorial

      Public
      This repo contains the sources of the official Viper tutorial (http://viper.ethz.ch/tutorial). Feel free to submit your fixes and additions via pull requests. Please report technical issues via the issue tracker.
      4•0•6•4•Updated Mar 18, 2025Mar 18, 2025

    • silicon-sif-extension

      Public
      Extension of Silicon for product programs, in particular product program counterexample transformation
      Scala
      •
      Mozilla Public License 2.0
      •0•0•0•0•Updated Mar 17, 2025Mar 17, 2025

    • viper-roots

      Public
      Isabelle
      •
      Mozilla Public License 2.0
      •0•2•0•0•Updated Feb 25, 2025Feb 25, 2025

    • 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•1•Updated Feb 18, 2025Feb 18, 2025

    • axiom-profiler-2

      Public
      Temporary redirect to renamed repo
      0•1•0•0•Updated Feb 14, 2025Feb 14, 2025

    • axiom-profiler

      Public archive
      The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
      C#
      •
      Other
      •4•32•20•2•Updated Feb 13, 2025Feb 13, 2025

    • carbon-proofgen

      Public
      Scala
      •
      Mozilla Public License 2.0
      •0•0•0•1•Updated Feb 2, 2025Feb 2, 2025

    • smt-logs

      Public
      Scripts to get logs from deductive verifiers
      Shell
      •
      Apache License 2.0
      •0•0•0•0•Updated Jan 27, 2025Jan 27, 2025

    • gobra-action

      Public
      Github Action to verify Go code with Gobra directly in a CI workflow
      gogolangverificationformal-verificationactionsgithub-actions
      Shell
      •
      Mozilla Public License 2.0
      •2•2•4•1•Updated Jan 17, 2025Jan 17, 2025