Memory Safety in Envzn

A new systems programming language

By Brian Haughton
Oct 12, 2026

Introduction

Envzn (https://envzn-lang.org) has been recently released in beta as a new modern systems programming language; at the time of this writing, it is still in development. It was designed to be memory safe from the start.

Much has been written about memory safety lately1 and it seems the volume has been turned up since many large companies decided to publicize that they are writing systems and programs in Rust. For example, Microsoft2 and Chromium3 each found that about 70% of their serious security bugs were memory-safety errors, and Google reports that Android’s share fell from 76% to 24% as new code moved to Rust.4

Our Definition

In designing Envzn, I considered the memory model for Java5, Go6, Rust7, C++8, and many other mainstream languages. I felt that Rust’s borrow checker was a definite step forward and found it inspiring. Rust’s hybrid model of proving lifetimes at compile time, but checking most boundaries at run time9, seems to be the honest path forward.

Many languages were designed under the assumption that memory safety was something that can only be achieved at run-time. Programs can become too complicated and developers are too brilliant for a language team to anticipate fully how the language would be used. Much research has been done on this topic, and many believe that while compile-time analysis is helpful, run-time checking is the only viable option for true memory safety.10

Envzn is also a hybrid model. I took the approach that compile time analysis is sufficient for everything the code text decides, like lifetimes, ownership, leaks, and initialization, because the compiler walks the whole program and can follow every reference through its call graph and control-flow graphs.11 For variables that depend upon input, like an array index, math calculation, or call depth, these are checked at run time, but cheaply because the proof has already covered everything else. Any pattern the compiler cannot prove safe is not admitted; it is refused and the developer has to redesign that code.12

“A correct Envzn program neither leaks nor crashes on a memory fault. Every allocation is owned, destruction happens at a point the source determines, and the patterns ownership cannot prove safe are refused at compile time rather than admitted and hoped over.”13

I divided the general hazards of memory safety into 8 categories that could create unsafe conditions for memory access, and addressed each either within the compiler, the language structure, or the run time:

  1. Escaping / dangling – a reference outlives the source it points to
  2. Use after move – a value is used after its ownership moved to another
  3. Reference mutation – a value is changed while a reference to it is live
  4. Leaks – memory is never freed
  5. Null or uninitialized – a value is read before its assignment
  6. Data races across threads – two threads access a value at once, one writing
  7. Spatial / bounds - access goes beyond the bounds of its allocation
  8. Stack exhaustion – call depth or frame size outgrows the main (or thread) stack

For those of you that are curious about other definitions, Microsoft’s four recurring root causes related to memory safety are out-of-bounds, use-after-free, type confusion, and uninitialized use.14 Type confusion cannot occur in Envzn code, and the other three are on the list.

How Our Compiler Achieves Memory Safety

Types in the Language

Envzn is an ahead-of-time compiled, strongly-typed language with 25 primitive types, plus classes, enums, structs, groups and interfaces, where casting is forbidden, but conversions are common. Pointers do not exist (outside of UNSAFE blocks) and there’s a single owner for each owning handle, and conversions to and from handles are not allowed.

  1. Primitives – like int64, float32; can never be null; kept and passed by value
  2. Owning handle – is allowed to be null (EMPTY); populated by assignment
  3. REFERENCE handle – can never be null; read-only reference to its source
  4. MUTABLE REFERENCE handle – can never be null; writable reference to its source; only one is allowed to exist at any given time for a source
  5. SHARED MUTABLE REFERENCE handle – can never be null; writable reference to its source; multiple are allowed at any given time for a source; must point to a SHARED CLASS; the SHARED CLASS is a monitor

Further, I disregarded the asymmetry of create/destroy, so I kept the “create” function, but specifically saw an opportunity for a language without the need for a “destroy”, “delete”, or “free” that also didn’t carry the burden of garbage collection. The “delete” function does not exist. Cleanup happens in a deterministic manner when an object falls out of scope at a closing brace ‘}’ boundary similar to C++.

The EVIR and the REFERENCE checker

With every library created in Envzn code, the compiler produces 3 files, the library, the library .headers file, and the library .evir file. The library is linked into your executable just like a C++ library, the .headers file contains all class public data fields and method declarations for the developer to read method signatures, and the .evir file contains the pre-compiled bytecode of the library.

For every REFERENCE variable (types 3-5 above), the compiler analyzer traces that handle from its beginning to its end, walking its use from the time it is assigned to when it falls out of scope. If the REFERENCE variable is used by another module (in a library or in an executable), the analyzer opens that .evir file for the library and includes that in its reference walk.

