> For the complete documentation index, see [llms.txt](https://tools.galois.com/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://tools.galois.com/cryptol/cryptol-the-language-of-cryptography.md).
# Cryptol: The Language of Cryptography
## What is Cryptol?
Cryptol is a mathematically-focused programming language for creating, analyzing, and verifying complex cryptographic algorithms. Intuitive, expressive, and precise, Cryptol and its associated software tools allow you to describe algorithms in the language of mathematics and prove key security and other properties.
[**View on GitHub**](https://github.com/GaloisInc/cryptol) [**Download**](/cryptol/get-started/download.md)
## Core Features, Capabilities, and Applications
* **Expressive Syntax:** Cryptol’s high-level abstraction and intuitive syntax make it exceptionally expressive and ideal for rapid prototyping, refining, and analyzing cryptographic algorithms.
* **Executable Specifications:** With Cryptol, users can create specifications that aren’t just theoretical models, but can be run as executable code.
* **Formal Verification:** Cryptol allows users to test and verify specifications, while [SAW](https://tools.galois.com/saw/) extends this capability to verify implementations written in C, Java, and Cryptol.
* **Scalable Security:** Cryptol and SAW automate much of the most time-consuming parts of formal verification, enabling the process to scale to complex systems
* **Open Source Library:** Access specs for traditional and post-quantum cryptographic algorithms in our [open source ](https://github.com/GaloisInc/cryptol-specs)repository of Cryptol specifications.
## How Does It Work?
**Bridging the Gap:** Cryptographic algorithms are typically represented in two forms: a non-executable mathematical notation for theoretical understanding (the “specification"), and a “reference implementation” for practical use. However, this approach presents a significant challenge: there isn’t an easy way to check the implementation against the mathematical specification to verify the correlation between the two and ensure it is correct and secure.
**A New Paradigm:** Cryptol revolutionizes this process in two key ways. First, it enables engineers to create specifications of cryptographic algorithms (e.g., to generate cryptographic keys, encryption/decryption algorithms, hashing functions, etc.) that are executable, testable, and verifiable. From those specifications, users can generate their own test vectors, prove theorems, and more. Second, using Galois’s Software Analysis Workbench (SAW), it’s possible to prove the equivalence of performant, manually-written implementations to specifications.
[**READ OUR DOCUMENTATION** ](/cryptol/get-started/documentation.md)
## Impact
Cryptol and SAW have been used in national security, fintech, and cloud computing applications to keep citizens, systems, and data safe; secure financial transactions; and protect the privacy of millions of people across the globe. The high assurance approach they represent forms the backbone—both technologically and philosophically—of Galois’s larger effort to create trustworthiness in the most critical systems on the planet, and to maximize impact through sharing these powerful tools with the open source community.
## Open Source
The R\&D community, industry, and the public at large can benefit when tools like Cryptol are open sourced. In addition, open-source tools can themselves benefit from and be independently verified by a broad, diverse user community. With this in mind, the U.S. Government and Galois agreed to open source Cryptol for broad application and public benefit, releasing the first fully public version in 2014. Now, Cryptol is open for anyone to use and explore, as is our open-source cryptographic library that includes specs for both traditional and post-quantum cryptographic algorithms.
[**View the Cryptol Specs Repository on Github**](https://github.com/GaloisInc/cryptol-specs)
---
# Agent Instructions
This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com.
## Querying This Documentation
If you need additional information that is not directly available in this page, you can query the documentation by asking a question.
Perform an HTTP GET request on the following URL with the `ask` and `goal` query parameters:
```
GET https://tools.galois.com/cryptol/cryptol-the-language-of-cryptography.md?ask=&goal=
```
`ask` is the immediate question: it should be specific, self-contained, and written in natural language.
`goal` is what the user is ultimately trying to achieve, the reason they need the answer. Sharing it helps GitBook give you a better, more relevant answer. A goal is most helpful when it describes the outcome the user wants rather than restating the question. For example, with `ask=how do I create an API token`, a goal like `automate deployments from our CI pipeline` lets GitBook tailor the answer to that use case.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.
Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.
