There have been several recent announcements about formal verification of software and hardware, both using AI and for AI systems:

• Harmonic announced last week that they are using their agent Aristotle for scalable verification of both software and hardware. For example, in a C library for big-number arithmetic, it was able to fix bugs and prove that a faster version was equivalent to the original. The person whose work I particularly follow in this area is Satnam Singh, who has worked on hardware verification for several years.
• SF-Tensor announced that they were formalizing NVIDIA’s PTX language in Lean to prove the correctness of GPU kernels. SF-Tensor was founded by three brothers at the age of 19, after they had completed their BSc degrees at 16 while attending high school.
• &Truth came out of stealth, announcing plans to use Lean to prove the correctness of AI-generated software. Key people involved include Clark Barrett, known for his work on cvc5 and CSLib; Ilya Sergey, known for Veil and his work on verification using separation logic; and Sebastian Ullrich, Lean’s second-in-command.
• Theorem. and Anthropic worked together on verifying open-source software running on a RISC-V processor. Their work covered encode–decode round-tripping, idempotence, algebraic laws, differential testing, self-consistency, and equivalence to reference implementations. They also proved isolation properties of a sandbox built on the xv6 academic kernel.
• AutoResearch.inc has also announced they have verified 7 web assembly tools down to ELF and sys calls (on x86-64 and RISC-V).

The common factor in these announcements is the goal of achieving full-stack formalization, either across the software stack or across a combination of software and hardware. In the past, verification was performed only on a small core of the software or on a simplified model of the actual software.

For reference, AWS’s access-control language, Cedar, had a Rust implementation running in production and a reference implementation—first in Dafny and later in Lean—that was verified for correctness.

One approach would be to develop Cedar entirely in Lean, compile to C, and deploy the generated C code in production. In addition to the formal model, we would write an optimized and full-featured implementation (which handles errors and messages more carefully, provides parsers for various formats, etc.) in Lean, and then prove the two equivalent. A key benefit of this approach is that we would formally verify—rather than just test—the equivalence of the deployed code and model. But there are significant downsides to writing production applications in Lean and deploying its generated C code. Lean is a new programming language, so it has a limited developer pool and lacks useful libraries available in mainstream languages. Debugging a failure might necessitate stepping through the generated C code and mapping it back to the Lean source, requiring expertise in C and Lean. Doing so could be particularly difficult if the failure is due to an interaction between handwritten code and Lean-generated C code. In addition, C is a memory-unsafe language, so a bug in the Lean compiler could lead to security issues.

— How We Built Cedar: A Verification-Guided Approach (April 2024)

Over the past year, I have been talking about liquid types as my personal preference for program verification. Liquid types are a restricted form of value-dependent types whose constraints can be checked automatically using SMT solvers. This is my sweet spot: you get much of the benefit of an expressive type system in which you can express properties such as typestate, preventing methods from being called when an object is in the wrong state—for example, calling read() after close(). And it comes at a much lower cost, especially because you do not have to write the proofs: the SMT solver takes care of that.¹

Until a few months ago, this trade-off was very important: very few people in the world had the expertise and time to undertake the full verification of a large open-source project (props to the seL4 folks!). Frontier models’ superhuman ability to generate proofs has since eroded this moat, and subsidized token prices make this the perfect time to conduct these experiments. I have to admit that the image above, which I used in my recent slides, might no longer make sense. It might become relevant again when token prices rise—probably to reflect their actual costs—and we need to save time and tokens while still verifying properties we care about, without going all the way down to the machine-code level.²

Right now, if we pursue full-stack verification, we might need to write code in a verification-first language like Lean. Dafny and my own aeon could be candidates, but Lean’s functional programming model and the substantial funding the project receives make it the ideal candidate. Rocq enthusiasts might not like it, but extracting executable code to OCaml is not such a significant advantage in the real world.

But we need Lean to improve. Above all, we need faster type checking and a much better optimizer. That’s the part that Bend2 got right from the start—the next mainstream language will require both verification and speed.

I started developing Aeon back in 2018 as a playground for program synthesis. Holes (?x) are valid expression in aeon (def f (i:Int) : Int := i * 2 + ?x compiles successfully and, when ?x is evaluated at runtime, it opens a repl asking the user for the right expression). However, the main advantage of holes is when you run the aeon compiler with "--synthesizer", it tries to find a suitable expression for the holes in your program. This blog post covers the different methods you have to describe what you want a function to do. We've decided on the function-level for the specification as it is the most normal public (and private) API of your code.

Basic Types

Aeon is a (very strongly) typed language, so you always need to write the types of top-level functions.¹ As such, all proposed candidate expressions to replace ?hole need to type-check. So writing Int as the return type already specifies something about the missing code.

def double (x:Int) : Int := ?hole

Liquid Types

