Skip to content

KeY Documentation

LLM support

Initializing search

Home
User Guide
Developer Guide
Historical

KeY Documentation

Home
User Guide
User Guide
- 1. Getting Started
  1. Getting Started
- 2. Working with the Prover
  2. Working with the Prover
- 3. Structuring Verification Projects
  3. Structuring Verification Projects
- 4. Proof Scripts
  4. Proof Scripts
- 5. SMT Solvers
  5. SMT Solvers
  - Adding SMT Solvers
- 6. Bridges to Other Tools
  6. Bridges to Other Tools
- 7. Language Reference
  7. Language Reference
- 8. FAQ
- Release Notes
Developer Guide
Developer Guide
- 1. Architecture
- 2. Building KeY
- 3. Working on the Code
  3. Working on the Code
- 4. Extending KeY
  4. Extending KeY
  - Overview
  - How-Tos (verified recipes)
    
    How-Tos (verified recipes)
    
    Add an Extension Module
    
    Add a Menu Entry
    
    Add a Toolbar
    
    Add Taclets
    
    Add a Proof Macro
    
    Add a Script Command
  - Writing Taclets
  - Polarity Triggers for Rewrite Taclets
  - GUI Extension Points
  - Script Commands in Depth
  - Adding SMT Solvers
  - Event Listeners
- 5. Using KeY as a Library
  5. Using KeY as a Library
  - KeY in External Projects
- 6. Internals
  6. Internals
- 7. Testing
  7. Testing
- 8. Writing Documentation
Historical
Historical
- Eclipse plugins (unsupported)
  Eclipse plugins (unsupported)
  - KeY basics
  - SED
  - Stubby
  - KeY IDE
  - MonKeY
  - Starter
  - VisualDBC
  - JML Editing
  - Resources

Table of contents

Features
Configuration
How to use

LLM support

⚠ not yet verified

Features¶

Configuration¶

How to use¶

Made with Material for MkDocs