> 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)

<figure><img src="/files/AghjeMeAECL46ydbDw6E" alt=""><figcaption></figcaption></figure>

## 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.&#x20;
* **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.&#x20;

**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.&#x20;

[**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.&#x20;

## 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.&#x20;

[**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 dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter, and the optional `goal` query parameter:

```
GET https://tools.galois.com/cryptol/cryptol-the-language-of-cryptography.md?ask=<question>&goal=<endgoal>
```

`ask` is the immediate question: it should be specific, self-contained, and written in natural language.
`goal` is optional and describes the broader end goal you are ultimately trying to accomplish on behalf of the user. GitBook uses it to tailor the answer towards what is most useful for that goal.

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.