Aeon supports liquid types by refining a basic type with a predicate. In the case below we refine the returning type of the function Int with the predicate that it needs to be equal to twice the value of x. Because Liquid Types can refer to other values in the program (such as function arguments), they are (value-)dependent types, but following a different discipline than the (full) dependent types you find in Lean, Rocq or Idris.

def double (x:Int) : {r:Int | r == x + x} := ?hole

So far, this definition covers both Refinement Types and Liquid Types. The main distinction of the two is that the refinements in Liquid Types need to be drawn from a decidable logic, so an SMT solver can give you a definitive answer of whether it type checks or not.

Liquid types guide synthesis directly in approaches such as Synquid and Liquid Tree Automata. In Aeon, their logical predicates can also be translated into constraints for SMT solving with Z3, syntax-guided synthesis (SyGuS), polynomial synthesis, and OR-Tools’ CP-SAT solver. Liquid Types are also used in our own custom synthesis algorithms that combine evolutionary search and liquid types.

Natural language documentation

Aeon also supports AeonDoc, using the @doc decorator to annotate a natural-language description of the function. We can take this documentation as input to a synthesis method (currently, only LLM-based synthesizers support @doc). This documentation complements any type that constrains the hole already.

@doc("Doubles the input.")
def double (x:Int) : Int := ?hole

Examples or test cases.

Aeon supports the decorator @example that takes a boolean predicate about the execution of the final synthesized function.

@example(double 3 = 6)
@example(double 5 = 10)
def double (x:Int) : Int := ?hole

Input–output examples guide many synthesis approaches: automata-based methods such as AFTA use them to prune spaces of candidate programs; top-down methods such as Myth or Decision Trees propagate examples into smaller synthesis subproblems; and bottom-up methods such as BUSTLE compose programs from smaller expressions evaluated on those examples. Examples also define fitness functions for genetic programming and provide training data for decision-tree learning, which learns conditional rules mapping inputs to outputs.

Decision Trees and Genetic Programming, coming from the Machine Learning backgrounds, assume that some examples might be wrong so they are more permissive. Other methods typically search for a solution that covers all examples. In this case, only noise-supporting methods can handle contradictory examples.