The reference walk that may include multiple .evir files detects instances of hazards 1 and 3 described above; the other 6 are handled by the analyzer, the language structure, or the runtime. Any module with even one REFERENCE that cannot be proven safe fails the build of that module. This means that sometimes good code may fail because the analyzer cannot prove that a REFERENCE is clean.

How Envzn handles each type:

  1. Escaping / dangling : structural checker + EVIR reference walk
  2. Use after move : source is poisoned; use after move is a detected compiler error
  3. Reference mutation : many readers/one writer; no mutation as REFERENCE
  4. Leaks : single ownership + acyclicity proof over strong edges + tool to detect leaks
  5. Null or uninitialized : presence proven before use
  6. Data races across threads : ownership moves on channel send; no shared mutable capture
  7. Spatial / bounds : runtime checks on every index or a guard allows proven unfettered access
  8. Stack exhaustion : no-recursion drops, use RECOVER to handle ‘StackOverflowError’

Calls into C code

For those that believe that with any access into another language that isn’t safe, like C, then the whole program is unsafe15, Envzn does allow access to C code but only in a sandbox or via a special direct call. By this definition, Envzn is therefore memory safe as long as you stay within the Envzn code.

For the sandbox approach, Envzn has a keyword UNSAFE that refers to a block of code with braces, written like UNSAFE{…}. The UNSAFE block allows unchecked access to C structures and data fields that would otherwise be forbidden. The guarantee is confinement; a raw C pointer cannot escape the block.

For the direct call, Envzn has a keyword phrase FOREIGN BIND to map C functions directly into Envzn code. C functions may be declared at the top of the .ev file in Envzn format, and then called directly from Envzn code.

MODULE ffiExample
// The module's manifest must opt in to the foreign boundary: "allows_foreign": true

// Bind a libc function with its real C signature (unistd.h):
//     ssize_t write(int fd, const void *buf, size_t count);
FOREIGN BIND write(int32 fd, binary[] data, C.size_t count) RETURNS C.ssize_t

CLASS Main IMPLEMENTS TaskStarter {
    INIT(REFERENCE String[] argv) { }

    METHOD start() RETURNS STATUS {
        ByteBuffer payload := "hello from C\n" INTO ByteBuffer
        binary[] bytes := payload->view(0, payload->size())->copy()

        // Every call across the boundary sits inside an UNSAFE block.
        int64 written = 0
        UNSAFE { written = FOREIGN::write(1, bytes, payload->size()) }

        // A negative length never reaches C as a huge size_t:
        // the conversion raises MathError before the call is made.
        int64 negative = -1
        TRY {
            int64 ignored = 0
            UNSAFE { ignored = FOREIGN::write(1, bytes, negative) }
        }
        RECOVER (MathError e) {
            printline("refused: a negative length cannot become a C size_t")
        }
        RETURN (SUCCESS)
    }
}

Using UNSAFE.HANDLE and Opaque types

Envzn has two types that can hold system level C pointers, but the developer cannot invoke any memory space from those nor convert them into handles or numbers. UNSAFE.HANDLE lowers to a raw untyped C pointer, but it’s only a storage device, received from a foreign function and passed back into a foreign function. Opaque is a primitive type that can hold any typed C pointer, like one specific to SSL. Within an UNSAFE block it can be assigned, used in foreign functions, and its structures accessed. See the Envzn Constitution I.I.viii(d).

What the Compiler Does

The EVIR bytecode file exists because in order to prove memory safety for any REFERENCE handle, the compiler must walk the code to check everywhere that REFERENCE is used. The machine code in the library itself doesn’t carry enough information for the walk, so the compiler generates a .evir bytecode file for each library, allowing the compiler to actually walk into the precompiled bytecode to check that REFERENCE, and to open as many .evir files as required to do so.

For those of you that may say either the walk is flawed or impossible to follow or would extend the compile time to something unreasonable, I’d say two things: first I will acknowledge that the compiler evir walk is not perfect and may miss something. In those cases the rule is that if the compiler cannot prove the REFERENCE is safe, then the build fails. Even so, it may still miss16. Second, timings have shown that even a complex three-hop .evir walk adds an average of about 2 secs to any build, a timeframe that I felt was reasonable.

The Test Suite

The current size of compiler is over 120k lines of code across ~300 python files with about 3300 test cases with diagnostic, adversarial, and probing tests; the standard library and adjacent modules are over 60k lines of code across ~280 Envzn files with about 3600 test cases. Every error found has contributed to our test suite. I have frequently used clang sanitizers for identifying errors. Also I have frequently asked AI to help find defects and log them.

