K 7.0: Improving K for Ecosystem Tool Developers

April 2024 saw the release of version 7.0 of the K Framework. Previously, K was focused on the implementation of programming language semantics, and external tool support was required to expand those semantics into production tooling for a language. In K 7.0, we have merged our Python support library for K (Pyk) into the K compiler, making it the primary way for tool developers to interact with K.

About K

K began as a research project at the University of Illinois in 2003. At its core, K is a programming language for defining the semantics of other programming languages. By writing a single definition of a language’s syntax and semantics, K derives a set of useful tools automatically. (for example, a fast interpreter for that language).

At Runtime Verification, K is at the heart of what we do, and we’ve used it to build implementations of almost every mainstream programming language at one time or another. For example, one of our most active projects is KEVM, our K implementation of the Ethereum virtual machine.

Legacy

In previous versions of K, developers largely interacted with the framework via a set of command-line tools that resemble a traditional compiler. A K language definition is compiled to produce a set of tools (interpreter, parser, theorem prover, …); these tools can then be used to execute, process or analyse programs.

$ kompile my-language.k
$ krun my-program.lang
$ kprove my-language-spec.k

While this approach works well for learning the K language and developing small semantics, it starts to become cumbersome for larger examples. At RV, we found ourselves developing increasingly complex shell scripts and ad-hoc Python applications to automate usage of the K toolchain and integrations with third-party language tooling. As we built larger applications using K, it became clear to us that we needed a more principled approach.

In 2022, we began to develop that principled approach. Much of the ad-hoc Python code we had developed over the years was upstreamed into a standalone library called Pyk. By doing so, we were able to reuse a lot of common patterns in K-based language tooling, and reduce the burden on project maintainers to implement common boilerplate such as integration testing, build systems, and dependency management. By 2023 and K version 6, writing Pyk-based Python applications had become the de facto way to write so-called “modern” K tooling; any new projects developed inside RV were using Pyk extensively, and we began the process of porting older projects over to using Pyk as well. Increasingly, the original command-line interface was becoming a legacy tool in practice.

New in K 7

As we began to shift the responsibility for more new (and existing) K features into Pyk, we realised that the time was right to upstream Pyk back into K and explicitly codify its role as the official frontend for developers interacting with K. This was a major refactoring of our code and infrastructure at RV, but so far we’ve been pleased with the resulting developer experience from having more of K under one roof.

This year, we’ve spent a lot of time working on improving the code quality and developer experience of the K compiler’s internals. By doing so, we’ve been able to make substantial progress on documenting and modularising some of the older and more complex parts of the compiler, and have been gradually re-implementing parts of the compiler in Pyk.

So far, a lot of the work that’s gone into K 7 and the 7.0 release is internal organisation and infrastructural changes that will let us move faster on subsequent improvements. We’ve substantially reduced our internal technical debt, and have several more ongoing projects that will take this improvement further. Future releases of K 7 will begin to include more new user-facing features and improvements as well:

• Upstreaming of widely-used third-party library support into K. This will make it easier to develop projects that use common cryptographic primitives, or want to expose their language tooling via JSON-RPC.
• Improved documentation and examples of writing modern semantics using K, as well as of the K language itself.
• New compiler features (such as fully-deterministic type inference) that will improve reliability and performance for large programs.

We’ll be posting regular threads on Twitter with updates on K throughout the year, so please keep an eye out for more improvements as we make them!

Building Tools with K

Our motivation for releasing this new version of K is that we’ve increasingly found that K works brilliantly as a library which more specialised applications and tools can be built on top of. Users in a language ecosystem typically don’t want to interact directly with the semantics of that language, but rather with accessible tools that abstract the underlying formalism away for them.

We’ve recently been excited to share our ongoing work on two such products in the EVM ecosystem, Kontrol and SimboliK:

• Kontrol works with Foundry projects to bring the power of symbolic execution to developers’ existing property test suites, giving them access to lightweight formal verification techniques with an extremely low barrier to entry.
• SimboliK is a brand-new Solidity debugger for Visual Studio Code with built-in symbolic execution based on K. SimboliK allows developers to inspect all possible execution traces at once within a single debugging session and with unmatched precision. 

These are just two use cases: we’re actively working on and proposing a number of other examples (such as translation validation for existing compilers, and ecosystem-specific formal verification) with partners. With K 7, it’s easier than ever to bring this kind of advanced tooling to new languages and ecosystems, and the range of applications for which K is the best fit is larger than ever. If you’re involved in building programming language tooling, we’d love to talk to you about your needs in this space.

What else is new?

As well as reorganising to focus on tool development with K, we’ve been working on improvements to the K language and compiler as usual. Some of the main highlights are:

• Deterministic type inference for most K terms. Our previous type inference machinery used a constraint solver to select valid typings, which could produce inconsistent or slow performance for some users. We’ve implemented a new mechanism based on the Simplesub algorithm that addresses the performance problem.
• Substantial improvements and cleanups to K’s attribute subsystem, resolving a number of unintuitive quirks that have been present in the language for some time. We hope to carry this work on and further improve the developer experience of the K language.
• General bug fixes and improvements supporting internal tool and semantics development.

Connect with us!

If you want to learn more about K, tooling, and our work to secure protocols, follow us on Twitter or ask any questions directly to our team on Discord.