symbolic EVM evaluator

The Rosette solver-aided host language, sample solver-aided DSLs, and demos

A proof assistant and a dependently-typed language

Kleene Algebra with Tests (KAT) and Brzozowski automata

Performant type-checking for python.

Statically typed programming language

An in-memory file system for Java 7+

Gradle plugin to use the Checker Framework for Java

A tutorial on the ott tool for presenting type theory

Educational Proof Assistant for Type Theory

Formal methods training program with an emphasis on software in the blockchain & decentralized financed (DeFi) industry

The Practical Immutability for Classes and Objects (PICO) type system enforces transitive class and object immutability

linear-checker

Static checker for Java

Pluggable type-checking for Java

A reflection-based proof tactic for lattices in Coq

Proofs for Simple Reference Immutability for System F-sub

Proofs for Qualifying System F-sub

SeaHorn Verification Framework

A CheckerFramework plugin to detect the use of weak algorithms with the Java crypto API.

Type system to detect accidental logging and inappropriate use of critical data in Java applications.

Model Checker for Java Programs

A Java compiler plugin that proves, at compile-time, that Java code only requests 256-bit data keys from AWS KMS.

Research programming language for concurrent ownership

Java toolkit that allows you to write coroutines.

Kungfu Trader

Checkstyle is a development tool to help programmers write Java code that adheres to a coding standard. By default it supports the Google Java Style Guide and Sun Code Conventions, but is highly co…

Glacier is a type annotation extension to Java that enforces transitive class immutability.