Our Current State and Our Journey Forward

The Envzn language today compiles and runs on macOS and Linux. It lowers to C++ but is on-path to lower to LLVM soon.

Notes

1. CISA, NSA, FBI and international partners, “The Case for Memory Safe Roadmaps,” December 2023, https://www.cisa.gov/case-memory-safe-roadmaps; and The White House, Office of the National Cyber Director, “Back to the Building Blocks: A Path Toward Secure and Measurable Software,” February 2024, https://bidenwhitehouse.archives.gov/oncd/briefing-room/2024/02/26/press-release-technical-report. ↩

2. M. Miller, “Trends, Challenges, and Strategic Shifts in the Software Vulnerability Mitigation Landscape,” BlueHat IL, February 2019; and Microsoft Security Response Center, “We Need a Safer Systems Programming Language,” July 2019, https://www.microsoft.com/en-us/msrc/blog/2019/07/we-need-a-safer-systems-programming-language. About 70% of the CVEs Microsoft patched over twelve years were memory-safety issues. ↩

3. The Chromium Projects, “Memory Safety,” https://www.chromium.org/Home/chromium-security/memory-safety. About 70% of 912 high- or critical-severity security bugs since 2015 were memory-safety bugs; half were use-after-free. ↩

4. J. Vander Stoep and A. Rebert, “Eliminating Memory Safety Vulnerabilities at the Source,” Google Security Blog, September 2024, https://security.googleblog.com/2024/09/eliminating-memory-safety-vulnerabilities-Android.html. Memory-safety vulnerabilities fell from 76% of Android’s total in 2019 to 24% in 2024. ↩

5. J. Gosling et al., The Java Language Specification, Java SE 21 Edition, §15.10.4: every array access is checked at run time and raises ArrayIndexOutOfBoundsException, https://docs.oracle.com/javase/specs/jls/se21/html/jls-15.html#jls-15.10.4. ↩

6. The Go Authors, “The Go Memory Model,” https://go.dev/ref/mem; see also R. Cox, “Off to the Races,” https://research.swtch.com/gorace. A data race on a multi-word value, such as a slice or an interface, can break Go’s memory safety. ↩

7. R. Jung, J.-H. Jourdan, R. Krebbers and D. Dreyer, “RustBelt: Securing the Foundations of the Rust Programming Language,” POPL 2018, https://plv.mpi-sws.org/rustbelt/popl18/. The first machine-checked safety proof for a realistic subset of Rust’s ownership type system. ↩

8. C and C++ are the memory-unsafe languages the guidance in note 1 recommends moving away from; see CISA et al., “The Case for Memory Safe Roadmaps” (note 1). ↩

9. S. Klabnik and C. Nichols, The Rust Programming Language, ch. 8.1, “Storing Lists of Values with Vectors,” https://doc.rust-lang.org/book/ch08-01-vectors.html. Indexing past the end of a vector panics at run time. ↩

10. L. Szekeres, M. Payer, T. Wei and D. Song, “SoK: Eternal War in Memory,” IEEE Symposium on Security and Privacy, 2013. A survey of run-time defences for C and C++, the setting in which run-time checking is treated as the only option. ↩

11. P. Cousot et al., the Astrée static analyzer, https://www.astree.ens.fr/. In 2003 it proved the absence of run-time errors in the Airbus A340 primary flight-control software (132,000 lines of C) with zero false alarms, in a subset of C that excludes recursion and dynamic allocation. ↩

12. H. G. Rice, “Classes of Recursively Enumerable Sets and Their Decision Problems,” Transactions of the American Mathematical Society 74 (1953); and P. Cousot and R. Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints,” POPL 1977. No analysis can decide every behaviour of every program, so a sound analysis must over-approximate, and some correct programs are refused. ↩

13. The Envzn Constitution, Article I.A, “Memory safe,” https://envzn-lang.org/constitution.html. ↩

14. M. Miller, BlueHat IL 2019 (note 2). The recurring root causes of Microsoft’s memory-safety CVEs were heap out-of-bounds access, use-after-free, type confusion and uninitialized use. ↩

15. H. Xu, Z. Chen, M. Sun, Y. Zhou and M. R. Lyu, “Memory-Safety Challenge Considered Solved? An In-Depth Study with All Rust CVEs,” ACM Transactions on Software Engineering and Methodology, https://arxiv.org/abs/2003.03296. Every memory-safety CVE in Rust studied (up to 2020) required unsafe code. ↩

16. This is why it is still a work in progress. ↩