An open source version of Cryptol has been released. The language is designed specifically for cryptography, and while this is the first public version, the language has been under development and in use for almost 15 years.
Cryptol was originally developed by Galois for the United States National Security Agency, but it is also used by private companies.
Writing about the new release on the company blog, the team points out that Cryptol helps developers detect (or avoid) correctness errors in cryptographic code. They say Cryptol reduces the gap between the reference specification of a cryptographic algorithm and an executable version which can be used for testing and verification.
The problem with many cryptographic algorithms is that they are written in academic papers in a mathematical notation that is not executable. This is then converted to a "reference implementation" which looks different to the math, and that reference implementation is then used in apps, but there has been no easy way to check the accuracy of the reference implementation against the mathematical specification.
Cryptol is a domain-specific language for specifying cryptographic algorithms. According to its creators a Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language.
Using a specification in Cryptol, programmers can generate their own test vectors, prove theorems, and (using other tools) verify equivalence to their own programs, or generate code or hardware from the specification.
The developers say Cryptol is a powerful tool for harnessing the power of SMT Solvers like Yices, Z3 and CVC4. The open source version of is, hosted on GitHub. If you want to see the range of uses to which it can be put, the download includes a ‘funstuff’ folder with solutions to puzzles such as Sudoku encoded in Cryptol, which then can be solved using the :sat command.
More Information
Related Articles
Prime Numbers And Primality Testing
Stick Figure Guide To AES Encryption
Public Key Cryptography Set To Fail In Five Years
Open Source Homomorphic Cryptography
To be informed about new articles on I Programmer, install the I Programmer Toolbar, subscribe to the RSS feed, follow us on, Twitter, Facebook, Google+ or Linkedin, or sign up for our weekly newsletter.
C# Could Overtake Java in TIOBE Index
13/11/2025
C# 14, the latest Long Term Support release of the .NET language was released this week as part of .NET 10. Currently in fifth position in the TIOBE Index rankings it looks set to overtake Java and it [ ... ]
Windows XP Crocs Now On Sale
07/11/2025
Fans nostalgic for the -er- good old days of Windows XP can now commemorate them with specially themed Crocs.
- Google Tunix Hack Hackathon Now Open
- AI Improves Devs Skills, Enhances Their Roles
- Linkerd Adds MCP Support
- Julia 1.12 Adds Trim Feature
- IBM Launches Granite Version 4.0 and Granite-Docling
- Robotic Gut Spider For Exploring Digestive Tract
- Jules Coding Agent Upgraded
- OpenCode - The Claude Code Alternative
- Qodana Revisited
- Formae Launched As Terraform Alternative
- InfluxDB 3.6 Released With AI Capabilities
- .NET 10, C# 14 and F# 10 Released Alongside Visual Studio 2026
- XAML.io 0.5 Adds Multi-File Project Editing
Comments
or email your comment to: comments@i-programmer.info