Jason E. Aten, Ph.D. glycerine

Q: The Ivy formal verification toolchain from Ken McMillan and Oded Padon https://kenmcmil.github.io/ivy uses Z3 and ABC backends to discarge verification conditions generated by models written in the Ivy language which is a language of the EPR (Effectively Propositional ) logic subset of first of logic. The role of the Ivy compiler is to compile from the Ivy language into the languages of Z3 and ABC. How can we properly characterize the difference between the input language and the output languages of Ivy? If Ivy input is in EPR, what is the language or logic subset

MFIC — Mechanically-Falsifiable Independent Control

A discipline for checks that can't be fooled by the same mistake that produced the work.

Abstract. When the author of a piece of work — an LLM, or a human moving fast — can be confidently and silently wrong, the usual defenses fail quietly: a test written from the same mistaken assumption as the code passes while the code is broken. MFIC is the class of check that escapes this trap, defined by four properties that must all hold at once. It is Mechanical (cases swept by machine, not hand-picked, so nothing is silently omitted), Falsifiable (each case genuinely bites when the work is wrong, on inputs you couldn't pre-arrange to pass), Independent (its verdict comes from the contract or the data — a source the producer doesn't control — which is segregation of duties restated for software), and a real Control (it holds the authority to block the bad outcome, not merely log it). This is the COSO / Sarbanes-Oxley model of internal co

Self-Describing Foreign Frame Protocol

Specification v1.7

JIT compilers, games, audio, and soft-real-time applications frequently need both high performance foreign-code interoperation and relief from garbage collection pauses.

Note to readers: This document is an early draft of a model for memory-safe references that I've been working on for the last ~2 years. While I think it is quite promising, the design is unfinished. The "regions" that I present in this document have not been given a formal semantics, and I have not explained where they originate from. My goal is merely to convince you that the design is promising, and that if seen to completion, it would advance the frontier of zero-cost memory safety.

Update March 2025: I am working on a newer version of this proposal, that aims to simplify the model substantially. When I have finished that proposal, I will put a link here.

Update August 2025: Verdagon has written an awesome blog post that explains this proposal at a high level. I recommend you check it out!

Abstract

In this document, I present a novel model for memory-safe references that aims to significantly improve upon the Rust-inspired model that Mojo c

Go development environment on Windows with MSYS2

Normally, it is sufficient to grab the Go MSI installer from the website in order to set up the toolchain. However, some packages that provide Go wrappers for C libraries rely on cgo tool, which in turn, needs the GCC toolchain in order to build the glue code. Also, 3rd-party dependencies are usually hosted on services like GitHub, thus Git is also needed. This mini-guide illustrates how to setup a convenient development environment on Windows using MSYS2.

	/*
	Copyright 2025 The Go Authors.

	Redistribution and use in source and binary forms, with or without
	modification, are permitted provided that the following conditions are
	met:

	* Redistributions of source code must retain the above copyright
	notice, this list of conditions and the following disclaimer.
	* Redistributions in binary form must reproduce the above

	// =============================================================================
	// XNU kperf/kpc demo
	// Available for 64-bit Intel/Apple Silicon, macOS/iOS, with root privileges
	//
	//
	// Demo 1 (profile a function in current thread):
	// 1. Open directory '/usr/share/kpep/', find your CPU PMC database.
	// M1 (Pro/Max/Ultra): /usr/share/kpep/a14.plist
	// M2 (Pro/Max): /usr/share/kpep/a15.plist
	// M3: /usr/share/kpep/as1.plist

	#!/usr/bin/env bash
	set -euo pipefail

	# patch-claude-code.sh — Rebalance Claude Code prompts to fix corner-cutting behavior
	#
	# What this does:
	# Patches the npm-installed @anthropic-ai/claude-code cli.js to rebalance
	# system prompt instructions that cause the model to cut corners, simplify
	# excessively, and defer complicated work.
	#

	package main

	import (
	"sync"
	"sync/atomic"
	"testing"
	"testing/synctest"
	"time"

	"fmt"

	This is an attempt to show that Raft's safety is
	preserved with single-server membership changes as
	described in the dissertation plus the patch that a
	leader may not append a new configuration entry to
	its log until it's committed an entry from its
	current term.

	This extends the safety argument in the
	paper/dissertation. The only part that's different
	(as far as I can tell) for membership changes is Step