Because writing examples can be tedious, you can use CSV data directly or through an auxiliary file (@csv_data("1.0,2.0\n3.0,6.0\n4.0,8.0") or @csv_file("double.csv").

Optimization goals

@minimize_int(abs $ (double 4) - (4 * 2))
@minimize_int(abs $ (double 5) - (5 * 2))
def double (x:Int) : {r:Int | r = x + x} := ?hole

Aeon supports multiple maximize and minimize decorators to express optimization goals. We might know a given ideal target for the minimization criteria or not (for open problems). This example is the former, where you cannot have a value lower than 0. However, if you were to maximize the return value of a function that returns prime numbers, you would have no target value.

When multiple objectives are set, we consider this a multi-objective optimization problem and each algorithm typically returns the Pareto set, containing solutions that no other candidate is better in all axis. Genetic Programming and OR-Tools solvers have these features built-in. Recent Genetic Programming approaches have recommended Lexicase-selection instead of a Pareto tournament, but my own experience does not confirm this recommendation. If you are going to evaluate all objectives, then lexicase selection might make sense, but because tournaments only evaluate one objective for few good candidates, it ends up being more computational cheaper, and more time is left for exploration.

A big advantage of examples and optimization constraints over liquid types is that you can write any aeon expression that you want (such as multiplication of variables i*j). Because Liquid Types are limited to decidable theories, you cannot write² this multiplication and other types of expressions and you are limited to linear integer arithmetic, arrays, uninterpreted functions and other SMT theories.

Property-based Tests

Property-based testing is the idea that instead of writing concrete input and output examples, you write properties that relate them, and have random inputs generated to validate those properties. For me, it is very similar, if not the same, as Metamorphic testing.

def double (x:Int) : Int := ?hole

@property(100)
def prop_double_is_bigger (x:Int | x > 0) : Bool := double x > x

In this example, the body of the double function will have to work with 100 randomly-generated inputs and return a value that complies with the state property every single time.

Results

You can either run aeon on the command line, selecting the synthesizer method with -s (python -m aeon multi_objective.ae -s gp --budget 10), or use an LSP editor to ask the compiler to synthesize using a particular method. If you are using VSCode, you have an extra interface to explore program synthesis.

The first specification yielded def double (x:Int) : Int := 1, which matches exactly what we asked it to return: an Integer. When using the other specifications we got a variety of solutions: x+x, 2*x and x+x+0. But this is with a very simple specification that I would assume any synthesizer should be able to generate. Larger examples are left to the reader (or to the next blog post).

Non-functional requirements

All of the intent that we have expressed for far was related to functional correctness. But software developers know that non-functional properties can be equally important in some projects. As such, we are adding support for different forms of expressing quality properties. In particular, we already support @minimize_cputime(expression) and @minimize_energy(expression) for minimizing execution time and energy consumption respectively. Despite this support, the example above is too simple and trivial that the measurement overhead is many times that of the execution. I would only recommend using these advanced decorators for larger programs.

And aeon also supports other properties, you just need to write the code that translates the candidate function into a measure of that quality, using the example or optimization decorators.

Happy synthesizing!

A realidade da habitação em Portugal é completamente fora deste mundo. A minha geração e a mais nova não consegue pagar o custo que a habitação tem sido nas grandes cidades, nem no Algarve.

O Ivo Bernardo fez uma análise da situação da habitação em Portugal, baseado em números públicos de uma variedade de fontes.

• Public housing: this is where the data sides most with the protesters. Social rental housing is 1.1% of dwellings in Portugal, against an EU average of 8%. At €150,000 per home, 3% financing and public land, a cost-rent home in Lisbon breaks even at about €10.9/m² a month, 35% below the city’s median new rent. It can almost pay for itself exactly where it’s needed most. Remember the €1.74 billion NHR cost in 2024? That’s roughly 11,600 of those homes. In one year.
• Vacant homes: worth chasing, in the right places. The 100,000-plus recoverable homes in pressure municipalities are real.
• Limiting investment funds: I can’t back it or reject it, because the data doesn’t exist. Before we legislate, we need to measure.

— The housing crisis in Europe pt1 by Ivo Bernardo

Por sua vez, o João Tomé usa também dados reais para analisar a questão das casas vazias.

Em 2021, quase 249 mil casas estavam vagas por outros motivos, fora do mercado, em edifícios sem necessidade de reparação ou apenas com reparações ligeiras. Os dados ajudam a localizar uma possibilidade de resposta à falta de habitação. Ainda não dizem quantas dessas portas se podem abrir. As experiências de outros países ajudam a escolher o que tentar: apoiar obras, gerir o arrendamento e reforçar a oferta nas zonas com procura.

— Quantas casas vazias podem voltar a ter gente? por João Tomé

O artigo inclui ainda uma tabela com referências para medidas que foram implementadas noutros países e os resultados.

De ambos os estudos, a minha conclusão é que precisamos de mais construção e reabilitação, precisamos de melhores números e acompanhamento da situação e, sobretudo, precisamos de descentralizar a população nas grandes áreas metropolitanas.

Infelizmente, manifestações de tendas dão-me pouca confiança que algo vá mudar. Mas termos novas iniciativas políticas que trabalhem estes desafios parece-me algo com maior probabilidade de funcionar. O resultado na Sérvia de um movimento estudantil ganhar as eleições inspira-me confiança, mas não podemos ter a taxa de abstenção que tem sido habitual no nosso país.

As AI technology gets adopted at a never-seen pace, we also need more people to work on AI Safety to make sure that AI applications are actually safe and aligned.

Because AI generates content and decisions faster than humans, this is a very interesting research problem: humans cannot verify AI alone, so we need smarter technology to do it.

In the interview below Ryan Kidd, the CEO of MATS, talks about the efforts they (and others) are doing to train people in AI Safety. Throughout the conversation he also addresses how many of these AI Safety companies/non-profits have been founded, and even goes into neural networks vs evolutionary algorithms.

But AI Safety is a very large umbrella that encompasses soft skills like Policy Making and writing Model Cards to more technical challenges like interpreting neural networks or building guardrails.

Ankur Pandey argues that AI Safety training is not focusing on building tools and that's probably where the gains are for society. I actually believe existing researchers from technical domains (like formal verification) are equipped to build the tools, they just need funding and support. As an example, Harmonic has been doing interesting stuff recently and I know they recruited the right people.

Unfortunately for those of us who do not want to relocate, many of these AI Safety companies are in-person in Berkeley, DC, Cambridge, NYC and London (with India and Singapore also investing in these areas). If I was funding these efforts, I would hire remotely and I would try to get funding from NATO/EU/UNESCO and other multinational organizations.

As for training, I think we should make sure that all universities offer an AI Safety course at least at the Masters level, but here I am, daydreaming again.

Early this month, OpenAI has released several papers answering decades old problems to which mathematicians have dedicated their own careers. This NYT piece on Terrence Tao (who first supported AI when it was AI to help humans in the process of discovery, but shunned them when it became apparent that they were looking for the discovery for discovery sake, and not for the journey of learning.

Personally, I think it's a matter of changing the training dataset to learn in the process, and AI can do maths the human way very soon.

OpenAI has tried to ask for forgiveness by pledging 5 million to mathematics, maybe hoping that they come back in tokens. On the other side of the duopoly, Anthropic has donated shares to the public good, which seems to me impossible to manage.

AI is here to stay, and it's only a matter of us, humans, mathematicians or software developers finding our raison d'être and learning to communicate with AI in a way that it also advances our knowledge.

At the heart of the crisis in the profession is a menacing question. If solving hard problems is a mission of math, what happens when machines can do it faster? So much of higher math — hiring, promotions, graduate training and acclaim — is based on the difficulty, quality and the impact of papers (the written documents explaining proofs) that a mathematician produces.

The consensus is that A.I.-assisted problem solving is the inevitable future, but no one knows exactly what that new world will look like. “Deep uncertainty will persist in these next years,” a draft report by a group of mathematicians meeting at Harvard on Ph.D. education concluded last month.

— Elisabeth Bumiller on Terry Tao Is on the Front Lines of the Debate Over AI and the Future of Math

This is a completely different subject. Academics created a bean counting system to assess progress that is completely fake. Research is a high-risk activity, like Venture Capital. You invest in many different projects and teams, hoping that one out of 100/1000/1 million succeeds and has a huge impact on society. So you should be okay with the losses you take. It's part of the high-risk/high-reward system.

CoARA and Informatics-Europe provide recommendations to assess researchers: focus on the research and forget bean-counting. But even universities that are trying to adopt CoAra (like my employer, U. Lisbon) forget about the goal and come back to KPIs for fear that funding will be given based on KPIs.

Curiosity-driven research has been responsible for many important discoveries and inventions. So there should be a base funding for that. Then, there should be strategic funding for each country's long-term priorities (healthcare, transportation, defense). Meet with people and fund based on the team and the impact that the project might bring.

To assess researchers, let their peers assess them through conversations and presentations about their work. Do not rely on publication counts and other metrics that can be gamed. And if you are not qualified to evaluate a researcher, maybe you shouldn't had hired them in the first place.

I designed a harness built on top of dependent types that uses information-flow policies to prevent attacks involving the lethal trifecta. However, expecting users to write liquid types was unrealistic, and creating a custom SDK for every external interface—filesystems, APIs, internet search and MCP tools—was not practical.

Following feedback from Lisbon.ai (thanks, Nuno, Fred, Sérgio and David), I started building Fronteira to make these technical ideas accessible to a wider audience.

What is Fronteira?

Fronteira is an MCP proxy that acts as a behavioral firewall. You log in through the browser and add integrations with GitHub, Gmail and other services through their MCP servers. You authenticate your harnesses with Fronteira and automatically get access to all your configured MCP servers. You also get portability across harnesses, but that is just a side effect.

The main advantage of Fronteira is that all MCP interactions go through it, allowing it to track behavior across multiple MCP servers. You get tool-call logging for your harness for free—or, in an enterprise setting, for all your users. I have to admit that this was extremely useful when debugging Fronteira itself, as well as some custom MCP servers.

Because all the data is centralized, we can track where information flows. In particular, this allows Fronteira to stop attacks involving the lethal trifecta. Such an attack can occur when a prompt injection causes an agent to read private data through one tool and expose it to an external endpoint through another. Requiring all interactions to pass through MCP servers is a clear limitation, which I will address later.

Because there are countless MCP providers and possible combinations, each with its own schema, it is impossible for me to write a set of rules that prevents harmful actions for everyone. Instead, Fronteira allows you to write your rules in English and translates them into Guard DSL, a language evaluated deterministically on every interaction.

Users are not expected to write Guard DSL themselves. Instead, they write rules in natural language and can check that the resulting code matches their expectations. The language's usability could be improved, but it is sufficient for the prototypes I have built.

While the rule language is evaluated deterministically, it can invoke nondeterministic components that use decision models—currently JEV—to determine whether content contains trade secrets or medical information. There is also session-level tracking, such as read_private in the example. So far, I have not found anything I could not express, but I am sure that will happen as soon as someone else starts using it.

Limitations and Technical Lessons Learned

The first limitation is clear: top-level harnesses access the filesystem directly, browse the internet directly, control desktop apps and access APIs directly, usually through skills or other instructions. All these interactions bypass Fronteira, making it useless for day-to-day security in your harness.

Second, harnesses come with skills that assume the user is using the harness's official Gmail integration—for example, Codex's integration. If Gmail is only available through Fronteira's MCP endpoint, Codex will sometimes fail to find it out of the box. Deploying Fronteira in the wild would therefore require us to write many skills to change this default behavior.

I also learned that no one respects the fact that MCP tool lists can be dynamic according to the specification. Requests for the tool list can return different results throughout a conversation, but harnesses do not implement support for this. They load the tool list at the beginning and do not reload it unless explicitly asked. I understand the challenge: reloading it before every response would increase the load on MCP servers and add latency. I would like a flag in the response that forces clients to refresh the list.

Furthermore, the MCP schema can change at any time. There is assumption that MCP schemas do not ever change, but I wonder how reliable the assumption is. MCP does not have explicit versioning, although some providers use REST-style versioned endpoints such as /api/v1.

On the other hand, I do not want Fronteira to expose a million tools at all times. I would like it to receive the prompt, or some related information, and dynamically select the relevant tools. Tools forbidden by the rules could then be excluded from the context, rather than occupying space when any attempt to call them would result in an error.

The final technical lesson I learned is that I was too optimistic about trusting Codex with DevOps. I asked it to mirror another app's Django configuration for Fronteira, but it changed the server root, exposing my Resend token and allowing spammers to send spam through my account. The issue was easy to identify and fix, but I expected more from Codex. I also realized that I still do not have a security tool I can point at a deployment, rather than its source code!

Alternatives to Fronteira

I did not look at competitors before implementing Fronteira. This was not because of laziness or incompetence. It was simply not a priority: I wanted to build it regardless, to understand the challenges firsthand.

Behavioral Rules

I was aware of Dogwood, Amazon's temporal specification extension to the Cedar specification (mainly used for AWS access permissions).

Dogwood can require previous explicit approval for some actions. Approval is something I wanted to add to Fronteira from the start through a mobile app. The following temporal rule in Cedar permits a share sale only if the same stock and number of shares were approved within the past hour.

permit (
    principal,
    action == AgentCore::Action::"SellShares",
    resource
)
when temporal {
    formerly within 1h AgentCore::Action::"ApproveSale"::response{
        input.stock: context.input.stock,
        input.shares: context.input.shares,
        output.approved: true
    }
};

To address some of the same limitations as Fronteira, Amazon uses the Dogwood engine in the Strands SDK. By combining the policy engine with a sandbox, they prevent agents from circumventing the "firewall." This is still not foolproof: agents can use a remote browser MCP server to call APIs, avoiding detection.

The Invariant SDK features dataflow guardrails. Both Invariant and Cordon offer MCP proxies like Fronteira. They share the same limitations, but I would like to highlight some interesting language features such as quantifiers and loop detection.

Executor.sh is another MCP proxy that adds some interesting configurations. For instance, it allows you to create policies in typescript, requiring approval of actions, but also more interesting behaviors such as allowing you to undo sending an email in the next 5 minutes.

MCP Proxies with Static Rules

Mintive, previously MintMCP, is very similar to Fronteira, except that it does not support behavioral rules. You can still detect private information leaking through static rules, but you cannot prevent malicious sequences of individually harmless calls.

Both the Lasso Security MCP Gateway and WitnessAI are very similar to Mintive: they automatically manage MCP servers and can detect leaks of information identified as private.

MCP Firewall performs a similar role but also focuses on filtering MCP responses, treating their contents as untrusted because they may contaminate subsequent reasoning.

NVIDIA NeMo is another proxy that validates tool parameters and responses against a range of requirements. However, it does not relate different tool calls to one another except through custom code.

Endram is a proxy that decides whether each call requires manual approval, something Dogwood also supports alongside more complex features.

Both WSO2 and Microsoft Global Secure Access support Cedar-like access control lists for MCP servers, with tool- and prompt-level controls.

Agent Control allows you to create guardrails in Python. These operate at the level of individual tool calls, but Agent Control also integrates with external guardrail infrastructure, such as Dogwood, whose language is more expressive.

Language Specification

AgentSpec is a specification language like Fronteira's, with a more principled design but similar features. I would like to study properties of the language, particularly ways to provide feedback when users write inconsistent rules.

Others

IBM offers MCP ContextForge, a central gateway focused more on discoverability and observability. agentgateway is also mostly focused on observability. TrueFoundry focuses on the M×N problem—M harnesses connecting to N MCP servers—and observability.

LlamaFirewall is similar in that it can inspect traces of calls and detect malicious patterns. However, it does so using a BERT-style LLM, whereas Fronteira primarily supports deterministic analysis.

Comparison Summary

Conclusion

After this exercise, I no longer believe in MCP proxies as security boundaries for agents. MCP covers only part of an agent's interaction with the world. Another reason is that MCP is a leaky abstraction. Models are post-trained in specific MCP and skill contexts, so they will always prefer direct alternatives, creating friction for the user.

However, I strongly believe in the need for logic-based policies to control agents. Those policies should be enforced at the agent boundary and should probably be developed alongside the harnesses and models. I would love this enforcement to be harness-independent and provided by a third party. However, given how models are becoming increasingly harness-specific, I do not see that working in the long term.

If you have read this far, I am looking for a new opportunity where I can apply my research experience in programming languages, systems and different areas of artificial intelligence to improve the safety of agentic systems. If you are looking for someone with that background, along with the agency and pace of someone who has worked at several startups, you can find my contact details on this website.

I certainly would not hire 1,000 third-party consultants to help fix patches. I would probably rethink the architecture of the whole system and company, so that the exposed footprint is minimized. I would give proper training to the internal 3.000 people and power them with AI tooling (even if for monitoring and preventing attacks). And I would even consider open-sourcing the code.

But hiring a lot of (most likely under qualified) people to patch vulnerabilities is a losing game.

If you subscribe to a Meta One plan, you can add links to a set number of posts and reels each month based on your plan:

• Meta One Advanced plan: up to 4 posts and 4 reels with links per month
• Meta One Expert plan: up to 8 posts and 8 reels with links per month
• Meta One Max plan: up to 12 posts and 12 reels with links per month

Meta is trying to sherlock Linktree. But I can't stop and think it's completely bananas that the internet was built on hypertext and openness, and Instagram created a silo and now it's requiring content creators to pay so their users can have a way out.

Capability evaluations aim to surface dangerous model behaviors before deploy- ment, but their reliability depends on the assumption that hidden capabilities can be elicited. We show this assumption does not hold under adversarial conditions by constructing backdoor attacks that embed encrypted neural networks within host model weights, decrypting and executing them only upon receiving a secret trigger. Using digital lockers, these hidden circuits remain provably hard to elicit and interpret under cryptographic assumptions, even given full access to model weights, extending prior work from hiding fixed strings to arbitrary computations. We implement our proof of concept constructions in PyTorch and evaluate elicitation through fine-tuning, weight noising, gradient-based trigger search, and latent adversarial training on a small chemical reaction prediction task – a proxy for CBRN-relevant capabilities. Our results demonstrate resistance to these methods and, together with our cryptographic guarantees, reveal a limit of elicitation-based capability audits. We release our models to support the improvement of defenses.

— AI Models Can Provably Hide Arbitrary Capabilities

This paper presents a way for neural networks to hide functionality (encrypted in apparently random weights) until a trigger message is sent.

In the next 007 movie, we see Q writing PyTorch code under pressure from terrorists, maybe Swordfish style.

This week, we are presenting the Barista paper at ASE'2026, and by 'we', I mean Catarina Gamboa, who is leading this work.

When trying to adopt LiquidJava, an annotation-based language that adds refinements to types, in your Java project, you will have to write the annotations for any library that you use, including the Java Standard Library. This is just a huge amount of work for your simple application. This issue is shared by LiquidHaskell, Frama-C's ACML and Java Modeling Language.

Roughly one year ago, we wanted to explore if we could have LLMs read the documentation (English) and write the specifications for libraries. We focused on a few examples from the Java Standard Library and, given that one year ago LLMs generated more slop than they do today, we came up with an agentic workflow that combined LLM to translate English to an Automata, and the Automata to specification. And by having the automata, we could create positive and negative examples of method call sequences that we could use to validate the generated specification and iterate until we are satisfied.

If you want to learn more about how we come up with the refinements below, you can read the interactive presentation Catarina prepared.

@StateSet({"unconnected", "bound", "connected",
  "inputshutdown", "outputshutdown",
  "bothshutdown", "closed"})
@RefinementAlias("ValidPort(int p) {p >= 0 && p <= 65535}")
@ExternalRefinementsFor("java.net.Socket")
public interface SocketRefinements {

  @StateRefinement(to = "unconnected(this)")
  public void Socket();

  @StateRefinement(to = "connected(this)")
  public void Socket(InetAddress address,
      @Refinement("ValidPort(_)") int port);

  @StateRefinement(from = "unconnected(this)",
                   to = "bound(this)")
  public void bind(SocketAddress bindpoint);

  ...
}

After-thoughts

Presenting this work almost one year after it was conducted feels very strange to me. LLMs have advanced so much in the meantime, that I believe they would be able to get better results without the need for our DFA-oriented architecture. Or probably we would have done a skill-based or tool-based architecture instead of multi-agent. LLMs are now much better at orchestrating the whole process and managing their contextual memory than they were back when we started this.

This paper (along with most of the accepted papers in SE these two years) should probably just be a pre-print, or a living benchmark. The results we present are a product of our time, that would be imperceptible for anyone who wasn't using LLMs to generate code last year, or for the rest of us that forget it easily.

I still see value in our approach, though. I am more and more convinced that we need more verified programming, not to avoid bugs, but rather to gain trust in the source code. While before software engineers would gain trust by building it themselves, and eventually by testing it, both of these tasks are so automated that we need other ways of building trust in our systems. That is an open question that I would love to have a complete answer to. Right now, formal methods and dependently-typed languages are a partial answer to that problem.

If you're in Münich, please go and see Catarina's talk on Thursday.

In our value statements, we usually say we value diversity, but our strategies and plans don’t quite live up that. Academics are themselves diverse. There isn’t a one-size-fits-all job description. The 40-40-20 model itself doesn’t fit everyone, and doesn’t fit every stage of the career. It is natural to focus more on different roles at different times, depending on opportunities and energy. Some of us are just not meant to be president, and not everyone has to lead large EU projects to contribute to research. Individuals sometimes manage to make other types of research contributions by forging productive partnerships, eg between people at different career stages, but it requires them to work against the system a bit, and subvert the expectations the University has written into its metrics.

[...]

Some of my colleagues are probably thinking, based on recent discussions in committees, that I’m kind of bolshie and difficult about university administration activities. Thank you, perhaps yes.

— Being an incentive, being an obstacle, being values by James McDermott

I am the difficult one in my department. Peer Review is in danger, facing an increased number of submissions (both papers and projects for funding). There are AI companies selling solutions to automate some of these solutions, but everyone with a Claude or Codex subscription can generate a paper in a couple of hours. A great paper? maybe not, but enough to be yet another submission to have to review.

In Artificial Intelligence conferences, you are limited to 20 submissions and/or you are required to be a reviewer (ICLR, ICML, NeurIPS). The quality of reviews decreases, and there are undergraduates [reviewing] some papers. I'm all in favor of Shadow PCs, but this seems too random to attribute any level of trust to the reviewers.

In Software Engineering, ICSE defined a maximum of 3 submissions (remember the Guinness World Record-level 12 accepted papers by the same author). ICSE, FSE and TOSEM have also agreed to share review(er)s, to avoid repeated work on the same submissions (reducing the reviewer bias resilience).

Other areas are also following suit with senior authors having to agree to review papers if needed, imposing submission limits, and even adding a submission fee.

These are all patches, not solutions to the problem. Many people have identified the solution: we must not count the number of papers (or funded projects) in the bean-counting process of research evaluation. If you give that much importance to a measure, the measure itself becomes the goal, and Peer Review will not survive.

And who rules the university? We do. It's a collegial management, so we need each of us to rise against these practices. Bureaucrats require KPIs and metrics that do not look at the substance of the work. But the idea of being a collegial organization is that we should look at the substance (and that requires time, that no one wants to spend).

And this is not a new idea. David Parnas said it in 2007, Computing Research Association has said it in 1999 and in 2015.

Another related issue is that when everyone is targeting Q1 and Core A/A* conferences (~top 25% venues), the top 25% conferences are now responsible for 75% of the submissions, and lower ranked venues die. This is non-sensical.

Recommendation R4.1 states: “Publication counts, whether weighted or not, must not be used to evaluate research value.”

— Informatics Europe, Informatics Research Evaluation (2025)

“the scientific content of a paper is much more important than publication metrics or the identity of the journal in which it was published.”

— DORA, recommendation 4

I agree with James, we need to fight for this change ourselves, because the attrition of the big machine of large organizations is against us.

If you deeply care about security, there are really two choices: You're sending satellites into space, and you should probably use seL4, a formally verified operating system. (I'm still a bit salty about the Australian government disbanding that team.) Everyone else should seriously consider unikernels. Stop trying to harden something that is very hackable. Invert it and design from the other direction.

— Geoffrey Huntley in unikernels were hard. key word: were.

I have been a fan of Unikernels since MirageOS was announced, but OCaml was always an issue, mostly because of the lack of libraries for unikernels, but also because of the double semicolon (sorry Jane Streeters, French people and CMUers).

In the age of agents, unikernels make sense to isolate agent tasks so that they have as little (security-attackable) surface as possible, finish as fast as possible, and you can run as many in a single machine as possible.

However, you need some kind of inter-unikernel communication protocol (some lightweight semantic socket) so that you can spawn several unikernels, designed for single-purpose tasks, and gather the results they found.

If you are working on such a topic, hit me up.

Unfortunately, monitoring for adversarial data access turns out to be one of the hardest problems you could imagine. The volume of data that agents produce is so high that no human being could possibly read it, and we probably wouldn’t recognize obfuscated malicious data even if we were looking directly at it. This means any attempt to monitor the inflow/outflow will have to be handled by other models. Thus, the future of agent sandboxing is (1) build a sandbox, (2) install an agent/model into it, (3) install a somewhat dumber/cheaper warden model to guard it, (4) hope you can trust the lunkhead to contain the wizard. And so on and so forth, as models become more intelligent and capable.

In other words: a warden-guarded sandbox is just another version of the alignment problem. You’re going to have to trust a model to do it, and that model will need to be at least some fraction as intelligent as the model it’s guarding. If you haven’t convinced yourself that it’s possible to build models you can trust, then sandboxing isn’t going to take you much farther.

— Matthew Green in Is sandboxing sufficient to contain rogue agents? – A Few Thoughts on Cryptographic Engineering

Matthew Green, a cryptographer at Johns Hopkins University, points out what I have been saying for a while: if you want your agents to be useful, they have to be able to access information and perform actions. How do you prevent those actions from being harmful? You use another agent to deny or allow each action. Thus alignment is still relevant, even if for the bouncer controlling the sandbox escape.

I actually believe we should be using deterministic guardrails that can be audited, instead of another model as a border patrol agent. I am working on such solution, which I will be sharing soon enough.

One thing I find notable about S3 today is that, while it used to drop in price reasonably often, there hasn't been a price drop in a full decade:

2006-03-14  $0.150/GB-month
2010-11-01  $0.140/GB-month
2012-02-01  $0.125/GB-month
2012-12-01  $0.095/GB-month
2014-02-01  $0.085/GB-month
2014-04-01  $0.030/GB-month
2016-12-01  $0.023/GB-month

Today it's still $0.023/GB-month.

— Simon Willison

I actually can't believe it hasn't gone up in the last couple of months.

Published in the 16th century, Journey to the West is a classic Chinese novel that tells the tale of Sun Wukong, a mythological monkey that helps a Buddhist monk journey to India. Among the many published sequels to Journey to the West, one of the three main ones, written by an unknown author, is The Later Journey to the West [后西游记]. In this sequel, the story shifts to Sun Xiaosheng, a young stone monkey who grows up on the same mountain long after Sun Wukong departed on his journey.

On August 31, Mango Excellent Media’s TV adaptation of this novel premiered during prime time. “It’s the first-ever fully AI-generated entertainment to hit mainstream provincial satellite prime time,” writes Mandy Wong. After seeing Bytedance Seedance 2.0’s (AI text-to-video model) release earlier this year, the team behind Journey to the West felt there was an opportunity to make a long-form series and break through a market “saturated with uninspired short-form dramas.” In this week’s feature translation (link to Huxiu article), Shuhan Liu reports on the makings of this AI-generated TV series.

Key Takeaways: From initial planning in March of this year to the premiere on August 31, the project took just six months (traditional TV dramas take 1-2 years). ByteDance’s Seeedance 2.0 and 2.5 models generated all the visuals, without live-action actors and filmed footage.

— ChinAI #374: China’s first AI-generated longform TV series by Jeffrey Ding

In the way-less-protective-than-europe US, there are writers’ strikes that prevent this from happening. What if, just as crazy idea, China decides to produce English-speaking TV shows?

Post-literacy is different from illiteracy. We can still read, but we prefer videos and podcasts to writing. This laziness is transforming us from a written society into an oral society. Oral societies think in ways that are more tribal than written ones: they are more forgetful, irrational, superficial, and simplistic. Thus, democracy, and perhaps the enlightenment itself, is imperilled.

— It’s the screens, stupid! by Alexander Thompson, a review of James Marriott's The New Dark Ages

Worth the rid to understand the relationship between screens (and their different nature) and society.

The 15-year-old passengers were riding in a driverless autonomous car around San Mateo Monday afternoon. The teens drank alcohol inside the Waymo taxi and shot Orbeez beads with a toy gun toward other vehicles.

A Waymo employee, who was remotely monitoring the car, tricked the unruly teenagers, authorities said. The employee told the young passengers that the Waymo was having mechanical issues and needed to stop.

Unknown to the teens, the employee had also called the San Mateo Police Department to report that a gun was firing from the car.

— The expectations of privacy in driverless cars – Terence Eden’s Blog by Terence Eden

Driverless cars are public spaces, currently owned by private companies who have the interest in protecting their property (the car) and their business (by being law-abiding, and avoiding issues like people dying in their cars).

Once (or if...) driverless cars become state owned, then I think that discussion should be relevant again.

— Wizard of Id — 13th September 2026

Not being a fan of monopoly when it comes to Good Boardgames™ (try Suburbia or Tigris & Euphrates if you want something actually good), but we really need an interactive media experience closer to Black Mirror or Years and Years. AI Safety is a big issue today, but no one wants to watch or play the media from the 80ies (WarGames), 90ies (The Net) or 2000s (I, Robot, A.I., Minority Report).

We have been working on aeon, a programming language with refinement types. Unliked add-on liquid types (LiquidHaskell, LiquidJava or Flux), it was designed to have them threaded throughout the program. Because of that, it has a very weird syntax that I have lately been changing to be as close to Lean as possible, so people don't have to learn yet another programming language.

Because aeon includes program synthesis capabilities, using a bunch of algorithms, my student Su decided to add support for LLM generation of aeon code inside the compiler. Back then, he used a system prompt that explained that the language was and how it related to existing languages.

However, this past year I have been using Sonnet, Opus, different GPTs and they have all been able to synthesize aeon code without a problem. The harness is good enough that it detects other .ae files in the repo and loads them into the context, and LLMs can easily learn languages from examples.

However, I wanted to understand how much fine-tuning alone could help models generate code in new programming languages. With my 3090 TI in hand, I set up the following experience:

I took 100 medium-sized aeon programs from the official repo, split into 80% training and 20% hold-out for evaluation. Each of the two models, Qwen 2.5 Coder 14B and Gwen 3.5-9B, was fine-tuned for 8 hours using LoRA within the limits of the GPU. Then, I assessed whether the generated programs (based on the 20% programs not used in fine-tuning) had a correct syntax.

The fine-tuned models were able to get it right more than half of times, while the original models were oblivious to this "new" programming language. Qwen 2.5 outperformed Qwen3.5, which is expected, given that smaller models are easier to fine-tune.

As a next step, we could perform fine-tuning, make the new weights available on HuggingFace and automatically download them inside the compiler, if the user has a compatible machine. But because the target user is only myself, I'll just use proper harnesses.